Bug in unification of polymorphic and not-yet-polymorphic type

The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of ($) where it would have to be instantiated impredicatively.

Initially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because:

const :: a -> (forall b. b) -> a

is accepted by the type checker. However, the simple:

id :: (forall a. a) -> (forall b. b)

is not, giving an error message:

    Couldn't match type `b' with `forall a. a'
      `b' is a rigid type variable bound by
          an expression type signature at <interactive>:1:32
    In the expression: id :: (forall a. a) -> (forall b. b)

This would seem to indicate that the type is being rewritten to:

forall b. (forall a. a) -> b

and then the forall a. a matched with the bare b. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation.

Trac metadata

Trac field	Value
Version	7.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture