Using type families in data types' return kinds leads to GHC panics and Core Lint errors
Despite #16821 (closed) being fixed, it is still possible to use type families in the return kinds of data types if UnliftedNewtypes is enabled. Moreover, GHC appears to be ill equipped to handle this, as this allows one to construct programs that fail -dcore-lint. Here is one example involving a newtype:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Bug where
import Data.Kind
import GHC.Exts
type family Id (x :: a) :: a where
Id x = x
newtype T :: TYPE (Id LiftedRep) where
MkT :: Int -> T
f :: T
f = MkT 42Click below to see the Core Lint error you get when compiling it:
$ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
Bug.hs:18:1: warning:
[RHS of f :: (T |> (TYPE
(D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N))_N)]
The type of this binder doesn't match the type of its RHS: f
Binder's type: (T |> (TYPE
(D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N))_N)
Rhs type: T
*** Offending Program ***
f :: (T |> (TYPE (D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N))_N)
[LclIdX]
f = (I# 42#) `cast` (Sym (N:T[0]) :: Int ~R# T)
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)
*** End of Offense ***
<no location info>: error:
Compilation had errorsAnd here is another involving a data family:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Bug where
import Data.Kind
import GHC.Exts
type family Id (x :: a) :: a where
Id x = x
data family T :: TYPE (Id LiftedRep)
newtype instance T where
MkT :: Int -> T
f :: T
f = MkT 42$ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:19:1: warning:
[RHS of f :: (T |> (TYPE
(D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N))_N)]
The type of this binder doesn't match the type of its RHS: f
Binder's type: (T |> (TYPE
(D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N))_N)
Rhs type: T
*** Offending Program ***
f_s122 :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
f_s122 = I# 42#
f :: (T |> (TYPE (D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N))_N)
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
f = f_s122 `cast` (Sym (N:R:T[0]) ; Sym (D:R:T0[0]) :: Int ~R# T)
$trModule_s123 :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s123 = "main"#
$trModule_s124 :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s124 = TrNameS $trModule_s123
$trModule_s125 :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s125 = "Bug"#
$trModule_s126 :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s126 = TrNameS $trModule_s125
$trModule :: Module
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
$trModule = Module $trModule_s124 $trModule_s126
*** End of Offense ***
<no location info>: error:
Compilation had errorsThat's not all. If you pick a slightly different example, you can actually get GHC to panic. Here is one such example:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Bug where
import Data.Kind
import GHC.Exts
type family Id (x :: a) :: a where
Id x = x
data family T :: TYPE (Id LiftedRep)
newtype instance T = MkT Int
f :: Int -> T
f = MkT$ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190802:
runtimeRepPrimRep
typePrimRep ((Int |> (TYPE
(Sym (D:R:Id[0] <RuntimeRep>_N <'LiftedRep>_N)))_N) :: TYPE
(Id 'LiftedRep))
Id 'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/simplStg/RepType.hs:525:5 in ghc:RepTypeThe culprit is the fact that TcHsType.checkDataKindSig, which is supposed to ensure that the return kind of a data type/data family declaration is well formed, only invokes tcIsRuntimeTypeKind:
is_TYPE :: Bool
is_TYPE = tcIsRuntimeTypeKind kindThis only checks that the return kind is of the shape TYPE r, but it does not check that r is free of type families.
You might wonder if simply disallowing the use of type families in data type return kinds would suffice to catch this bug. In other words, make the following change:
- is_TYPE = tcIsRuntimeTypeKind kind
+ is_TYPE = tcIsRuntimeTypeKind kind && isTyFamFree kindUnfortunately, things are not that simple. If this change is made, this causes the UnliftedNewtypesDifficultUnification test case (which is supposed to compile) to fail. This is because this test case contains the following declarations:
type family Interpret (x :: Color) :: RuntimeRep where
Interpret 'Red = 'IntRep
Interpret 'Blue = 'WordRep
data family Foo (x :: Color) :: TYPE (Interpret x)
newtype instance Foo 'Red = FooRedC Int#
data family Bar (x :: Color) :: TYPE (Interpret x)
newtype instance Bar 'Red :: TYPE (Lower Int) where
MkBR :: Int# -> Bar 'RedThe fact that this test case ever worked to begin with might be an accident, since if you make a small tweak to it:
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
index de831f9200..121c5515d2 100644
--- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
@@ -18,6 +18,8 @@ type family Interpret (x :: Color) :: RuntimeRep where
data family Foo (x :: Color) :: TYPE (Interpret x)
newtype instance Foo 'Red = FooRedC Int#
+fooRedC :: Int# -> Foo Red
+fooRedC = FooRedC
newtype Quux :: TYPE (Interpret Red) where
MkQ :: Int# -> QuuxThen it begins to panic as described above:
$ ~/Software/ghc3/inplace/bin/ghc-stage2 UnliftedNewtypesDifficultUnification.hs
[1 of 1] Compiling UnliftedNewtypesDifficultUnification ( UnliftedNewtypesDifficultUnification.hs, UnliftedNewtypesDifficultUnification.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190802:
runtimeRepPrimRep
typePrimRep ((Int# |> (TYPE (Sym (D:R:Interpret[0])))_N) :: TYPE
(Interpret 'Red))
Interpret 'Red
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/simplStg/RepType.hs:525:5 in ghc:RepTypeThis leads me to wonder: which forms of data declarations are intended to actually support type families in their return kinds? The conclusion in #16821 (closed) seemed to be that normal data types do not support them. The existence of the UnliftedNewtypesDifficultUnification test case, on the other hand, seems to indicate that data family declarations (as well as data family instances) should support them. If this is true, how can we reconcile this with the problems observed above?