GHC HEAD-only panic (buildKindCoercion)
The following program compiles without issue on GHC 8.6.3:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Type.Bool (type (&&))
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: forall k. k -> Type
data instance Sing :: Bool -> Type where
SFalse :: Sing False
STrue :: Sing True
(%&&) :: forall (x :: Bool) (y :: Bool).
Sing x -> Sing y -> Sing (x && y)
SFalse %&& _ = SFalse
STrue %&& a = a
data RegExp :: Type -> Type where
App :: RegExp t -> RegExp t -> RegExp t
data instance Sing :: forall t. RegExp t -> Type where
SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
type instance Apply ReNotEmptySym0 r = ReNotEmpty r
type family ReNotEmpty (r :: RegExp t) :: Bool where
ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
sReNotEmpty :: forall t (r :: RegExp t).
Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
blah :: forall (t :: Type) (re :: RegExp t).
Sing re -> ()
blah (SApp sre1 sre2)
= case (sReNotEmpty sre1, sReNotEmpty sre2) of
(STrue, STrue) -> ()
However, it panics on GHC HEAD:
$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20190114 for x86_64-unknown-linux):
buildKindCoercion
Any
ReNotEmpty re2_a1hm
Bool
t_a1hg
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion
Trac metadata
Trac field | Value |
---|---|
Version | 8.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | highest |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |