使用with子句匹配Vect末尾元素时报Not a constructor application or primitive错误

你尝试实现基于视图的Vect末尾n个元素模式匹配，已有定义如下：

data SplitLast : (n : Nat) -> (xs : Vect r a)
                 -> {auto prf : n `LTE` r} -> Type where
  Append : forall m, n . (init : Vect m a) -> (tail : Vect n a)
  -> SplitLast {prf=rewrite plusCommutative m n in lteAddRight n} n (init ++ tail)

splitLast : (n : Nat) -> (xs : Vect r a)
            -> {auto prf : n `LTE` r} -> SplitLast n xs

上述代码可正常编译，但在with子句中使用该视图时出现报错：

flipLast : Vect (S (S r)) Nat -> Vect (S (S r)) Nat
flipLast xs with (splitLast 2 xs)
  flipLast (leading ++ [m, n]) | (Append leading [m, n]) = leading ++ [n, m]

报错信息：

While processing left hand side of with block in flipLast. Can't match
on ?postpone [no locals in scope] (Not a constructor application or primitive).
...
187 | flipLast (leading ++ [m, n]) | (Append leading [m, n]) = leading ++ [n, m]
^^

• 模式匹配的左侧仅支持构造器表达式，++是Vect的拼接函数，不属于构造器（Vect的构造器仅为::和Nil），编译器无法反向将输入的xs拆解为leading ++ [m, n]的形式，因此抛出匹配失败错误。
• 你的SplitLast视图本身已经完成了Vect的拆分逻辑，Append构造器返回的init和tail就是拆分完成的前后段，无需在原参数位置重复做拼接匹配。

直接使用视图返回的拆分结果即可，无需对原参数做拼接模式匹配：

flipLast : Vect (S (S r)) Nat -> Vect (S (S r)) Nat
flipLast xs with (splitLast 2 xs)
  flipLast _ | (Append leading [m, n]) = leading ++ [n, m]

如果存在隐式证明合一的问题，也可以简化SplitLast的定义，将证明逻辑完全封装在splitLast的实现中，避免构造器内的rewrite影响类型推断：

data SplitLast : (n : Nat) -> (xs : Vect r a) -> {auto prf : n `LTE` r} -> Type where
  Append : (init : Vect m a) -> (tail : Vect n a) -> SplitLast n (init ++ tail)

内容的提问来源于stack exchange，提问作者joel