Guards refine match return predicate arguments

[thierry-martinez]

Bug 5530 - Fixpoint guard when generalization occurs on strict subterms

The following fixpoint definition now typechecks.

Inductive Counter: nat -> Set :=
  Zero: Counter O
| Succ: forall n, Counter n -> Counter (S n).

Fixpoint count2 n (u: Counter n) (v: Counter n) {struct u}: unit :=
  match u with
    Zero => fun _ => tt
  | Succ n u' =>
    fun (v: Counter (S n)) => match v with
      Succ n v' => fun u' => count2 n u' v'
    end u'
  end v.

[thierry-martinez]

The guard condition becomes unsafe indeed, sorry for the noise!
I keep thinking about a safe solution.

Example adapted from failure/subterm3.v (thanks to Hugo Herbelin for pointing this).

Axiom prop_ext: forall P Q, (P <-> Q) -> P=Q.

Inductive I: Prop := C: (False -> I) -> I.

Lemma I_eq_True: I = True.
Proof.
  apply prop_ext. split.
  - trivial.
  - intros. constructor. apply False_rect.
Qed.

Lemma I_eq_False_impl_I: I = (False -> I).
Proof.
  apply prop_ext. split.
  - trivial.
  - exact C.
Qed.

Inductive eq': Prop -> Prop := eq_refl': eq' I.

Lemma I_eq_False_impl_I': eq' (False -> I).
Proof.
  rewrite <- I_eq_False_impl_I. constructor.
Qed.

Fail Fixpoint loop (x: I): False :=
  match x with
    C f =>
    match I_eq_False_impl_I' in eq' T return T -> False with
      eq_refl' => fun x => loop x
    end f
  end.