mと（マイナスm 0）の間のタイプの不一致

Question

私は、バイナリと単項関数からツリーとして構築された、n-ary関数の従属型を定義しようとしています;これは(Vect n a) -> aの型と同型です） Idrisを学ぶ練習として。

n項関数に引数を適用する関数を定義しようとしている（（N-1）進機能を生成する）一方で、私は非常に疑わしいエラーを得た：

Type mismatch between 
      ArityFn m a (Type of ng) 
    and 
      ArityFn (minus m 0) a (Expected type) 

    Specifically: 
      Type mismatch between 
        m 
      and 
        minus m 0 

は、ここでのコードです質問のため

data ArityFn : Nat -> (ty: Type) -> Type where 
    Val  : (x : ty) -> ArityFn 0 ty 
    UnaryFn : (ty -> ty) -> ArityFn 1 ty 
    BinaryFn : (ty -> ty -> ty) -> ArityFn 2 ty 
    NAryFn : (ty -> ty -> ty) -> (ArityFn n ty) -> (ArityFn m ty) -> ArityFn (n + m) ty 

%name ArityFn nf, ng, nh 

applyArityFn : a -> (ArityFn n a) -> (LTE 1 n) -> ArityFn (n - 1) a 
... (some definitions elided) 
applyArityFn x (NAryFn h (UnaryFn f) ng) _ = mkNAryFn h (Val (f x))  ng 

これは型チェッカーのバグですか？

:def minus戻ります（他のもののうち、いくつかのクリーンアップを法）：

Original definiton: 
minus 0 right = 0 
minus left 0 = left 
minus (S left) (S right) = minus left right 

をあなたはminus left 0 = leftがないことを見ることができます疑いで、捕まってしまった関数の定義を探し

Answer 1

前にパターンminus 0 right = 0があるので、定義的に保持する。もちろん、両方の式が一致すると同じ結果を返しますが、idrisはそのことを知らないのです。 mで何とかパターンマッチのいずれか

• とminusはその最初の引数が証拠によって
• や書き換えを露出されるのヘッドコンストラクタということになりまし減らすために得る：

  あなたはあなたができる望む結果を得るために、 minus m 0 = m。