相关疑难解决方法(0)

我正在玩伊德里斯,我遇到了一些令我困惑的事:

以下类型检查:

conc : Vect n a -> Vect m a -> Vect (n+m) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

但这不是:

conc : Vect n a -> Vect m a -> Vect (m+n) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

出现以下错误:

When checking right hand side of conc with expected type
        Vect (m + 0) a

Type mismatch between …