Opened 13 months ago

Last modified 5 months ago

#15862 new bug

Panic with promoted types that Typeable doesn't support

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.1
Keywords: Typeable, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (8)

comment:1 Changed 13 months ago by goldfire

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, 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.

comment:2 in reply to:  1 Changed 13 months ago by RyanGlScott

Replying to 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.

comment:3 Changed 13 months ago by simonpj

Keywords: ImpredicativeTypes added

comment:4 Changed 12 months ago by RyanGlScott

Keywords: ImpredicativeTypes removed
Summary: Typeable panic with promoted rank-2 kind (initDs)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.

comment:5 Changed 12 months ago by RyanGlScott

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

comment:6 Changed 12 months ago by Iceland_jack

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
Last edited 12 months ago by Iceland_jack (previous) (diff)

comment:7 Changed 12 months ago by RyanGlScott

Keywords: TypeInType added

comment:8 Changed 5 months ago by Marge Bot <ben+marge-bot@…>

In 25ee60cd/ghc:

Synchronize ClsInst.doTyConApp with TcTypeable validity checks (#15862)

Issue #15862 demonstrated examples of type constructors on which
`TcTypeable.tyConIsTypeable` would return `False`, but the `Typeable`
constraint solver in `ClsInst` (in particular, `doTyConApp`) would
try to generate `Typeable` evidence for anyway, resulting in
disaster. This incongruity was caused by the fact that `doTyConApp`
was using a weaker validity check than `tyConIsTypeable` to determine
if a type constructor warrants `Typeable` evidence or not. The
solution, perhaps unsurprisingly, is to use `tyConIsTypeable` in
`doTyConApp` instead.

To avoid import cycles between `ClsInst` and `TcTypeable`, I factored
out `tyConIsTypeable` into its own module, `TcTypeableValidity`.

Fixes #15862.
Note: See TracTickets for help on using tickets.