concat-2.idr

sPlusAssoc : (m, n: Nat) -> S (m + n) = plus m (S n)
sPlusAssoc Z     n = refl
sPlusAssoc (S m) n = rewrite sPlusAssoc m n in refl

total concat : Vect n a 
            -> Vect m a 
            -> replace {P = \k => Vect k a} (sPlusAssoc m n) (Vect (m + n) a)
concat (x :: xs) ys = x :: (concat xs ys)
concat nil       ys = ys

error

- + Errors (1)
 `-- tutorial.idr line 16 col 24:
     When elaborating type of snoc.concat:
     When elaborating an application of function replace:
             Can't unify
                     Type
             with
                     (\k => Vect k a) (S (plus m n))
             
             Specifically:
                     Can't unify
                             Type
                     with
                             (\k => Vect k a) (S (plus m n))