SingNat.hs

{-# LANGUAGE DataKinds, GADTs, PatternSynonyms, PolyKinds, ScopedTypeVariables, TypeFamilies, ViewPatterns #-}
module SingNat where

import Unsafe.Coerce

data Nat = Z | S Nat

data family Sing (a :: k)

newtype instance Sing (a :: Nat) = SingNat Int

data IsSingNat (a :: Nat) where
  IsSZ :: IsSingNat Z
  IsSS :: Sing n -> IsSingNat (S n)

isSingNat :: Sing n -> IsSingNat n
isSingNat (SingNat 0) = unsafeCoerce IsSZ
isSingNat (SingNat n) = unsafeCoerce IsSS (SingNat (n - 1))

pattern SZ :: forall (n :: Nat) . () => (n ~ Z) => Sing n
pattern SZ <- (isSingNat -> IsSZ)
  where
    SZ = SingNat 0

pattern SS :: forall (n :: Nat) . () => forall (n' :: Nat) . (n ~ S n') => Sing n' -> Sing n
pattern SS n <- (isSingNat -> IsSS n)
  where
    SS (SingNat n) = SingNat (n + 1)
~