Opened 3 months ago
Closed 3 months ago
#15343 closed bug (fixed)
Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | high | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | TypeInType | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | dependent/should_fail/T15343 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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 | ^^^^^^^^
Change History (8)
comment:1 Changed 3 months ago by
comment:2 Changed 3 months ago by
Cc: | goldfire added |
---|
This started panicking in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.)
comment:3 Changed 3 months ago by
Simplification:
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind elimSing :: forall (p :: forall z. z). p elimSing = undefined data WhySym :: Type -> Type hsym = elimSing @WhySym
comment:7 Changed 3 months ago by
Status: | new → merge |
---|---|
Test Case: | → dependent/should_fail/T15343 |
I'd like Richard to check these patches, if he has time, but they are outright bugs and should probably move to the branch
comment:8 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Comment:5 merged in 5b10d537bde8e1c1cf5e0359d38dac7351ae8b2a. Comment:6 merged in cfc4afad16d0eb99d5576cd998bcf473a1bc2af5.
Here's a smaller example: