concatenate personalizzati definiti vettore

Question

Ho definito un vettore come tale:

{-# 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 

e sto cercando di fare un vectorConcat, come ad esempio:

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

Tuttavia, quando si cerca di fare questo:

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) 

Ho il seguente errore e non sono sicuro di come risolverlo:

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' 

Sono stato bloccato su questo per un po ', e mi chiedevo se potevo ottenere qualsiasi direzione.

Answer 1

GHC in realtà non conosce molti fatti sull'aritmetica, e in particolare (in questo caso) non sa che l'addizione è commutativa. Non è neanche facile insegnare questo fatto a GHC.

Tuttavia, in questo caso specifico, si può semplicemente commutare i termini nella definizione di (*) a mano, e poi le cose compilare bene:

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