`filter_stack_domain` of guard checker using wrong context? · Coq devs & plugin devs

Hi,
I'm wondering about a thing I noticed when reading the code of the guardedness checker in inductive.ml. In filter_stack_domain, the filter_stack function goes into recursion (line 965 on the master branch) to filter the stack according to the remaining body c0 of the match predicate with an altered environment env, obtained at line 952. However, that environment will now contain the elements of the ctx from decomposing the type a, which I believe it shouldn't.
For example in:

Hypothesis (p : nat -> Prop).
Hypothesis (H0 : forall n, p n -> p (S n)).
Fixpoint test7 (n : nat) :=
  fun H =>
  match n return forall (H: forall m, p m), p n with
  | 0 => fun H => H 0
  | S n => fun H => H0 n (test7 n H)
  end H.

When restricting the stack domain upon entering the match, filter_stack will, in the first step, examine the prod (H : forall m, p m). After decomposing the type forall m, p m, m will be added to env in line 952. And now the remaining stack is restricted with p n (by the recursive call) in an environment where the Rel 2 for n is incorrectly bound to m, which shouldn't be in scope.

Can someone please confirm that this is unintended? (if so, the fix is simple: just rename the new env created in the let in line 952 to not shadow the old one).
I've not really attempted to construct a more sophisticated example where this might actually break something (mostly because I don't fully understand why the restriction of subterm information flowing through a match is needed in the first place).

Matthieu Sozeau (Dec 16 2020 at 10:03):

Matthieu Sozeau (Dec 16 2020 at 10:07):

The filter_stack_domain ensures that the guard checking handles the "commutative cut" of iota and beta redexes correctly: one can consider H a subterm in a branch (match c with | Ci => fun H => b end) arg iff arg is already a subterm of inductive type (and not arbitrary type). Failure to restrict this results in an inconsistency in presence of propositional extensionality or univalence (look for the coq-club messages and patches by Maxime Dénès IIRC)

Stream: Coq devs & plugin devs

Topic: `filter_stack_domain` of guard checker using wrong context?

Lennard Gäher (Dec 15 2020 at 14:32):

Matthieu Sozeau (Dec 16 2020 at 10:03):

Matthieu Sozeau (Dec 16 2020 at 10:07):

Lennard Gäher (Dec 16 2020 at 10:21):