GitLab

The following program panics on GHC 8.6 and later:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

data family Sing :: forall k. k -> Type
data SomeSing :: Type -> Type where
  SomeSing :: Sing (a :: k) -> SomeSing k

class SingKind k where
  type Demote k :: Type
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

data instance Sing (z :: a :~~: b) where
  SHRefl :: Sing HRefl

instance SingKind (a :~~: b) where
  type Demote (a :~~: b) = a :~~: b
  fromSing SHRefl = HRefl
  toSing HRefl    = SomeSing SHRefl

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
                   (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
                   (r :: a :~~: b).
            Sing r
         -> Apply p HRefl
         -> Apply p r
(~>:~~:) SHRefl pHRefl = pHRefl

type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
  Why a (_ :: a :~~: y)  = y :~~: a

data    WhySym (a :: j) :: forall   (y :: z). (a :~~: y) ~> Type
-- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
-- The version above does NOT panic
type instance Apply (WhySym a) e = Why a e

hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
        a :~~: b -> b :~~: a
hsym eq = case toSing eq of
            SomeSing (singEq :: Sing r) ->
              (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl

$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180627 for x86_64-unknown-linux):
        coercionKind
  Nth:3
      (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion

As noted in the comments, replacing WhySym with a version that explicitly quantifies z avoids the panic.

This is a regression from GHC 8.4.3, in which the program simply errored:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:56:38: error:
    • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
        but ‘WhySym a’ has kind ‘forall (y :: z0).
                                 TyFun (a1 :~~: y) * -> *’
    • In the type ‘(WhySym a)’
      In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
      In a case alternative:
          SomeSing (singEq :: Sing r)
            -> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
    • Relevant bindings include
        singEq :: Sing a2 (bound at Bug.hs:55:23)
        eq :: a1 :~~: b (bound at Bug.hs:54:6)
        hsym :: (a1 :~~: b) -> b :~~: a1 (bound at Bug.hs:54:1)
   |
56 |               (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
   |                                      ^^^^^^^^

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture