{-# LANGUAGE RankNTypes   #-}
{-# LANGUAGE TypeFamilies #-}

module Phantom where

data Zero
data Succ n

type One   = Succ  Zero
type Two   = Succ  One
type Four  = Succ (Succ Two )
type Six   = Succ (Succ Four)
type Eight = Succ (Succ Six )

class Nat n where
    toInt :: n -> Int
instance Nat Zero where
    toInt _ = 0
instance (Nat n) => Nat (Succ n) where
    toInt _ = 1 + toInt (undefined :: n)

newtype Pointer n = MkPointer Int
newtype Offset  n = MkOffset  Int

multiple :: forall n. (Nat n) => Int -> Offset n
multiple i = MkOffset (i * toInt (undefined :: n))

add :: Pointer m -> Offset n -> Pointer (GCD Zero m n)
add (MkPointer x) (MkOffset y) = MkPointer (x + y)

fetch32 :: (GCD Zero n Four ~ Four) => Pointer n -> IO ()
fetch32 = undefined

type family   GCD  d        m        n
type instance GCD  d        Zero     Zero    = d
type instance GCD  d       (Succ m) (Succ n) = GCD (Succ d) m n
type instance GCD  Zero    (Succ m)  Zero    = Succ m
type instance GCD (Succ d) (Succ m)  Zero    = GCD One d m
type instance GCD  Zero     Zero    (Succ n) = Succ n
type instance GCD (Succ d)  Zero    (Succ n) = GCD One d n