Core Lint error (From-kind of Cast differs from kind of enclosed type) with TH-generated data type
The following program will produce a Core Lint error when compiled:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind (Constraint, Type)
import Language.Haskell.TH hiding (Type)
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type SameKind :: k -> k -> Constraint
type SameKind a b = ()
type Const :: Type -> Type -> Type
type family Const x y where
Const x _ = x
type Wat :: forall (x :: Type) -> Const Type x -> Type -> Const Type x
type Wat x y z = Bool
{-
data WatSym2 (x :: Type) (y :: Const Type x) :: (~>) Type (Const Type x)
where
WatSym2KindInference :: forall x y z f.
SameKind (Apply (WatSym2 x y) z) (Wat x y z) =>
WatSym2 x y f
-}
$(do let watSym2 = mkName "WatSym2"
watSym2KindInference = mkName "WatSym2KindInference"
x <- newName "x"
y <- newName "y"
z <- newName "z"
f <- newName "f"
let d = DataD [] watSym2 [ kindedTV x (ConT ''Type), kindedTV y (ConT ''Const `AppT` ConT ''Type `AppT` VarT x) ]
(Just (InfixT (ConT ''Type) ''(~>) (ConT ''Const `AppT` ConT ''Type `AppT` VarT x)))
[ ForallC [ PlainTV x SpecifiedSpec
, PlainTV y SpecifiedSpec
-- , KindedTV y SpecifiedSpec (ConT ''Const `AppT` ConT ''Type `AppT` VarT x)
, PlainTV z SpecifiedSpec
, PlainTV f SpecifiedSpec
]
[ConT ''SameKind `AppT` (ConT ''Apply `AppT` (ConT watSym2 `AppT` VarT x `AppT` VarT y) `AppT` VarT z)
`AppT` (ConT ''Wat `AppT` VarT x `AppT` VarT y `AppT` VarT z)]
(GadtC [watSym2KindInference] [] (ConT watSym2 `AppT` VarT x `AppT` VarT y `AppT` VarT f))
]
[]
pure [d])$ /opt/ghc/9.0.1/bin/ghc Bug.hs -dcore-lint -dno-typeable-binds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
*** Core Lint errors : in result of CorePrep ***
Bug.hs:43:2: warning:
From-kind of Cast differs from kind of enclosed type
From-kind: Const (*) x_a30I
Kind of enclosed type: *
Actual enclosed type: y_a30J
Coercion used in cast: Sym (D:R:Const[0] <*>_N <x_a30I>_N)
In the type of a binder: WatSym2KindInference
In the type ‘forall {x} {y :: Const (*) x}
{a :: TyFun (*) (Const (*) x)} {z} {f :: TyFun (*) (*)}.
(y ~# (y |> Sym (D:R:Const[0] <*>_N <x>_N)))
-> (a ~# (f |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x>_N)))_N))
-> SameKind
(Apply
(WatSym2 x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) |> (TyFun
<*>_N
(D:R:Const[0]
<*>_N <x>_N))_N
%<'Many>_N ->_N <*>_N)
z)
(Wat x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) z |> D:R:Const[0]
<*>_N <x>_N)
-> WatSym2 x y a’
Substitution: [TCvSubst
In scope: InScope {z_X0 f_X1 x_a30I y_a30J a_a31O}
Type env: [X0 :-> z_X0, X1 :-> f_X1, a30I :-> x_a30I,
a30J :-> y_a30J, a31O :-> a_a31O]
Co env: []]
*** Offending Program ***
$WWatSym2KindInference [InlPrag=INLINE[final] CONLIKE]
:: forall x y z (f :: TyFun (*) (*)).
SameKind
(Apply
(WatSym2 x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) |> (TyFun
<*>_N (D:R:Const[0] <*>_N <x>_N))_N
%<'Many>_N ->_N <*>_N)
z)
(Wat x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) z |> D:R:Const[0]
<*>_N <x>_N) =>
WatSym2
x
(y |> Sym (D:R:Const[0] <*>_N <x>_N))
(f |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x>_N)))_N)
[GblId[DataConWrapper],
Arity=1,
Caf=NoCafRefs,
Str=<L,U>,
Unf=OtherCon []]
$WWatSym2KindInference
= \ (@x_a30I)
(@y_a30J)
(@z_X0)
(@(f_X1 :: TyFun (*) (*)))
(dt_s325 [Occ=Once1]
:: SameKind
(Apply
(WatSym2
x_a30I (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)) |> (TyFun
<*>_N
(D:R:Const[0]
<*>_N
<x_a30I>_N))_N
%<'Many>_N ->_N <*>_N)
z_X0)
(Wat
x_a30I
(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
z_X0 |> D:R:Const[0] <*>_N <x_a30I>_N)) ->
WatSym2KindInference
@x_a30I
@(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
@(f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N)
@z_X0
@f_X1
@~(<(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))>_N
:: (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
~# (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)))
@~(<(f_X1 |> (TyFun
<*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N)>_N
:: (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N)
~# (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N))
dt_s325
WatSym2KindInference [InlPrag=NOUSERINLINE CONLIKE]
:: forall {x} {y :: Const (*) x} {a :: TyFun (*) (Const (*) x)} {z}
{f :: TyFun (*) (*)}.
(y ~# (y |> Sym (D:R:Const[0] <*>_N <x>_N)))
-> (a ~# (f |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x>_N)))_N))
-> SameKind
(Apply
(WatSym2 x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) |> (TyFun
<*>_N
(D:R:Const[0] <*>_N <x>_N))_N
%<'Many>_N ->_N <*>_N)
z)
(Wat x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) z |> D:R:Const[0]
<*>_N <x>_N)
-> WatSym2 x y a
[GblId[DataCon], Arity=3, Caf=NoCafRefs, Unf=OtherCon []]
WatSym2KindInference
= \ (@x_a30I)
(@(y_a30J :: Const (*) x_a30I))
(@(a_a31O :: TyFun (*) (Const (*) x_a30I)))
(@z_X0)
(@(f_X1 :: TyFun (*) (*)))
(eta_B0
:: y_a30J ~# (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)))
(eta_B1
:: a_a31O
~# (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N))
(eta_B2 [Occ=Once1]
:: SameKind
(Apply
(WatSym2
x_a30I (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)) |> (TyFun
<*>_N
(D:R:Const[0]
<*>_N
<x_a30I>_N))_N
%<'Many>_N ->_N <*>_N)
z_X0)
(Wat
x_a30I
(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
z_X0 |> D:R:Const[0] <*>_N <x_a30I>_N)) ->
WatSym2KindInference
@x_a30I
@y_a30J
@a_a31O
@z_X0
@f_X1
@~(eta_B0
:: y_a30J ~# (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)))
@~(eta_B1
:: a_a31O
~# (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N))
eta_B2
*** End of Offense ***
<no location info>: error:
Compilation had errorsCuriously, the Core Lint error goes away if you do either of the following:
- Replace the Template Haskell–generated version of
WatSym2with the hand-written version that is commented-out above. - Replace the
, PlainTV y SpecifiedSpecline with the, KindedTV y SpecifiedSpec (ConT ''ConstAppTConT ''TypeAppTVarT x)line below it that is commented out.
Because Template Haskell appears to be critical to triggering this bug, I suspect that this may be related to #11812 or #17537. The error here is different than what is seen in those issues, however, so to be on the safe side, I decided to open a dedicated issue for this.