Relax a bit the guard condition.

My previous optimization of guard checking (f1280889) made it slightly stricter,
in the presence of dependent pattern matching and nested inductive types whose
toplevel types are mutually recursive.

The following (cooked-up) example illustrates this:

Inductive list (A B : Type) := nil : list A B | cons : A -> list A B -> list
A B.

Inductive tree := Node : list tree tree -> tree.

Lemma foo : tree = tree. exact eq_refl. Qed.

Fixpoint id (t : tree) :=
  match t with
  | Node l =>
    let l := match foo in (_ = T) return list tree T with eq_refl => l end
    in
    match l with
    | nil  => Node (nil _ _)
    | cons x tl => Node (cons _ _ (id x) tl)
    end
  end.

is accepted, but changing tree to:

Inductive tree := Node : list tree tree -> tree.
with tree2 := .

made id be rejected after the optimization.

The same problem occurred in Paco, and is now fixed.

Note that in the example above, list cannot be mutually recursive because of the
current strict positivity condition for tree.

0 files changed, 0 insertions, 0 deletions