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).

@Lennard Gäher you are right, I think this is unintended.

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)

Thanks for the confirmation and the pointers! I'll create an issue then.

(for reference, the corresponding thread on coq-club is https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html -- the restriction now makes a lot more sense to me).

Last updated: Oct 13 2024 at 01:02 UTC