[Haskell-cafe] Well-typed functions with nonexisting signatures [Was: type variable question]

[oleg at pobox.com]

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.