Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,865
    • Issues 4,865
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 455
    • Merge requests 455
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19743
Closed
Open
Created Apr 25, 2021 by Ryan Scott@RyanGlScottMaintainer

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.

Edited Apr 25, 2021 by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking