Shouldn't this require ImpredicativeTypes?

The following program compiles:

{-# LANGUAGE RankNTypes #-}
module TestRN1 where

type X = forall a . a

comp :: (X -> c) -> (a -> X) -> (a -> c)
comp = (.)

But this one fails:

{-# LANGUAGE RankNTypes #-}
module TestRN2 where

comp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)
comp = (.)

Error:

    Cannot instantiate unification variable ‘b0’
    with a type involving foralls: forall a1. a1
      Perhaps you want ImpredicativeTypes
    In the expression: (.)
    In an equation for ‘comp’: comp = (.)

I would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.

Trac metadata

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