the type `xs ++ [] = xs` fails to compile

[rgrover]

Compiling the following declaration emits an error message. The code is adapted from the nearly identical function in Data.Vect.idr in Idris1.

Steps to Reproduce

import Data.Vect

vectNilRightNeutral : {n : Nat} -> (xs : Vect n a) -> xs ++ [] = xs

Expected Behavior

Should compile.

Observed Behavior

VectNil.idr:5:66--7:1:While processing type of vectNilRightNeutral at VectNil.idr:5:1--7:1:
Can't solve constraint between:
    n
and
    plus n 0

Why is the type-system complaining in this case?

Switching the order of arguments to ++ satisfies the type-checker (quite likely following from the definition of plus where plus n 0 cannot be normalized any further):

vectNilRightNeutral : {n : Nat} -> (xs : Vect n a) -> xs ++ [] = xs

Nevertheless, it should not be a problem to state the type xs ++ [] = xs.

Typing the following on the Idris2 REPl gives the same error:

:t \n:Nat => \a : Type => \xs : Vect n a => xs ++ [] = xs

[ziman]

Try ~=~ instead of =.

||| Explicit heterogeneous ("John Major") equality.  Use this when Idris
||| incorrectly chooses homogeneous equality for `(=)`.
||| @ a the type of the left side
||| @ b the type of the right side
||| @ x the left side
||| @ y the right side
public export
(~=~) : (x : a) -> (y : b) -> Type
(~=~) = Equal

[rgrover]

thanks.

[rgrover]

Any suggestions on how to define vectNilRightNeutral in this new world with heterogeneous equality?

vectNilRightNeutral : (xs : Vect len a) -> (xs ++ []) ~=~ xs
vectNilRightNeutral [] = Refl
vectNilRightNeutral (x :: xs) =
  let inductiveHypothesis = vectNilRightNeutral xs
   in rewrite inductiveHypothesis
    in Refl

compiles to the error message:

Can't solve constraint between:
    len
and
    plus len 0