I'm getting a type error in the last line of the following program:
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]]).
This is the error I get:
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).
I don't really understand why I am getting this error. What is different between app and plus here?. Does it have to do with app being polymorphic while plus is a monomorphic nat -> nat -> nat function?
In case that matters, my version of Coq is 8.5.
You guessed it right: it does have something to do with app being polymorphic. The problem is that Coq allows implicit arguments to be inferred differently depending on whether the corresponding term is applied to arguments or not. More precisely, non-maximal implicits are only inserted when the term is applied to something, but not inserted if the term is used on its own, like your app. There are two ways to remedy the situation:
1- Force Coq to infer something for that instance, as in fold_right (@app _) [] [[5; 6]; [7; 8]].
2- Use a global declaration that will make the type argument maximally inserted: Arguments app {_} _ _.. For more details on what this is doing, check the reference manual