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.
|Component||Compiler (Type checker)|