[Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]

[Don Stewart]

andrewcoppin:
> Gleb Alexeyev wrote:
> >foo :: (forall a . a -> a) -> (Bool, String)
> >foo g = (g True, g "bzzt")
> 
> So, after an entire day of boggling my mind over this, I have brought it 
> down to one simple example:
> 
>  (id 'J', id True)   -- Works perfectly.
> 
>  \f -> (f 'J', f True)   -- Fails miserably.
> 
> Both expressions are obviously perfectly type-safe, and yet the type 
> checker stubbornly rejects the second example. Clearly this is a flaw in 
> the type checker.

I'm sorry you are still confused, Andrew.

This is documented rather nicely in section 8.7.4.2 of
the GHC user's guide. In particularly, you'll want to not ethat
arbitrary rank type inference is undecidable, so GHC imposes a
simple rule requiring you to annotate those polymorphic parameters
of higher rank you want.

See here

  http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id408394

Read this carefully, and then read the references.

> Interestingly, if you throw in the undocumented "forall" keyword, 
> everything magically works:
> 
>  (forall x. x -> x) -> (Char, Bool)
> 
> Obviously, the syntax is fairly untidy. And the program is now not valid 
> Haskell according to the written standard. And best of all, the compiler 
> seems unable to deduce this type automatically either.

Please read the above link. In particular, pay attention to the word
"undecidable". Reading and comprehending Odersky and Laufer's paper, "Putting
type annotations to work", will explain precisely why you're butting
your head up against deciability.

-- Don