Congruence of Type Level Nats in Haskell

Question

I am trying to implement a version of Braun Tree in Haskell, which requires me to prove this fact about Nats

If n :~: m, then n + 1 :~: m + 1

However, I am failing to fill the undefined below. I tried Refl, but the type system complains.

import GHC.TypeLits
import Data.Type.Equality

sucCong :: ((p :: Nat) :~: (q :: Nat)) -> (p + 1 :: Nat) :~: (q + 1 :: Nat)
sucCong proof = undefined

How do I prove this?

Answer 1

Pattern-match on the proof to make its statement available to the constraint solver. Then there is only one constructor for the type (:~:) so there's not much choice in the rest of the definition anyway.

sucCong :: (p :~: q) -> (p+1) :~: (q+1)
sucCong Refl = Refl