Illegal application (Non-functional construction)

[mattam82]

Illegal application (Non-functional construction)

[ANogin]

Just to add to the list of weird things that happen with these kinds of examples, if I change the above test case by swapping the order of num and sum (that is, replacing Equations num ... where sum ... with Equations sum ... where num ...), then I get

Recursive definition of sum is ill-formed.
In environment
sum : forall f : foo, (foo_type f -> nat) -> forall fs : list foo, compact_prod (map foo_type (f :: fs)) -> nat
f : foo
numf : foo_type f -> nat
fs : list foo
f0 : foo
l : list foo
val : compact_prod (map foo_type (f :: f0 :: l))
num : forall f : foo, foo_type f -> nat
f1 : foo
l0 : list foo
f2 : foo
l1 : list foo
val0 : foo_type (List (f2 :: l1))
Recursive call to sum has principal argument equal to "l1" instead of "l".
Recursive definition is:
"fun (f : foo) (numf : foo_type f -> nat) (fs : list foo) =>
 sum_functional sum (fix num (f0 : foo) : foo_type f0 -> nat := num_functional sum num f0) f numf fs".

[ANogin]

See also the "P.S." comment in #93 for an example of what makes a difference in seeing or not seeing this issue.

[ANogin]

This appears to be fixes in the latest v8.8

[mattam82]

Indeed, it's similar to #105