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

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!

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.

How about this slightly different formulation. Notice the change in the position of Opp:

data Parity = Even | Odd

type family Opp (n :: Parity) = (m :: Parity) | m -> n where
    Opp 'Even = 'Odd
    Opp 'Odd  = 'Even

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

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

This makes pred "go with the grain". The compiler doesn't need to "undo" the Opp application, is just "works forward".

But wait, doesn't this shift the problem to the Succ constructor? Actually, yes, if I remove the injectivity annotation, the type of terms like

ghci> Succ (Succ Zero)

fails to be inferred. But why the injectivity annotation wasn't sufficient before, but it is now? I don't know.