Behavior of type level naturals in GHC 7.8

Question

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?

Answer 1

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.

Answer 2

The GHC 7.8 solver still won't solve for a lot of arithmetic relations with type naturals. Though in this case it's perfectly safe to use unsafeCoerce to force GHC to recognize the intended type.

{-# LANGUAGE
  DataKinds, GADTs, TypeOperators, TypeFamilies, StandaloneDeriving
  #-}

import GHC.TypeLits
import Unsafe.Coerce

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        = unsafeCoerce y
concatV (x :> xs) y = unsafeCoerce $ x :> concatV xs y