
Nicolas Frisby wrote
The commented out signature is the signature that GHC infers for the function. When I uncomment that signature, it will no longer type check. Why does this happen? Even with the forall and the explicit signatures in the where clause, it chokes.
Alas, this is the property of Haskell, even of Haskell98. Half a year ago I even wanted to write a message on the Haskell' list, pointing out the embarrassment. One one hand, writing signatures is highly recommended. On the other hand, there exist, even in Haskell98, well-typed functions for which signatures simply do not exist. The number of such exceptions multiply when we move to higher-rank types (where such anomalies are to be expected). The reason for the anomalies is the difference between the 'internal' language that expresses inferred types and the external type language.
Is there a canonical example example that exhibits this behavior?
Yes, it was discussed back in 2003. Here's the canonical form: g::(Show a,Show b) => a->b g = undefined --h :: Show a => b -> a h x = g(h x) Both Hugs and GHC (in the pure Haskell98 mode!) are happy with h. Both compilers infer the type for h, shown in the comment. If you give h the type signature -- the one that is inferred by the compilers themselves -- both compilers complain. This example has been distilled from practical problems (the earliest one was by Levent Erkok reported back on 2000) http://www.mail-archive.com/haskell@haskell.org/msg06754.html The following thread gives more detail and discussion: http://www.haskell.org/pipermail/haskell/2003-May/011730.html The final solution to the problem is in http://www.haskell.org/pipermail/haskell/2003-May/011762.html I have actually managed to give h the type signature. The following message indicates that the problem is actually quite common: http://www.haskell.org/pipermail/haskell-cafe/2003-May/004302.html Here's an example of an anomaly with higher-rank types: http://www.haskell.org/pipermail/haskell-cafe/2004-October/007207.html http://www.haskell.org/pipermail/haskell-cafe/2004-October/007212.html we can define functions Foo and Bar (data constructors are functions) such that we can write
myFoo :: Int -> Foo myFoo i = Foo (Bar run op) where run :: Monad m => StateT Int m a -> m a run prog = do (a, s) <- runStateT prog i return a op :: Monad m => StateT Int m Int op = get
but we cannot write the composition of Foo and Bar more directly:
foo run op = Foo (Bar run op)
The latter is not accepted: it must have a signature but no signature can ever be given to this function.