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... [3] http://stackoverflow.com/questions/5885479/weird-error-when-using-scoped-typ... [4] http://hackage.haskell.org/trac/ghc/ticket/4347