TypeApplications + RankNTypes permits "impredicativity"

I was slightly surprised to discover that the combination of TypeApplications and RankNTypes allows impredicative instantiations, for example:

map @(forall a . a) :: ((forall a. a) -> b) -> [forall a. a] -> [b]

Is this desirable, or should it require ImpredicativeTypes?

Trac metadata

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

changed weight to 5

added Tbug Trac import labels

added TypeInType label

assigned to @rae

This is not desirable. I think I see why this happens, and I have a fix, but I actually can't reproduce. Do you have a minimal complete test case?

added TypeApplications label and removed TypeInType label

I see, the above works with the :t command in GHCi, but trying to evaluate it or compile it in a module gives this error:

    • Illegal polymorphic or qualified type: forall a1. a1 -> a1
      GHC doesn't yet support impredicative polymorphism
    • When checking the inferred type
        t :: forall b.
             ((forall a. a -> a) -> b) -> [forall a. a -> a] -> [b]

Should this message mention ImpredicativeTypes? In theory, it ought to be possible to actually use ImpredicativeTypes now if you insert enough type applications.

However, the following example compiles, and I think it shouldn't:

{-# LANGUAGE RankNTypes, TypeApplications #-}
module T11355 where
t = map @(forall a . a -> a) ($ True) [id]

mentioned in commit e6ca9300

changed milestone to %8.0.1

Trac metadata

Trac field	Value
Test case	- → typecheck/should_fail/T11355

added 1 deleted label

Cherry-picked to ghc-8.0 as d4661c1a.

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added Pnormal label