Skip to content

GitLab

Closed
Created by Ryan Scott@RyanGlScottMaintainer

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 42

Click 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 errors

And 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 errors

That'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:RepType

The 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 kind

This 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 kind

Unfortunately, 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 'Red

The 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# -> Quux

Then 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:RepType

This 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?