How to read this "proof" GHC Core?

Question

I wrote this little part of Haskell to find out how the GHC proves that for natural numbers you can only halve:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-} module Nat where data Nat = Z | S Nat data Parity = Even | Odd type family Flip (x :: Parity) :: Parity where Flip Even = Odd Flip Odd = Even data ParNat :: Parity -> * where PZ :: ParNat Even PS :: (x ~ Flip y, y ~ Flip x) => ParNat x -> ParNat (Flip x) halve :: ParNat Even -> Nat halve PZ = Z halve (PS a) = helper a where helper :: ParNat Odd -> Nat helper (PS b) = S (halve b) 

The corresponding parts of the kernel will become:

 Nat.$WPZ :: Nat.ParNat 'Nat.Even Nat.$WPZ = Nat.PZ @ 'Nat.Even @~ <'Nat.Even>_N Nat.$WPS :: forall (x_apH :: Nat.Parity) (y_apI :: Nat.Parity). (x_apH ~ Nat.Flip y_apI, y_apI ~ Nat.Flip x_apH) => Nat.ParNat x_apH -> Nat.ParNat (Nat.Flip x_apH) Nat.$WPS = \ (@ (x_apH :: Nat.Parity)) (@ (y_apI :: Nat.Parity)) (dt_aqR :: x_apH ~ Nat.Flip y_apI) (dt_aqS :: y_apI ~ Nat.Flip x_apH) (dt_aqT :: Nat.ParNat x_apH) -> case dt_aqR of _ { GHC.Types.Eq# dt_aqU -> case dt_aqS of _ { GHC.Types.Eq# dt_aqV -> Nat.PS @ (Nat.Flip x_apH) @ x_apH @ y_apI @~ <Nat.Flip x_apH>_N @~ dt_aqU @~ dt_aqV dt_aqT } } Rec { Nat.halve :: Nat.ParNat 'Nat.Even -> Nat.Nat Nat.halve = \ (ds_dJB :: Nat.ParNat 'Nat.Even) -> case ds_dJB of _ { Nat.PZ dt_dKD -> Nat.Z; Nat.PS @ x_aIX @ y_aIY dt_dK6 dt1_dK7 dt2_dK8 a_apK -> case a_apK `cast` ((Nat.ParNat (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N ; Nat.TFCo:R:Flip[0]))_R :: Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd) of _ { Nat.PS @ x1_aJ4 @ y1_aJ5 dt3_dKa dt4_dKb dt5_dKc b_apM -> Nat.S (Nat.halve (b_apM `cast` ((Nat.ParNat (dt4_dKb ; (Nat.Flip (dt5_dKc ; Sym dt3_dKa ; Sym Nat.TFCo:R:Flip[0] ; (Nat.Flip (dt_dK6 ; Sym dt2_dK8))_N ; Sym dt1_dK7))_N ; Sym dt_dK6))_R :: Nat.ParNat x1_aJ4 ~# Nat.ParNat 'Nat.Even))) } } end Rec } 

I know the general flow of type casting through instances of the Flip type family, but there are some things that I cannot fully accomplish:

• What is the value of @~ <Nat.Flip x_apH>_N ? is it a flip instance for x? How is this different from @ (Nat.Flip x_apH) ? I'm interested in < > and _N

Regarding the first actor in halve :

• What do dt_dK6 , dt1_dK7 and dt2_dK8 ? I understand that this is some evidence of equivalence, but what is it?
• I understand that Sym runs back equivalence
• What does ; ? Is the proof of equivalence sufficiently applied?
• What are the suffixes _N and _R ?
• Are there any TFCo:R:Flip[0] and TFCo:R:Flip[1] instances of Flip?

Answer 1

@~ is a coercion application.

Angle brackets denote the reflexive compulsion of their contained type with the role indicated by the underlined letter.

Thus, <Nat.Flip x_ap0H>_N is a proof of equality that Nat.Flip x_apH is equal to the value of Nat.Flip x_apH (as equal types of not only equal representations).

PS has a lot of arguments. We look at the $WPS smart constructor, and we see that the first two are types x and y respectively. We have evidence that the argument to the constructor is Flip x (in this case, we have Flip x ~ Even . Then we have the proofs x ~ Flip y and y ~ Flip x . The final argument is the value ParNat x .

Now I will pass the first class of type Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

Let's start with (Nat.ParNat ...)_R This is a type constructor application. He raises the proof x_aIX ~# 'Nat.Odd to Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd . R means that this means that it means that the types are isomorphic but not the same (in this case they are the same, but we do not need this knowledge to perform the translation).

Now we consider the main part of the proof (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) . ; means transitivity, that is, apply this evidence in order.

dt1_dK7 is proof x_aIX ~# Nat.Flip y_aIY .

If we look at (dt2_dK8 ; Sym dt_dK6) . dt2_dK8 shows y_aIY ~# Nat.Flip x_aIX . dt_dK6 is of type 'Nat.Even ~# Nat.Flip x_aIX . So, Sym dt_dK6 is of type Nat.Flip x_aIX ~# 'Nat.Even and (dt2_dK8 ; Sym dt_dK6) is of type y_aIY ~# 'Nat.Even

Thus, (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N is proof that Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even .

Nat.TFCo:R:Flip[0] is the first flip rule, which is Nat.Flip 'Nat.Even ~# 'Nat.Odd' .

Putting them together, we get (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) has type x_aIX #~ 'Nat.Odd .

The second more complex composition is a little more difficult to develop, but should work on the same principle.