Eu me deparei com esse problema ao analisar mônadas livres, mas o reduzi a um exemplo muito menor.
Em Haskell temos o seguinte tipo:
fmap :: Functor f => (a -> b) -> f a -> f b
Suponha também que temos a seguinte função:
foo :: Num a => p -> a
foo = \_ -> 1
Então
fmap foo :: (Functor f, Num b) => f a -> f b
-- and
fmap (fmap foo)
:: (Functor f1, Functor f2, Num b) => f1 (f2 a) -> f1 (f2 b)
Então seria de se esperar que pudéssemos aplicar fmap (fmap foo)somente a algo do tipo (Functor f1, Functor f2) => f1 (f2 a), mas
fmap (fmap foo) foo :: (Functor f, Num b, Num (f a)) => p -> f b
O quê? Por que esse tipo verifica e por que ele tem o tipo fornecido?
Se alguém pudesse explicar o que está acontecendo aqui, isso seria muito apreciado. Peço desculpas pelo título vago, mas não entendo o suficiente o que está acontecendo aqui para torná-lo mais específico. Ficarei feliz em atualizá-lo para algo mais pesquisável depois que uma resposta esclarecer.