GitLab

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