Behavior of type level naturals in GHC 7.8
haskell, type-level-computation, types
Solution
Type-level naturals still don't really do computation yet. GHC 7.10 is slated to have an SMT solver integrated to finally handle everything you think it should be able to.
As a theoretically unsound but working answer to your actual question - `unsafeCoerce` exists for the case when you know two expressions have the same type, but the compiler doesn't.
Problem
If you want vectors indexed by their length you can do something like this: ``` {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies, StandaloneDeriving #-} data N = P N | Z type family Add (n :: N) (m :: N) :: N type instance Add Z a = a type instance Add (P a) b = P (Add a b) infixr 5 :> data Vect n a where V0 :: Vect Z a (:>) :: a -> Vect n a -> Vect (P n) a deriving instance Show a => Show (Vect n a) concatV :: Vect n a -> Vect m a -> Vect (Add n m) a concatV V0 y = y concatV (x :> xs) y = x :> concatV xs y ``` In ghc 7.8 I was hoping this would become obsolete with the new type literals, but the direct conversion is invalid: ``` {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies, StandaloneDeriving #-} import GHC.TypeLits infixr 5 :> data Vect (n :: Nat) a where V0 :: Vect 0 a (:>) :: a -> Vect n a -> Vect (n+1) a deriving instance Show a => Show (Vect n a) concatV :: Vect n a -> Vect m a -> Vect (n + m) a concatV V0 y = y concatV (x :> xs) y = x :> concatV xs y ``` Unfortunatley this gives an error: `NB:`+' is a type function, and may not be injective `. I understand why this happens, but since the type literals are compiler magic anyways, I don't know why the compiler could not magic this away either. I tried changing `Vect` : `(:>) :: a -> Vect (n-1) a -> Vect n a`. This way there is an explicit formula for the inner vector, but this gives the error: ``` Couldn't match type `(n + m) - 1' with `(n - 1) + m' Expected type: Vect ((n + m) - 1) a Actual type: Vect ((n - 1) + m) a ``` So now it requires a proof of basic arithmetic. I haven't been able to make either version work. Is there a way to write a proof of `(n + m) - o == (n - o) + m` for the compiler, or somehow make the first version work?