Panic with promoted types that Typeable doesn't support

The following program panics on GHC 8.2 and later:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Type.Reflection

newtype Foo = MkFoo (forall a. a)

foo :: TypeRep MkFoo
foo = typeRep @MkFoo

$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
GHC error in desugarer lookup in Bug:
  attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.1 for x86_64-unknown-linux):
        initDs

Trac metadata

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

changed weight to 5

added Tbug Trac import Typeable labels

I was surprised to see this, so I tried

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Type.Reflection

newtype Foo = MkFoo (forall a. a)

foo :: TypeRep MkFoo
foo = undefined

instead. And that program is accepted... but it really shouldn't be.

The problem is that the type of foo is TypeRep @((forall a. a) -> Foo) 'MkFoo, which involves an impredicative instantiation of the kind variable of TypeRep. This is not currently allowed.

I would fix the missing impredicativity check before worrying about initDs.

However, with #12045 (closed), I suppose we'll want to start allowing impredicative kind instantiations... even then, we won't be able to deal with type representations involving foralls (at least, not without another rewrite of TypeRep). So, I suppose tackling the initDs bug directly is also a step forward.

Replying to [ticket:15862#comment:163196 goldfire]:

I would fix the missing impredicativity check before worrying about initDs.

In case you didn't notice this, I deliberately enabled ImpredicativeTypes in this program :)

I, too, am surprised that this panics, though. Especially since typeIsTypeable appears to already answer "no" when a type contains a nested forall like this:

typeIsTypeable (ForAllTy{})         = False

It's possible that something else is going wrong, though.

added ImpredicativeTypes label and removed Typeable label

changed title from Typeable panic with promoted rank-2 kind (initDs) to Panic with promoted types that Typeable doesn't support

It turns out that this problem is more general than just this one example (which happens to use ImpredicativeTypes). Here is //another// program which triggers the same panic:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Type.Reflection

type family F a
type instance F Int = Type

data Bar = forall (a :: F Int). MkBar a

bar :: TypeRep (MkBar True)
bar = typeRep

This time, the culprit is likely the fact that MkBar True contains a cast/coercion somewhere, which is another thing that Typeable doesn't support.

added Typeable label and removed ImpredicativeTypes label

Unboxed sums, too:

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UnboxedSums #-}
module Bug where

import Type.Reflection

data Quux = MkQuux (# Bool | Int #)

bar :: TypeRep MkQuux
bar = typeRep

$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
GHC error in desugarer lookup in Bug:
  attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.2 for x86_64-unknown-linux):
        initDs

This also fails

data Bar where
  MkBar :: forall (a :: F Int). a -> Bar

but this succeeds

data Bar where
  MkBar :: (a :: F Int) -> Bar

where

>> bar
'MkBar Bool 'True

added TypeInType label and removed Typeable label

added Typeable label

added compiler crash label

Also for data constructors that use Eq# behind the scenes:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
module Bug where

import Data.Kind
import Type.Reflection

data Quuz :: (Type ~ Type) => Type where
  MkQuuz :: Quuz

quuz :: TypeRep MkQuuz
quuz = typeRep

$ /opt/ghc/8.6.5/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
GHC error in desugarer lookup in Bug:
  attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.5 for x86_64-unknown-linux):
        initDs

Note that this does not panic if you change TypeRep MkQuuz to TypeRep Quuz; that merely triggers the same error message as in #13933.

assigned to @RyanGlScott

mentioned in merge request !1199 (closed)

Aha, I've figured out what's going on here. The culprit isn't typeIsTypeable at all, unlike what I surmised in #15862 (comment 163203). Instead, the real issue is that the code in the Typeable solver isn't synchronized properly with the validity checks in TcTypeable, which means that it tries to generate Typeable evidence for type constructors that TcTypeable rejects as impermissible. This, in turn, results in the panics observed above.

I've submitted a fix at !1199 (closed).

mentioned in commit ec0d61d1

mentioned in commit 027f9ec1

mentioned in commit 9fabc85b

mentioned in commit 623a627e

closed via commit 25ee60cd

mentioned in commit 25ee60cd

Testsuite-tests: typecheck/should_fail/T15862

changed milestone to %8.10.1

mentioned in issue #16835 (closed)

mentioned in commit 5a167d0c

changed milestone to %8.8.1

added 1 deleted label

mentioned in commit 272c1988

mentioned in commit 27425530

mentioned in commit 3b780065

mentioned in commit fc7bdba6

added Pnormal label

removed 1 deleted label