Opened 4 years ago

Closed 4 years ago

#11428 closed bug (fixed)

ImpredicativeTypes causes GHC panic with 8.0.1-rc1

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: ImpredicativeTypes, TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


I noticed this issue when attempting to compile conduit with GHC 8.0.1-rc1 (specifically, the Data.Conduit.Internal.Pipe module). This (greatly simplified) code, which compiles without issue on GHC 7.10.3:

{-# LANGUAGE ImpredicativeTypes #-}
module Data.Conduit.Internal.Pipe where

data Pipe o r =
    HaveOutput (Pipe o r) o

mapOutputMaybe :: (o1 -> Maybe o2) -> Pipe o1 r -> Pipe o2 r
mapOutputMaybe f (HaveOutput p o) =
  maybe id (\o' p' -> HaveOutput p' o') (f o) (mapOutputMaybe f p)

emits a GHC panic with GHC 8.0.1-rc1:

[1 of 1] Compiling Data.Conduit.Internal.Pipe ( Wat.hs, interpreted )
ghc: panic! (the 'impossible' happened)
  (GHC version for x86_64-unknown-linux):
  a_a15Z[tau:5] -> b_a15Y[tau:5]

Please report this as a GHC bug:

Note that this code does not require -XImpredicativeTypes, and removing the pragma makes the code compile again.

Marking as high since it's a regression, but not highest because -XImpredicativeTypes has long been broken (see also #11319). Still, this currently happens on code in the wild, and perhaps it would be worth turning this into a more sensible error.

Change History (3)

comment:1 Changed 4 years ago by simonpj

Keywords: TypeApplications added
Milestone: 8.0.1

comment:2 Changed 4 years ago by goldfire

Hopefully my work (Phab:D1777 is an unfinished checkpoint) toward #11397 will nab this as well.

comment:3 Changed 4 years ago by bgamari

Resolution: fixed
Status: newclosed

Indeed this now fails with the error

T11428.hs:12:13: error:
    • Couldn't match expected type ‘forall a. a -> a’
                  with actual type ‘Pipe o2 r0 -> Pipe o2 r0’
    • When checking that: Pipe o2 r0 -> Pipe o2 r0
        is more polymorphic than: forall a. a -> a
      The lambda expression ‘\ o' p' -> HaveOutput p' o'’
      has two arguments,
      but its type ‘o2 -> forall a. a -> a’ has only one
      In the second argument of ‘maybe’, namely
        ‘(\ o' p' -> HaveOutput p' o')’
    • Relevant bindings include
        f :: o1 -> Maybe o2 (bound at T11428.hs:11:16)
        mapOutputMaybe :: (o1 -> Maybe o2) -> Pipe o1 r -> Pipe o2 r
          (bound at T11428.hs:11:1)

When compiled with ImpredicativeTypes.

Note: See TracTickets for help on using tickets.