Bug: Derive NoConfusion for this inductive seems almost correct, but forgets to apply an argument?

[drcicero]

Derive NoConfusion seems to fail for inductives with

1. at least one parameter
2. at least one index
3. recursive occurrence of the type with a different parameter

For example, see this meaningless definition of a Foo with a parameter and an index of type unit:

From Equations Require Import Equations.
Inductive Foo (x:unit) : unit -> Set :=
| Easy : Foo x tt
| Hard : Foo tt tt -> Foo x tt.
Derive NoConfusion for Foo.
(* error *)

The error message is:

In environment
x :
sigma
  (fun
     index : sigma (fun _ : unit => unit)
   => Foo (pr1 index) (pr2 index))
x0 : unit
u : unit
The term "Foo u" has type "unit -> Set"
which should be Set, Prop or Type.

It seems that Derive NoConfusion generated a term that almost typechecks, except for the fact that it forgot to supply a value for the formal argument x. (According to the error message the missing argument may be the x0 in the environment).

If we change any of the conditions above (1,2,3) this error does not happen... For example, NoConfusion can be derived just fine, for an inductive Bar, that differs from Foo only by using the same parameter x for Hard (Condition 3):

From Equations Require Import Equations.
Inductive Bar (x:unit) : unit -> Set :=
| Easy : Bar x tt
| Hard : Bar (* -> *) x (* <- *) tt -> Bar x tt.
Derive NoConfusion for Foo.
(* no errors! *)

Could it be that the derivation code somewhere assumes wrongly that all occurrences of the inductive to be defined have the same parameters (however, that should only be required for occurrences in tail position) -- and if this assumption is not true, then we do not get any arguments for the parameters?

Using coq 8.13.2 and coq equations 1.3~beta+8.13.

[mattam82]

That's a real limitation, it should support non-uniform parameters.