Opened 4 years ago
Closed 4 years ago
#5650 closed bug (invalid)
Type error when annotating a let binding with a forall type
Reported by: | pelotom | Owned by: | simonpj |
---|---|---|---|
Priority: | normal | Milestone: | 7.4.1 |
Component: | Compiler | Version: | 7.2.1 |
Keywords: | Cc: | ||
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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."
Change History (3)
comment:1 Changed 4 years ago by igloo
- Milestone set to 7.4.1
- Owner set to simonpj
comment:2 Changed 4 years ago by pelotom
comment:3 Changed 4 years ago by simonpj
- difficulty set to Unknown
- Resolution set to invalid
- Status changed from new to closed
It's quite right actually. The Haskell 2010 Report, in the section on pattern bindings, http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-880004.5, defines the static semantics of
p = e
where pattern p binds variables x1 .. xn, thus:
t = e x1 = case t of p -> x1 ... xn = case t of p -> xn
So let's try that with your example, which is a (degenerate) pattern binding:
t = id x = case t of (x :: forall a. a->a) -> x
When you typecheck this, t gets type forall a. a->a, but the occurrence of t in the rhs of x is instantiated, of course, to give type b -> b, where we don't yet know the type b. And that fails to match the type of x in the pattern.
So I think GHC is following the specification.
Simon
I also asked this question on SO, which seems like it may be a related. In that case, GHC 6.12.1 actually accepts the type, whereas 7.x rejects it.