Coqで `fold_right`と一緒に` app`を使用できないのはなぜですか？

Question

私は次のプログラムの最後の行の型エラーを取得しています：

Require Import List. 
Import ListNotations. 

(* This computes to 10 *) 
Compute (fold_right plus 0 [1;2;3;4]). 

(* I want this to compute to [5;6;7;8] but it gives a type error instead *) 
Compute (fold_right app [] [[5;6]; [7;8]]). 

これは私が取得エラーです：私はこれを取得していますなぜ

Error: 
The term "app" has type "forall A : Type, list A -> list A -> list A" while it is expected to have type 
"Type -> ?A -> ?A" (cannot instantiate "?A" because "A" is not in its scope). 

私は本当に理解していませんエラー。 appとplusの違いは何ですか？それはappが多形であるのに対して、plusは単形nat -> nat -> natの機能ですか？

重要な場合は、私のCoqのバージョンは8.5です。

Answer 1

あなたはそれを正しく推測しました：それは多形であるappと関係があります。問題は、Coqが、対応する項が引数に適用されるかどうかによって、暗黙の引数が異なる方法で推論されることを可能にすることです。より正確には、非最大のimplicitsは、用語が何かに適用されている場合にのみ挿入されますが、その用語が独自に使用されている場合は挿入されません（appなど）。状況を改善するには、2つの方法があります。

1強制的にCoqがそのインスタンスに対して何かを推測するようにします（fold_right (@app _) [] [[5; 6]; [7; 8]]など）。

2タイプ引数を最大限に挿入するグローバル宣言を使用してください：Arguments app {_} _ _.。これについての詳細はreference manual