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 errors

Curiously, the Core Lint error goes away if you do either of the following:

1. Replace the Template Haskell–generated version of WatSym2 with the hand-written version that is commented-out above.
2. Replace the , PlainTV y SpecifiedSpec line with the , KindedTV y SpecifiedSpec (ConT ''Const AppTConT ''TypeAppT VarT 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.