Opened 6 months ago
Closed 2 months ago
#14174 closed bug (fixed)
GHC panic with TypeInType and type family
Reported by: | dfeuer | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.3 |
Component: | Compiler (Type checker) | Version: | 8.2.1 |
Keywords: | TypeInType | Cc: | goldfire, Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | polykinds/T14174.hs, T14174a |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
This rather simple type family,
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-} module GenWhoops where import GHC.Generics type family GenComp k (x :: k) (y :: k) :: Ordering where GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y
produces the following panic:
ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170828 for x86_64-unknown-linux): piResultTy k_a1LK[tau:1] p_a1Lz[sk:1] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type
This happens with both GHC 8.2.1 and something very close to HEAD.
Change History (9)
comment:1 Changed 6 months ago by
comment:2 Changed 6 months ago by
Cc: | Iceland_jack added |
---|
comment:3 Changed 6 months ago by
Here is a simpler way to trigger the same panic
{-# LANGUAGE TypeInType, RankNTypes, KindSignatures, PolyKinds #-} module Foo where data T k (x :: k) = MkT data S x = MkS (T (x Int) x)
comment:4 Changed 4 months ago by
Milestone: | 8.2.2 → 8.2.3 |
---|
It looks like this won't be fixed in 8.2.2.
comment:5 Changed 4 months ago by
This might be another occurrence of this bug:
{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) | (:~>) class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 type family ElimBool (p :: Bool -> Type) (z :: Bool) (pFalse :: p False) (pTrue :: p True) :: p z where -- Commenting out the line below makes the panic go away ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue type family ElimBoolTyFun (p :: Bool ~> Type) (z :: Bool) (pFalse :: p @@ False) (pTrue :: p @@ True) :: p @@ z where ElimBoolTyFun p z pFalse pTrue = ElimBoolPoly (:~>) p z pFalse pTrue type family ElimBoolPoly (arr :: FunArrow) (p :: (Bool -?> Type) arr) (z :: Bool) (pFalse :: App Bool arr Type p False) (pTrue :: App Bool arr Type p True) :: App Bool arr Type p z where ElimBoolPoly _ _ False pFalse _ = pFalse ElimBoolPoly _ _ True _ pTrue = pTrue
$ /opt/ghc/8.2.1/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.2.1 for x86_64-unknown-linux): piResultTy k0_a1Zd[tau:1] z_aS3[sk:1] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:948:35 in ghc:Type
comment:7 Changed 2 months ago by
Test Case: | → polykinds/T14174.hs, T14174a |
---|
Still open because I need to fix the example in comment:5 (which is T14174a
).
comment:9 Changed 2 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
OK, finally fixed I believe. Hurrah.
Note: See
TracTickets for help on using
tickets.
This really should just be an error, I imagine. It's an (accidental) non-linear pattern where the two types have different kinds.