Type error when annotating a let binding with a forall type
|Reported by:||pelotom||Owned by:||simonpj|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||Differential Rev(s):|
I'm not sure if this is a bug or not, but it's certainly counterintuitive to me.
Why does this example fail to type check?
Prelude> let (x :: forall a. a -> a) = id in x 3 <interactive>:0:31: Couldn't match expected type `forall a. a -> a' with actual type `a0 -> a0' In the expression: id In a pattern binding: (x :: forall a. a -> a) = id
I have RankNTypes and ScopedTypeVariables enabled.
I asked this question on StackOverflow: http://stackoverflow.com/questions/8190431/type-error-when-ascribing-a-valid-forall-type-to-a-let-bound-variable
User ibid's theory there was this:
"In a let binding let x = id in ..., what happens is that id's type forall a. a->a gets instantiated into a monotype, say a0 -> a0, which is then assigned as x's type and is then generalized as forall a0. a0 -> a0. If, as I think, the pattern type signature is checked before generalization, it's essentially asking the compiler to verify that the monotype a0 -> a0 is more general than the polytype forall a. a -> a, which it isn't."