Understanding the casts involved in patterns matching a datatype that is indexed over a user defined kind

Question

So, I was playing around with DataKinds and TypeFamilies in Haskell and started to look at the Core GHC generated.

Here is a little TestCase to motivate my question:

{-# 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

Let's take a look at the generated Core for the eval function

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)
    }

Obviously we need to carry around information about what a 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.

It would be something like this:

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)
    }

This I can understand perfectly well, what troubles me in the TypeFamilies example is this part:

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

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)

Kind regards,

raichoo

Answer 1

The semicolon is syntax for transitivity of coercions.

The latest (as of September 2014) paper about System FC is "Safe Zero-Cost Coercions in Haskell" from ICFP 2014.

In particular, in Figure 3 of that paper we see the syntax of coercions. "γ₁;γ₂" is coercion transitivity. If γ₁ is a coercion that witnesses that "τ₁ ~ τ₂" and γ₂ is a coercion that witnesses that τ₂ ~ τ₃ then "γ₁;γ₂" is a coercion that witnesses τ₁ ~ τ₃.

In the example, when you write eval (I i) = i what the compiler sees on the right hand side is a value of type Int, and what it needs (from the return type of the function) is something of InterpTy a. So now it needs to construct a proof that Int ~ InterpTy a.

Informally, (reading from right to left and ignoring roles - for the details of which see the linked paper):

1. From doing the GADT pattern match we learn that "a ~ Int" (that's dt_dLh)
2. So we apply Sym to it, to get "Int ~ a".
3. Then apply the InterpTy family to get "InterpTy Int ~ InterpTy a" (this is an instance of /congruence/)
4. Then we compose that transitively with "Sym InterpTyTyInt" (which is the flipped version of the axiom that states that "InterpTy TyInt ~ Int") to get the coercion we're after: "Int ~ InterpTy a"