type-level-add.hs

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits

data V (n::Nat) = V
  deriving Show


type family Add (x :: Nat) (y :: Nat) :: Nat where
  Add x y = x+y

add :: (KnownNat n, KnownNat m) => V n -> V m -> V (Add n m)
add _ _ = V

eq' :: (KnownNat n) => V n -> V n -> V n
eq' a _ = a


main = do
  let v1 = V :: V 1
      v2 = V :: V 2
      v3 = V :: V 3
  print $ natVal $ add v1 v2
  print $ natVal $ eq' (add v1 v2) v3