haskell - ユーザー定義の種類でインデックス付けされたデータ型に一致するパターンに含まれるキャストを理解する

Question

それで、私は Haskell で遊んでいてDataKinds、TypeFamilies生成されたコア GHC を見始めました。

これが私の質問の動機となる小さなテストケースです。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module TestCase where

data Ty = TyBool | TyInt

type family InterpTy (t :: Ty) :: *
type instance InterpTy TyBool = Bool
type instance InterpTy TyInt  = Int

data Expr (a :: Ty) where
  I :: Int  -> Expr TyInt
  B :: Bool -> Expr TyBool

eval :: Expr a -> InterpTy a
eval (I i) = i
eval (B b) = b

eval関数用に生成されたコアを見てみましょう。

TestCase.eval =
  \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) ->
    case ds_dL3 of _ [Occ=Dead] {
      TestCase.I dt_dLh i_as6 ->
        i_as6
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
                ; (TestCase.InterpTy (Sym dt_dLh))_R
                :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);
      TestCase.B dt_dLc b_as7 ->
        b_as7
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0])
                ; (TestCase.InterpTy (Sym dt_dLc))_R
                :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM)
    }

a明らかに、特定のブランチに何があり得るかについての情報を持ち歩く必要があります。Datakind のインデックスを作成せず、TypeFamilies を使用しない場合、キャストははるかに理解しやすくなります。

次のようになります。

Main.eval =
  \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) ->
    case ds_d1sQ of _ [Occ=Dead] {
      Main.I' dt_d1to i_aFa ->
        i_aFa
        `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg);
      Main.B' dt_d1tk b_aFb ->
        b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg)
    }

これは完全に理解できますが、TypeFamiliesこの例で問題になるのは次の部分です。

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
      ; (TestCase.InterpTy (Sym dt_dLh))_R
      :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);

2行目は本当に私を混乱させるものです。そこでセミコロンは何をしているのですか？ここでは少し場違いに思えますか、それとも何か不足していますか? これについて読むことができる場所はありますか（お勧めできる書類があれば喜んで受け取ります）

敬具、

雷鳥