{-# LANGUAGE RankNTypes, TypeOperators, TypeFamilies, ScopedTypeVariables, FlexibleContexts, UndecidableInstances, FlexibleInstances, EmptyDataDecls, GADTs #-}
module Data.Nat where

import Unsafe.Coerce

-- Adapted from Ryan Ingram's http://www.mail-archive.com/haskell-cafe@haskell.org/msg60806.html

newtype I x   = I { unI :: x }
newtype K x y = K { unK :: x }

-- Same representation, can be coerced at no cost. Probably buys us nothing though, as we must add to maintain invariants.
data Z  
data S n 

newtype Nat n = Nat Int

instance Show (Nat n) where
  show = show . natToInt

z :: Nat Z
z = Nat 0

s :: Nat n -> Nat (S n)
s (Nat n) = Nat (n + 1)

natToInt :: Nat n -> Int
natToInt (Nat i) = i

data Reifiable n where
  Proof :: Reify n => Reifiable n

data Exists = forall n. Ex !(Reifiable n)

reifiable :: Nat n -> Reifiable n
reifiable (Nat i) = case aux i (Ex . proof) of
                        Ex p -> unsafeCoerce p
  where
    proof :: Reify n => n -> Reifiable n
    proof _ = Proof
    aux :: Int -> (forall n. Reify n => n -> r) -> r
    aux i k = undefined
                  
class Reify n where
  witnessNat :: Nat n
instance Reify Z where
  witnessNat = z
instance Reify n => Reify (S n) where
  witnessNat = s (witnessNat)

type family (:+:) a b :: *
type instance (:+:) Z n = n
type instance (:+:) (S m) n = S (m :+: n)

type family (:*:) a b :: *
type instance (:*:) Z n = Z
type instance (:*:) (S m) n = n :+: (m :*: n)

addNat :: Nat a -> Nat b -> Nat (a :+: b)
addNat (Nat a) (Nat b) = Nat (a + b)

mulNat :: Nat a -> Nat b -> Nat (a :*: b)
mulNat a b = Nat (natToInt a * natToInt b)


data NatView n where
  Zero :: NatView Z
  Succ :: Nat n -> NatView (S n)
  

view :: Nat n -> NatView n
view (Nat 0) = unsafeCoerce Zero
view (Nat (n+1)) = unsafeCoerce (Succ (Nat n))