A different(?) "Illegal application (Non-functional construction)"

[ANogin]

With the latest v8.8, the following code

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive Foo :=
| Prod : list Foo -> Foo.

Equations foo_type (t : Foo) : Type :=
  foo_type (Prod fs) := compact_prod (List.map foo_type fs).

(* Moving val into the return type, rather than having it as an argument might be unnecessary if
   https://github.com/mattam82/Coq-Equations/issues/73 was fixed *)
Equations lookup (t:Foo) : forall (val: foo_type t) (what: list nat), option nat := {
  lookup (Prod ss) := fun val what => 
    match what with nil=> None | cons hd tail => lookup_prod ss val hd tail end}

  where (struct ss) lookup_prod (ss: list Foo) 
                                  (val : compact_prod (map foo_type ss)) 
                                  (what_hd: nat) (what_tl: list nat) : option nat := {
  lookup_prod nil _ _ _ := None;
  lookup_prod (cons shd stl) _ _ what_tl <= (fun val what_hd => lookup_prod stl val what_hd what_tl) => {
    lookup_prod (cons shd nil) val 0 what_tl _ := lookup shd val what_tl;
    lookup_prod (cons shd nil) _ _ _ _ := None;
    lookup_prod (cons shd _) val 0 what_tl _ := lookup shd (fst val) what_tl;
    lookup_prod (cons _ _) val (S what_hd) _ what_stl_fun := what_stl_fun (snd val) what_hd}}.

results in

Illegal application (Non-functional construction): 
The expression "f" of type
 "forall l : list Foo,
  P (Prod l)
    (fun (val : foo_type (Prod l)) (what : list nat) =>
     match what with
     | [] => None
     | hd :: tail => lookup_prod l val hd tail
     end)"
cannot be applied to the terms
 "[]" : "list Foo"
 "val" : "compact_prod (map foo_type [])"
 "what_hd" : "nat"
 "what_tl" : "list nat"
 "None" : "option nat"

[mattam82]

This one is because the recursive calls under the match in lookup was not recognized, and we hence try to build a combined mutual induction principle for non-mutual inductives. Allowing the recognition of this recursive calls solves this (fix incoming), but it's a bit fragile for automation of the induction proof. Pattern-matchings should rather happen on the left. The right fix is to just define lookup as:

Equations(struct t) lookup (t:Foo) (val: foo_type t) (what: list nat) : option nat := {
  lookup (Prod ss) val nil := None;
  lookup (Prod ss) val (cons hd tl) := lookup_prod ss val hd tl }

Note the (struct t) annotation which is now taken into account (fix incoming as well).

[mattam82]

Now fixed