Opened 5 years ago

Closed 23 months ago

#9420 closed bug (fixed)

Impredicative type instantiation without -XImpredicativeTypes

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.9
Keywords: ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11319 Differential Rev(s):
Wiki Page:

Description

Consider this module:

{-# LANGUAGE RankNTypes #-}

module Bug where

rank2 :: ((forall a. a -> a) -> b) -> ()
rank2 _ = ()

foo :: () -> ()
foo x = x

quux :: (forall a. a -> a) -> Int
quux _ = 5

bar = foo . rank2 $ quux

The (.) in the definition of bar requires an impredicative instantiation -- that is, one of its type variables is instantiated to a forall-type. Yet, the module compiles without -XImpredicativeTypes. To confirm this behavior, the following is an excerpt from -ddump-simpl:

Bug.bar =
  break<7>()
  (break<6>()
   GHC.Base..
     @ ()
     @ ()
     @ ((forall a_a1Tj. a_a1Tj -> a_a1Tj) -> GHC.Types.Int)
     Bug.foo
     (Bug.rank2 @ GHC.Types.Int))
    Bug.quux

Note the third type argument to (.).

Fixing this would be a breaking change that could affect users.

Change History (4)

comment:1 Changed 5 years ago by simonpj

See also #4347, #4295, #7264, #8808, #9420

comment:2 Changed 4 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:3 Changed 2 years ago by simonpj

Keywords: ImpredicativeTypes added

comment:4 Changed 23 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

This has been fixed since GHC 8.0.1, since GHC now does properly detect the impredicative instantiation:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug2.hs, interpreted )

Bug2.hs:14:13: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls: (forall a. a -> a) -> b0
        GHC doesn't yet support impredicative polymorphism
    • In the second argument of ‘(.)’, namely ‘rank2’
      In the expression: foo . rank2
      In the expression: foo . rank2 $ quux
   |
14 | bar = foo . rank2 $ quux
   |             ^^^^^

Bug2.hs:14:21: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls: (forall a. a -> a) -> Int
        GHC doesn't yet support impredicative polymorphism
    • In the second argument of ‘($)’, namely ‘quux’
      In the expression: foo . rank2 $ quux
      In an equation for ‘bar’: bar = foo . rank2 $ quux
   |
14 | bar = foo . rank2 $ quux
   |                     ^^^^

(See also #11319 for the plan to allow such impredicative instantiations via TypeApplications.)

Note: See TracTickets for help on using tickets.