Runtime type-level naturals

TypeNats.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

data Nat
  = Zero
  | Succ Nat

data SingNat n where
  SZero :: SingNat 'Zero
  SSucc :: SingNat n -> SingNat ('Succ n)

instance TestEquality SingNat where
  testEquality SZero SZero = Just Refl
  testEquality (SSucc n) (SSucc m) =
    case testEquality n m of
      Just Refl -> Just Refl
      _ -> Nothing
  testEquality _ _ = Nothing

data SomeNat where
  SomeNat :: SingNat n -> SomeNat

toSomeNat :: Int -> SomeNat
toSomeNat 0 = SomeNat SZero
toSomeNat n =
  case toSomeNat $ n - 1 of
    SomeNat m -> SomeNat $ SSucc m

instance Eq SomeNat where
  SomeNat n == SomeNat m =
    case testEquality n m of
      Just Refl -> True
      _ -> False