Nat.hs

{-# LANGUAGE TypeFamilies, UndecidableInstances, KindSignatures, DataKinds, TypeOperators, GADTs, RankNTypes, PolyKinds #-}

import Data.Kind
import Data.Type.Equality

data Nat = Z | S Nat

data SNat :: Nat -> Type where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

type family Plus n m where
  Plus Z m = m
  Plus (S n) m = S (Plus n m)

plus_Z :: SNat n -> Plus n Z :~: n
plus_Z SZ = Refl
plus_Z (SS n) | Refl <- plus_Z n = Refl

plus_succ :: SNat n -> SNat m -> S (Plus n m) :~: Plus n (S m)
plus_succ SZ _ = Refl
plus_succ (SS n) m | Refl <- plus_succ n m = Refl

plus_comm :: SNat n -> SNat m -> Plus n m :~: Plus m n
plus_comm SZ m | Refl <- plus_Z m = Refl
plus_comm (SS n) m | Refl <- plus_comm n m
                   , Refl <- plus_succ m n
                   = Refl