--module Singletons where

{-# LANGUAGE TemplateHaskell, PolyKinds, DataKinds, TypeFamilies,
             ScopedTypeVariables, GADTs, StandaloneDeriving, RankNTypes,
             TypeOperators #-}

import Data.Singletons.TH
import Unsafe.Coerce    -- don't hate me yet! keep reading!

data Nat_ = Zero_ | Succ_ Nat_
data SNat_ :: Nat_ -> * where
  SZero_ :: SNat_ Zero_
  SSucc_ :: SNat_ n -> SNat_ (Succ_ n)

plus_ :: Nat_ -> Nat_ -> Nat_
plus_ Zero_     n = n
plus_ (Succ_ m) n = Succ_ (plus_ m n)

type family Plus_ (m :: Nat_) (n :: Nat_) :: Nat_
type instance Plus_ Zero_     n = n
type instance Plus_ (Succ_ m) n = Succ_ (Plus_ m n)

sPlus_ :: SNat_ m -> SNat_ n -> SNat_ (Plus_ m n)
sPlus_ SZero_     n = n
sPlus_ (SSucc_ m) n = SSucc_ (sPlus_ m n)

class SingI (a :: k) where
  sing :: Sing a
