#11355 closed bug (fixed)

TypeApplications + RankNTypes permits "impredicativity"

Reported by: adamgundry Owned by: goldfire
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.11
Keywords: TypeApplications Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T11355
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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?

Change History (7)

comment:1 Changed 21 months ago by simonpj

Keywords: TypeInType added

comment:2 Changed 21 months ago by goldfire

Keywords: TypeApplications added; TypeInType removed
Owner: set to goldfire

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?

comment:3 Changed 21 months ago by adamgundry

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]

comment:4 Changed 21 months ago by Richard Eisenberg <eir@…>

In e6ca9300/ghc:

Fix #11355.

Previously, the check for impredicative type applications was
in the wrong spot.

Test case: typecheck/should_fail/T11355

comment:5 Changed 21 months ago by goldfire

Milestone: 8.0.1
Status: newmerge
Test Case: typecheck/should_fail/T11355

comment:6 Changed 21 months ago by bgamari

Cherry-picked to ghc-8.0 as d4661c1adc732b12d39a6aab4a3f5a8c61e27dde.

comment:7 Changed 21 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.