[Haskell-cafe] ScopedTypeVariables in let-bindings (not where-bindings!) and bug 4347

[Paolo G. Giarrusso]

Hi all, I have some problem with ScopedTypeVariables, let and so on,
at least in GHC 7.
My aim is to be able to supply a polymorphic type signature in let
bindings. Confusingly, I find no such example in the blog post about
local let generalization [1]. I first met this problem when porting
some test-code from Kiselyov, when refusing to convert its let-
bindings into where-bindings (which, btw, can't be typed into GHCi).
I've also added a comment to the bug report, but it's still quite
possible that I'm missing something.

== Summary ==
My starting point today: I wanted to test polymorphic recursion by
entering this definition into GHCi:
a :: a -> a
a = a a
This is accepted without extra language pragmas but only with the type
signature, due to the use of polymorphic recursion for which type
inference is undecidable.
To type it into GHCi I need to supply a polymorphic type in a let-
binding. However, it turns out that
Prelude> let id2 :: Int -> Int = \x -> x
works but there's no way whatsoever to make the following work:
Prelude> let (id2 :: forall t. t -> t) = \x -> x

because of bug 4347.

But let's start from the beginning.
== Walk-through, with various other complaints. ==
So let's try this:
$ ghci -XScopedTypeVariables
Prelude> let a :: forall b. b -> b = a a
[...request of enabling -XRank2Types or -XRankNTypes, confusing or
BUGGY because the type is rank-1 ...]

Prelude> :set -XRank2Types
Prelude> let a :: forall b. b -> b = a a

<interactive>:1:31:
    Couldn't match expected type `forall b. b -> b'
                with actual type `b0 -> b0'
    In the first argument of `a', namely `a'
    In the expression: a a
    In a pattern binding: a :: forall b. b -> b = a a

Uh? That's strange. Seems an instance of bug #4347, but the error
message is not yet the same. To get that, let's make an easier
example: id. Of course, it needs no type signature, but if one can't
give to this an explicit signature, realistic examples are hopeless.

So, at the GHCi 7.0.3 prompt, I can't type:
Prelude> let id2 :: t -> t = \x -> x
GHCi first suggests using -XScopedTypeVariables. Let's try that:
Prelude> :set -XScopedTypeVariables
Prelude> let (id2 :: Int -> Int) = \x -> x
This monomorphic function is fine, but the original polymorphic one is
not accepted, it complains that t is not in scope - fine, let's add
forall:
*Main> let (id :: forall t. t -> t) = \x -> x

<interactive>:1:6:
    Illegal polymorphic or qualified type: forall t. t -> t
    Perhaps you intended to use -XRankNTypes or -XRank2Types
    In a pattern type signature: forall t. t -> t
    In the pattern: id :: forall t. t -> t
    In a pattern binding: (id :: forall t. t -> t) = \ x -> x

This is already confusing for me - the intended type is rank-1. But
let's listen to GHCi again:
Prelude> :set -XRank2Types

Now, the error message is really puzzling:
Prelude> let (id2 :: forall t. t -> t) = \x -> x

<interactive>:1:33:
    Couldn't match expected type `t0 -> t1'
                with actual type `forall t. t -> t'
    The lambda expression `\ x -> x' has one argument,
    but its type `forall t. t -> t' has none
    In the expression: \ x -> x
    In a pattern binding: (id2 :: forall t. t -> t) = \ x -> x

What's up? The documentation never mention let, but it does mention
type signatures for patterns [2], and in "let a = b in c", "a" is IIRC
a considered a pattern. Still, the lack of examples with let is
already confusing.
id2 :: forall t. t -> t = \x -> x
How does "forall t. t -> t" have no argument? At worst, it expects a
type-argument, in its System F representation . The only
implementation problem I see in this code is that unification must
"see through" the forall. I've seen this behavior described [3, 4],
but all the problematic examples have been fixed in some way. Here, I
see no direct fix.

Best regards
Paolo G. Giarrusso

[1] http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
[2] http://www.haskell.org/ghc/docs/7.0.3/html/users_guide/other-type-extensions.html#pattern-type-sigs
[3] http://stackoverflow.com/questions/5885479/weird-error-when-using-scoped-type-variables-and-the-y-combinator-in-haskell
[4] http://hackage.haskell.org/trac/ghc/ticket/4347