Wrong computation of non-uniform parameters breaks the generation of nested eliminators

[thomas-lamiaux]

Description of the problem

This code makes the new generation of the induction principle bug, it seems to be due to n being wrongfully computed as a uniform parameter

Small Rocq / Coq file to reproduce the bug

Set Debug "backtrace".
Set Debug "generate_eliminators".

(* Preliminary to be testable without the prelude *)
Notation "A -> B" := (forall (_ : A), B) (right associativity, at level 99).

(* This needs to be registered *)
Inductive unit : Set :=
    tt : unit.

Register unit as core.unit.type.
Register tt as core.unit.tt.

Inductive prod (A B : Type) : Type :=
pair : A -> B -> prod A B.

Arguments pair {_ _}.

#[universes(polymorphic)]
Inductive prod_all@{sa sb ; ua ub +} A (PA : A -> Type@{sa;ua}) B (PB : B -> Type@{sb;ub}) : prod A B -> Type :=
pair_all : forall a, PA a -> forall b, PB b -> prod_all A PA B PB (pair a b).

#[universes(polymorphic)]
Definition prod_all_forall@{sa sb ; ua ub +} A (PA : A -> Type@{sa;ua}) (HPA : forall a, PA a)
                    B (PB : B -> Type@{sb;ub}) (HPB : forall b, PB b) :
                    forall (x : prod A B), prod_all A PA B PB x :=
fun x => match x with
| pair a b => pair_all A PA B PB a (HPA a) b (HPB b)
end.

Register Scheme prod_all as All for prod.
Register Scheme prod_all_forall as AllForall for prod.

Variant Box (F  : unit -> Type) := .

Inductive Cut (x : unit) : Type :=
| triv : Box (fun n => prod (Cut n) unit) -> Cut x.

Version of Rocq / Coq where this bug occurs

master

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[thomas-lamiaux]

From what I understand, it is due to how Rocq check positivity for nested inductive types.
It does so by substituting the uniform parameters in the body, than checking it.
In this case, it reduces the body and end up with an empty, so declares it uniform.

It is problematic, because it is anti-modular as showcased above.
In particular, this issue is a much minimize version of MetaRocq typing case that after much reduction end up with typing Σ everywhere, and it ends being considered as uniform.

Variant case_side_conditions `{checker_flags} wf_local_fun typing Σ Γ ci p ps mdecl idecl indices predctx :=
| case_side_info
    ...
    (wf_pctx : wf_local_fun Σ (Γ ,,, predctx))
    ...
    (ind_inst : ctx_inst (typing Σ) Γ (p.(pparams) ++ indices)
                         (List.rev (subst_instance p.(puinst)
                                                   (ind_params mdecl ,,, ind_indices idecl : context))))
    (not_cofinite : isCoFinite mdecl.(ind_finite) = false).

Used for nesting in

    case_side_conditions (fun Σ Γ => wf_local Σ Γ) typing Σ Γ ci p ps
                         mdecl idecl indices predctx  ->

@mattam82 @yannl35133 that should concern you

[thomas-lamiaux]

After considering the problem I think it would make sense to change it as the only cases where it arises can easily be changed to

    case_side_conditions (fun Γ => wf_local Σ Γ) (typing Σ) Σ Γ ci p ps
                         mdecl idecl indices predctx  ->

I have opened #21498 to try the ci and see how many failures it causes