I’m trying to build the sources for CPDT using Coq 8.10.2.
make fails with error
File "./src/GeneralRec.v", line 890, characters 55-66:
Error:
In environment
n : nat
m : nat
The term "Ret (n + m)" has type "comp nat" while it is expected to have type
"?T@{x:=m}" (unable to find a well-typed instantiation for
"?T": cannot ensure that "Type@{max(Set,comp.u0+1)}" is a subtype of
"Type@{Cpdt.GeneralRec.6713}").
GeneralRec:80 reads
(** Have we finally reached the ideal solution for encoding general recursive definitions, with minimal hassle in syntax and proof obligations? Unfortunately, we have not, as [comp] has a serious expressivity weakness. Consider the following definition of a curried addition function: *)
Definition curriedAdd (n : nat) := Ret (fun m : nat => Ret (n + m)).
This works in an earlier version of Coq I have installed.
Any hints as to what could be going wrong?