title: Understanding the casts involved in patterns matching a datatype that is indexed over a user defined kind
body: <p>So, I was playing around with <code>DataKinds</code> and <code>TypeFamilies</code> in Haskell and started to look at the Core GHC generated.</p>
  
  <p>Here is a little TestCase to motivate my question:</p>
  
  <pre><code>{-# 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  -&gt; Expr TyInt
    B :: Bool -&gt; Expr TyBool
  
  eval :: Expr a -&gt; InterpTy a
  eval (I i) = i
  eval (B b) = b
  </code></pre>
  
  <p>Let's take a look at the generated Core for the <code>eval</code> function</p>
  
  <pre><code>TestCase.eval =
    \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) -&gt;
      case ds_dL3 of _ [Occ=Dead] {
        TestCase.I dt_dLh i_as6 -&gt;
          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 -&gt;
          b_as7
          `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0])
                  ; (TestCase.InterpTy (Sym dt_dLc))_R
                  :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM)
      }
  </code></pre>
  
  <p>Obviously we need to carry around information about what <code>a</code> could be in the specific branch. If I don't indexing over a Datakind and would not use TypeFamilies the cast is a lot easier to understand.</p>
  
  <p>It would be something like this:</p>
  
  <pre><code>Main.eval =
    \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) -&gt;
      case ds_d1sQ of _ [Occ=Dead] {
        Main.I' dt_d1to i_aFa -&gt;
          i_aFa
          `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg);
        Main.B' dt_d1tk b_aFb -&gt;
          b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg)
      }
  </code></pre>
  
  <p>This I can understand perfectly well, what troubles me in the <code>TypeFamilies</code> example is this part:</p>
  
  <pre><code>(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
        ; (TestCase.InterpTy (Sym dt_dLh))_R
        :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);
  </code></pre>
  
  <p>The second line is what really confuses me. What is the semicolon doing there? It seems a bit out of place here or am I missing something? Is there a place where I can read up on this (I gladly take papers if you can recommend one)</p>
  
  <p>Kind regards,</p>
  
  <p>raichoo</p>