I am trying to tag canonical Nat datatype with (Even/Odd) Parity kind to see if we can get any free theorems. Here is the code:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
-- Use DataKind promotion with type function for even-odd
module EvenOdd where
data Parity = Even | Odd
-- Parity is promoted to kind level Parity.
-- Even & Odd to type level 'Even & 'Odd of kind Parity
-- We define type-function opp to establish the relation that
-- type 'Even is opposite of 'Odd, and vice-versa
type family Opp (n :: Parity) :: Parity
type instance Opp 'Even = 'Odd
type instance Opp 'Odd = 'Even
-- We tag natural number with the type of its parity
data Nat :: Parity -> * where
Zero :: Nat 'Even
Succ :: Nat p -> Nat (Opp p)
-- Now we (should) get free theorems.
-- 1. Plus of two even numbers is even
evenPlus :: Nat 'Even -> Nat 'Even -> Nat 'Even
evenPlus Zero n2 = n2 -- Line 31
evenPlus (Succ (Succ n1)) n2 = Succ (Succ (evenPlus n1 n2))
However, GHC throws type error:
Could not deduce (p1 ~ 'Even)
from the context ('Even ~ Opp p)
bound by a pattern with constructor
Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
in an equation for `evenPlus'
at even-odd.hs:31:13-26
or from (p ~ Opp p1)
bound by a pattern with constructor
Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
in an equation for `evenPlus'
at even-odd.hs:31:19-25
`p1' is a rigid type variable bound by
a pattern with constructor
Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
in an equation for `evenPlus'
at even-odd.hs:31:19
Expected type: Nat 'Even
Actual type: Nat p
In the first argument of `evenPlus', namely `n1'
In the first argument of `Succ', namely `(evenPlus n1 n2)'
As I understand it, the gist of the above error is that GHC was unable to deduce (p1 ~ 'Even), when the context has the equation: ((Opp (Opp p1)) ~ 'Even).
Why does this happen? Is there something wrong with my approach?