Opened 6 years ago

Closed 6 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:


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

    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:

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 6 years ago by igloo

Milestone: 7.4.1
Owner: set to simonpj

comment:2 Changed 6 years ago by pelotom

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.

comment:3 Changed 6 years ago by simonpj

difficulty: Unknown
Resolution: invalid
Status: newclosed

It's quite right actually. The Haskell 2010 Report, in the section on pattern bindings,, 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.


Note: See TracTickets for help on using tickets.