concatenate custom defined vector

Question

I have defined a vector as such:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}
data Nat = Z | S Nat

type family (+) (n :: Nat) (m :: Nat) :: Nat
type instance Z     + m = m
type instance (S n) + m = S (n + m)

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

data Vec (n :: Nat) a where
  VNil  :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a

and am attempting to make a vectorConcat, as such:

vectorConcat :: Vec m (Vec n a) -> Vec (m * n) a

However, when trying to do this:

vectorAppend :: Vec n a -> Vec m a -> Vec (n + m) a
vectorAppend VNil         ys = ys
vectorAppend (VCons x xs) ys = VCons x (vectorAppend xs ys)

vectorConcat :: Vec m (Vec n a) -> Vec (m * n) a
vectorConcat VNil = VNil
vectorConcat (VCons x xs) = vectorAppend x (vectorConcat xs)

I get the following error, and am not sure how to resolve it:

Could not deduce (((n1 * n) + n) ~ (n + (n1 * n)))
from the context (m ~ 'S n1)
  bound by a pattern with constructor
             VCons :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a,
           in an equation for `concatV'

I have been stuck on this for a while, and wondering if I could get any direction.

Answer 1

GHC doesn't really know many facts about arithmetic, and in particular (in this case) doesn't know that addition is commutative. It's not easy to teach GHC this fact, either.

However, in this specific case, you can simply commute the terms in your definition of (*) by hand, and then things compile just fine:

type instance (S n) * m = m + (n * m)