GHC 9.0.1+ panics (No skolem info), GHC 8.10.4 produces error message
If you compile the following program with GHC 9.0.1 or later, it will panic:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
type Sing :: k -> Type
type family Sing
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type D :: Type -> Type
data D a = MkD a
type SD :: D a -> Type
data SD z where
SMkD :: Sing x -> SD (MkD x)
type instance Sing @(D a) = SD
elimD :: forall a (p :: D a ~> Type) (d :: D a).
Sing d
-> (forall (x :: a). Sing x -> Apply p (MkD x))
-> Apply p d
elimD sd k = go sd
where
go :: forall a' (d' :: D a').
Sing d' -> Apply p d'
go (SMkD sx) = k sx
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:43:30: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.0.1:
No skolem info:
[a_axS[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
On the other hand, GHC 8.10.4 will produce a proper error message:
$ /opt/ghc/8.10.4/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:43:30: error:
• Expected kind ‘D a1’, but ‘d'’ has kind ‘D a'1’
• In the second argument of ‘Apply’, namely ‘d'’
In the type signature:
go :: forall a' (d' :: D a'). Sing d' -> Apply p d'
In an equation for ‘elimD’:
elimD sd k
= go sd
where
go :: forall a' (d' :: D a'). Sing d' -> Apply p d'
go (SMkD sx) = k sx
• Relevant bindings include
k :: forall (x :: a1). Sing x -> Apply p ('MkD x)
(bound at Bug.hs:40:10)
sd :: Sing d (bound at Bug.hs:40:7)
elimD :: Sing d
-> (forall (x :: a1). Sing x -> Apply p ('MkD x)) -> Apply p d
(bound at Bug.hs:40:1)
|
43 | Sing d' -> Apply p d'
| ^^
Bug.hs:44:22: error:
• Could not deduce: x ~~ x0
from the context: d' ~ 'MkD x
bound by a pattern with constructor:
SMkD :: forall a (x :: a). Sing x -> SD ('MkD x),
in an equation for ‘go’
at Bug.hs:44:9-15
‘x’ is a rigid type variable bound by
a pattern with constructor:
SMkD :: forall a (x :: a). Sing x -> SD ('MkD x),
in an equation for ‘go’
at Bug.hs:44:9-15
Expected type: Sing x0
Actual type: Sing x
• In the first argument of ‘k’, namely ‘sx’
In the expression: k sx
In an equation for ‘go’: go (SMkD sx) = k sx
• Relevant bindings include
sx :: Sing x (bound at Bug.hs:44:14)
go :: Sing d' -> Apply p d' (bound at Bug.hs:44:5)
k :: forall (x :: a1). Sing x -> Apply p ('MkD x)
(bound at Bug.hs:40:10)
sd :: Sing d (bound at Bug.hs:40:7)
elimD :: Sing d
-> (forall (x :: a1). Sing x -> Apply p ('MkD x)) -> Apply p d
(bound at Bug.hs:40:1)
|
44 | go (SMkD sx) = k sx
| ^^