How can I find the predecessor of a Natural with type-level parity checking?

Question

I've been working with natural numbers with additional type-level parity information. succ has been successfully implemented in the most straightforward way:

succ :: Natural p -> Natural (Opp p)
succ = Succ

However, I'm still struggling with getting pred to typecheck. A minimal example:

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

data Parity = Even | Odd

type family Opp (p :: Parity) = (r :: Parity) | r -> p where
  Opp 'Odd = 'Even
  Opp 'Even = 'Odd

data Natural :: Parity -> * where
  Zero :: Natural 'Even
  Succ :: Natural p -> Natural (Opp p)

pred :: Natural (Opp p) -> Natural p
pred (Succ n) = n

What can I do to successfully implement pred? Right now I'm getting many different large and complicated type errors, especially could not deduce Opp p ~ p1.

Answer 1

As @chi indicated,

Injectivity annotations are not exploited by GHC for anything except for allowing some types that would be otherwise considered ambiguous. Only for that. They are not used, as one would expect, to infer a ~ b from F a ~ F b. Personally, I consider them to be nearly useless, in their current form.

So you have to define Natural a bit differently:

data Natural :: Parity -> * where
  Zero :: Natural 'Even
  Succ :: (p ~ Opp s, s ~ Opp p) => Natural p -> Natural s

Now you can get both of the things you need.

Answer 2

Given singletons for Parity:

data SParity :: Parity -> Type where
  SEven :: SParity Even
  SOdd :: SParity Odd

We can prove the injectivity of Opp

oppInj' :: Opp p ~ Opp q => SParity p -> SParity q -> p :~: q
oppInj' SEven SEven = Refl
oppInj' SOdd SOdd = Refl

Now we can define:

data Natural' :: Parity -> Type where
  Zero' :: Natural' Even
  Succ' :: SParity p -> Natural' p -> Natural' (Opp p)
pred' :: SParity p -> Natural' (Opp p) -> Natural' p
pred' p (Succ' q n) = case oppInj' p q of Refl -> n

You may safely perform erasure to get rid of all the singleton junk:

-- for maximum symmetry, instead of relying on type applications we could
-- just substitute Proxy# in place of SParity everywhere, but meh
oppInj :: forall p q. Opp p ~ Opp q => p :~: q
oppInj = unsafeCoerce Refl -- we know this is OK because oppInj' exists
data Natural :: Parity -> Type where
  Zero :: Natural Even
  Succ :: Natural p -> Natural (Opp p)
pred :: forall p. Natural (Opp p) -> Natural p
pred (Succ (n :: Natural q)) = case oppInj @p @q of Refl -> n

This pattern, doing something with singletons and then erasing them for an improvement in space and time (here it's just a constant factor) is common when doing dependently typed programming in Haskell. Normally, you wouldn't write Natural' or pred', but they are useful as guides for writing the erased versions.

PS: Make sure to handle the Zero case!