change computation of uniform parameters

[thomas-lamiaux]

Change the computation of the uniform-parameters in the nested case

Fixes / closes #21497

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.

• Opened overlay pull requests.
  Adapt to rocq-prover/rocq#21498 (changed computation uniform parameters) MetaRocq/metarocq#1233

[thomas-lamiaux]

@coqbot run full ci

[coqbot-app]

🔴 CI failure at commit 9b30b9e without any failure in the test-suite

✔️ Corresponding job for the base commit 80ca8f9 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-metarocq

• You can also pass me a specific list of targets to minimize as arguments.

[yannl35133]

Can you fix the generator code without modifying the kernel?
If not, does this part of the code need to stay in the kernel or can this be moved out?
This PR is only a good idea if the answers are no and "it needs to stay"

[SkySkimmer]

This can make rocq take arbitrary amounts of time, eg

#[local] Set Warnings "-abstract-large-number".
Definition size := 0x100000000.
Record Fin (n : nat) := Fin_mk { val : nat; isLt : (val < n) }.
Record UInt32 := mk { val0 : Fin size }.

[coqbot-app]

🔴 CI failure at commit 9b30b9e without any failure in the test-suite

✔️ Corresponding job for the base commit 80ca8f9 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-metarocq

• You can also pass me a specific list of targets to minimize as arguments.

[SkySkimmer]

why is this warning getting printed 12 times?

[thomas-lamiaux]

No idea, it should be printing four times, once per induction scheme because they are a look up for Box each time

[thomas-lamiaux]

It is probably because the type is generated, and the term, and the term needs to generate the type, and it ends with a x3

[thomas-lamiaux]

but this was already the case for nested_eliminators.out

[thomas-lamiaux]

Can you fix the generator code without modifying the kernel? If not, does this part of the code need to stay in the kernel or can this be moved out? This PR is only a good idea if the answers are no and "it needs to stay"

It needs to stay for different reasons, plus, it is another job to start refactoring the kernel than fixing a bug

[thomas-lamiaux]

@coqbot run full ci

[thomas-lamiaux]

@coqbot run full ci

[thomas-lamiaux]

@coqbot run full ci

[yannl35133]

Can you fix the generator code without modifying the kernel? If not, does this part of the code need to stay in the kernel or can this be moved out? This PR is only a good idea if the answers are no and "it needs to stay"

It needs to stay for different reasons, plus, it is another job to start refactoring the kernel than fixing a bug

It's only a bug because your generator assumed a semantics that was not the one computed here, the rest of the code seems fine.
I understand this is weird semantics, but that's what it is nonetheless. It's used in the guard condition, so changing this would arguably be a (imo poorly justified) regression there, if not worse (though I severely doubt it would).

You have another solution which is to not trust this number and compute it with your own semantics on your side.

[thomas-lamiaux]

It's used in the guard condition, so changing this would arguably be a (imo poorly justified) regression there, if not worse (though I severely doubt it would).

1. Over-optimisations that break modularity are bugs. They were no issue before because they were no clear theory about eliminators for nested inductive types. This design choice now clearer appear wrong.
2. This does not change the expressivity, as every definition can be slightly rewritten in order not to rely on the over-optimisation. It is 99% backward compat as proven by the CI, except 10l~ diff in MetaRocq because as always MetaRocq does weird stuff. It is better to agree for a common number in declarations.mli than start using different code, in different places.
3. I don't see what it changes for the guard. As far as I see, the number of uniform parameters does not appear in wf_path. Moreover, I do not change wf_path, and I use a more restrictive number in declaration.mli so they are no reasons it would introduce a bug.
4. I plan to open a more complete draft PR to redo the positivity condition soon, and see if the dynamic positivity checking of nested inductive types is really needed in the CI. If not, we could accept exactly the inductive for which we know how to generate a useful eliminator for.

[thomas-lamiaux]

@yannl35133, @SkySkimmer and @ppedrot agreed to do this change, if you oppose as a maintainer of the kernel, or they are convinced by your arguments, it can be discussed next Rocq call. As you wish.

[SkySkimmer]

@coqbot bench

[yannl35133]

1. Since it's been that way for 12 years, it is a feature, how unfortunate it might be.
2. This changes the expressivity, as some definitions need to be rewritten. Even the CI caught a development which relies on this feature, so removing it needs a bigger reason imo
   2b. I'd be fine with adding a comment or a similar provision that this number has a weird meaning until it is changed.
3. The change for the guard was the wrong thing to focus on, I had missed at first the difference that this change makes for the positivity checker, which makes for a more visible difference
4. Please open this PR for a larger change. It will lead to a more open discussion on what to change and what to break, take long enough that enough people will find this, and hopefully lead to extensive explanations for the new definition of positivity and everything around it (be it as a paper or simply a fully written reference manual page)

Examples that get rejected after the PR:

Variant Empty (A : Type) := .
Variant Box (F : Type -> Type) (t : Type) := box (x : F t).

Inductive Weird1 (A : Type) : Type :=
| weird1 : A -> Empty (Weird1 (Weird1 (A * A))) -> Weird1 A.

Inductive Weird2 (A : Type) : Type :=
| weird2 : A -> Box Weird2 A -> Weird2 A.

Inductive Rec1 := C1 (x : Weird1 Rec1).
Inductive Rec2 := C2 (x : Weird2 Rec2).

Fixpoint f1 (x : Rec1) : False := match x with C1 (weird1 _ x _) => f1 x end.
Fixpoint f2 (x : Rec2) : False := match x with C2 (weird2 _ x _) => f2 x end.

[thomas-lamiaux]

Since it's been that way for 12 years, it is a feature, how unfortunate it might be.

Not used, not needed => bug

Even the CI caught a development which relies on this feature, so removing it needs a bigger reason imo

Not an argument. At the opposite, only having to change 10l out of the whole CI shows that people only stumble on it by accident

this number has a weird meaning until it is changed.

It is computation is perfectly sensible. Moreover, they are no spec of the computation of uniform parameters in the refman, which we can add with this PR.

The change for the guard was the wrong thing to focus on, I had missed at first the difference that this change makes for the positivity checker, which makes for a more visible difference

I don't see the issue with this example no longer be accepted.

Variant Empty (A : Type) := .
Inductive Weird1 (A : Type) : Type :=
| weird1 : A -> Empty (Weird1 (Weird1 (A * A))) -> Weird1 A.
Fail Inductive Rec1 := C1 (x : Weird1 Rec1).

At the opposite, rejecting it is a feature.
If you have unsued variables it is your issue.
This definition of Empty should additionally cause a warning unsed_variables imo.

The following example is the only one that can break and needs fixing.

Variant Box (F : Type -> Type) (t : Type) := box (x : F t).
Inductive Weird2 (A : Type) : Type :=
| weird2 : A -> Box Weird2 A -> Weird2 A.

but as explained it is equi-expressive to the following, into which it can easily be rewritten.
Moreover, as shown by the CI, no one uses that except MetaRocq which got fixed easily.

Variant Box (F : Type) := box (x : F).
Inductive Weird2 (A : Type) : Type :=
| weird2 : A -> Box (Weird2 A) -> Weird2 A.

[thomas-lamiaux]

@yannl35133 @tabareau It actually does change something non-trivial if you start hiding stuff under match like this type

Inductive depends_on_b (b : bool) (F : Type -> Type) (A : Type) := 
| cdepb : if b then F nat else F A -> depends_on_b b F A

If you define the following

Inductive RT A :=
| node : depends_on_b false RT A

Then you can't nest on A whether before it was allowed.
I do not know how many people use weird dynamic stuff like that, it seems no one in the CI.
In practice, it is still expressive, but it may remove a bit of modularity.
Note, that with our version of positivity, nesting on depends_on_b would not be allowed all together

[thomas-lamiaux]

@yannl35133 what could be done is keep the former value, and use my code to raise an error at definition if it finds a smaller value saying it may cause the generation of elimination principles to fail ? Note this is linked to #21495
I am open to other ideas.

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                        coq-bedrock2 │  350.82   356.01  -1.46 │  2918448077214   2918831134627  -0.01 │  833532   837648  -0.49 │
│ coq-neural-net-interp-computed-lite │  236.68   239.23  -1.07 │  2268249393528   2268188956738   0.00 │  872384   873572  -0.14 │
│                        rocq-bignums │   25.00    25.22  -0.87 │   159113139207    159101923018   0.01 │  460492   459488   0.22 │
│          rocq-metarocq-translations │   15.57    15.70  -0.83 │   110704930443    110723179616  -0.02 │  777224   775460   0.23 │
│                 rocq-mathcomp-order │   80.52    81.15  -0.78 │   599949217825    600018660944  -0.01 │ 2021684  2024160  -0.12 │
│               coq-engine-bench-lite │  127.89   128.87  -0.76 │   957467814539    959576059733  -0.22 │ 1037116  1037244  -0.01 │
│                        coq-coqprime │   52.96    53.27  -0.58 │   362113432029    362217939534  -0.03 │  823616   825660  -0.25 │
│              rocq-mathcomp-fingroup │   26.62    26.77  -0.56 │   173982760499    174000992103  -0.01 │  601668   601556   0.02 │
│                 coq-category-theory │  552.42   554.92  -0.45 │  4048251203140   4049925205502  -0.04 │  930720   931548  -0.09 │
│                            coq-corn │  648.62   651.55  -0.45 │  4381154856386   4381276724116  -0.00 │  768052   766860   0.16 │
│                             coq-vst │  840.93   844.61  -0.44 │  6367478477302   6367410490920   0.00 │ 2063160  2061132   0.10 │
│              rocq-mathcomp-solvable │  103.00   103.45  -0.43 │   720856976779    720859750297  -0.00 │ 1528032  1528132  -0.01 │
│                      coq-coquelicot │   46.58    46.78  -0.43 │   274568482104    274548594651   0.01 │  841100   840684   0.05 │
│        coq-fiat-crypto-with-bedrock │ 7076.13  7105.81  -0.42 │ 58141213985563  58140580459726   0.00 │ 3117540  3105308   0.39 │
│                        coq-rewriter │  333.91   335.29  -0.41 │  2488972941032   2489071434538  -0.00 │ 1492264  1495064  -0.19 │
│                 rocq-metarocq-pcuic │  628.52   630.86  -0.37 │  4024774053046   4024786509265  -0.00 │ 1919120  1921328  -0.11 │
│                   coq-iris-examples │  366.61   367.84  -0.33 │  2415816463426   2415816875371  -0.00 │ 1128484  1127652   0.07 │
│               rocq-mathcomp-algebra │  332.15   333.23  -0.32 │  2487722418604   2487708091285   0.00 │ 1628028  1624800   0.20 │
│                    coq-fiat-parsers │  276.24   277.07  -0.30 │  2114131958940   2114085921299   0.00 │ 2259128  2256164   0.13 │
│                rocq-metarocq-common │   40.57    40.69  -0.29 │   261095278811    261073821573   0.01 │  905692   905544   0.02 │
│              coq-mathcomp-odd-order │  608.38   609.95  -0.26 │  4380404144232   4380499909965  -0.00 │ 3369772  3369592   0.01 │
│                            coq-hott │  154.32   154.71  -0.25 │  1043894431904   1043826399245   0.01 │  465956   468244  -0.49 │
│           rocq-metarocq-safechecker │  358.47   359.35  -0.24 │  2644054675529   2644550457338  -0.02 │ 1845204  1854284  -0.49 │
│                    coq-math-classes │   83.23    83.42  -0.23 │   506116242604    506120371061  -0.00 │  512708   513692  -0.19 │
│                           rocq-elpi │   16.00    16.03  -0.19 │   112372538776    112339754518   0.03 │  579516   576120   0.59 │
│             rocq-mathcomp-character │  101.69   101.88  -0.19 │   726534925632    726480683870   0.01 │ 2148332  2148048   0.01 │
│               coq-mathcomp-analysis │ 1083.07  1084.29  -0.11 │  8189121565487   8188054669498   0.01 │ 2630272  2628708   0.06 │
│         coq-rewriter-perf-SuperFast │  479.20   479.54  -0.07 │  3737547146175   3737110856992   0.01 │ 1252456  1262172  -0.77 │
│                         coq-unimath │ 1803.31  1803.38  -0.00 │ 14950670506162  14950374284949   0.00 │ 1072072  1073716  -0.15 │
│                           coq-verdi │   43.55    43.55   0.00 │   289089929855    289079005242   0.00 │  525968   526000  -0.01 │
│                        coq-compcert │  311.39   311.34   0.02 │  2044127205747   2043898347668   0.01 │ 1186068  1186556  -0.04 │
│                         coq-coqutil │   46.71    46.69   0.04 │   291984613935    291987392222  -0.00 │  564572   564176   0.07 │
│                       coq-fourcolor │ 1366.46  1365.77   0.05 │ 12570687729889  12570408146267   0.00 │ 1416616  1418568  -0.14 │
│          coq-performance-tests-lite │  913.57   912.37   0.13 │  7318191679221   7314148367531   0.06 │ 1840200  1840132   0.00 │
│                  rocq-mathcomp-boot │   39.61    39.53   0.20 │   233311398857    233287939420   0.01 │  752728   751552   0.16 │
│              rocq-metarocq-template │   82.73    82.56   0.21 │   568094968687    568134249806  -0.01 │ 1049264  1049936  -0.06 │
│               rocq-metarocq-erasure │  479.33   478.30   0.22 │  3273026521074   3273083471599  -0.00 │ 1894100  1892500   0.08 │
│                       coq-fiat-core │   55.25    55.12   0.24 │   336312530025    336306151141   0.00 │  480340   482532  -0.45 │
│                 rocq-mathcomp-field │  187.73   187.27   0.25 │  1433298506149   1433471000973  -0.01 │ 2736932  2736536   0.01 │
│                      coq-verdi-raft │  494.97   493.34   0.33 │  3406705213504   3406575398914   0.00 │  817056   817028   0.00 │
│                           coq-color │  230.90   230.06   0.37 │  1460586618280   1460598123148  -0.00 │ 1148380  1147624   0.07 │
│                 rocq-metarocq-utils │   24.08    23.98   0.42 │   155405880137    155401697882   0.00 │  596256   594000   0.38 │
│                        rocq-runtime │   74.30    73.84   0.62 │   537922434811    537785135880   0.03 │  498952   495896   0.62 │
│                         rocq-stdlib │  449.69   446.73   0.66 │  1547995078269   1547938818146   0.00 │  627736   630216  -0.39 │
│             rocq-mathcomp-ssreflect │    1.20     1.18   1.69 │     8314771941      8315537140  -0.01 │  863156   862732   0.05 │
│                           rocq-core │    6.88     6.76   1.78 │    40944022741     40907251613   0.09 │  437352   437820  -0.11 │
│                      rocq-equations │    8.70     8.49   2.47 │    59875291442     59905008773  -0.05 │  398896   397832   0.27 │
│                            coq-core │    2.76     2.69   2.60 │    18308484682     18316555063  -0.04 │   88856    88936  -0.09 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                        TOP 25 SLOW DOWNS                                                         │
│                                                                                                                                  │
│  OLD    NEW    DIFF    %DIFF   Ln                    FILE                                                                        │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  96.2   97.6  1.3503    1.40%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html              │
│  11.5   12.2  0.7100    6.18%  194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                     │
│  1.23   1.79  0.5610   45.55%  813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                    │
│  27.2   27.7  0.5125    1.89%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                 │
│  46.6   47.1  0.4216    0.90%  115  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                   │
│  11.8   12.2  0.4121    3.50%  324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html     │
│ 0.248  0.626  0.3772  151.88%   34  rocq-stdlib/theories/Logic/SetoidChoice.v.html                                               │
│  24.6   25.0  0.3699    1.50%   12  coq-fourcolor/theories/proof/job319to322.v.html                                              │
│  11.7   12.0  0.3535    3.03%  388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html     │
│  46.6   46.9  0.3311    0.71%  115  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │
│  4.02   4.32  0.2996    7.45%  492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                         │
│  29.8   30.1  0.2947    0.99%   12  coq-fourcolor/theories/proof/job001to106.v.html                                              │
│  18.0   18.3  0.2856    1.59%   32  coq-performance-tests-lite/src/pattern.v.html                                                │
│  29.0   29.3  0.2793    0.96%  145  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                 │
│ 0.346  0.622  0.2765   79.92%  586  rocq-stdlib/theories/Strings/Byte.v.html                                                     │
│  29.3   29.6  0.2648    0.90%   12  coq-fourcolor/theories/proof/job589to610.v.html                                              │
│ 0.326  0.590  0.2636   80.85%    1  rocq-stdlib/theories/ZArith/ZNsatz.v.html                                                    │
│ 0.261  0.518  0.2577   98.89%   19  rocq-stdlib/theories/FSets/FSetFacts.v.html                                                  │
│  6.79   7.03  0.2473    3.64%  842  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                    │
│  28.7   28.9  0.2387    0.83%   12  coq-fourcolor/theories/proof/job563to588.v.html                                              │
│  7.61   7.85  0.2369    3.11%  633  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html     │
│ 0.274  0.506  0.2320   84.74%   13  rocq-stdlib/theories/ZArith/Zmin.v.html                                                      │
│ 0.306  0.530  0.2234   72.91%   11  rocq-stdlib/theories/setoid_ring/Rings_Q.v.html                                              │
│   120    120  0.2229    0.19%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                       │
│  20.8   21.0  0.2226    1.07%  479  rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html             │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SPEED UPS                                                             │
│                                                                                                                                          │
│  OLD     NEW     DIFF     %DIFF    Ln                     FILE                                                                           │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   67.6    62.7  -4.9549   -7.33%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                      │
│   67.6    64.7  -2.8590   -4.23%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html    │
│    203     201  -2.4097   -1.19%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html    │
│   40.5    38.8  -1.6610   -4.10%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│   44.7    43.4  -1.3687   -3.06%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│   31.5    30.5  -0.9931   -3.15%   139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   31.6    30.6  -0.9813   -3.11%   157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   32.8    31.8  -0.9752   -2.97%   121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   31.7    30.8  -0.9578   -3.02%   148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   31.6    30.8  -0.8258   -2.61%   180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   31.5    30.7  -0.8212   -2.61%   166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   31.4    30.6  -0.8041   -2.56%   198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   31.6    30.8  -0.8021   -2.54%   214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│   42.4    41.6  -0.7493   -1.77%   246  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                     │
│   65.5    64.8  -0.6869   -1.05%   716  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                            │
│   18.2    17.6  -0.5770   -3.17%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                        │
│   33.3    32.7  -0.5540   -1.67%    12  coq-fourcolor/theories/proof/job439to465.v.html                                                  │
│   45.7    45.2  -0.5427   -1.19%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                 │
│ 33.789  33.278  -0.5110   -1.51%   194  coq-vst/veric/expr_lemmas4.v.html                                                                │
│   31.4    30.9  -0.5030   -1.60%   258  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                       │
│   26.6    26.2  -0.4529   -1.70%    62  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html                                   │
│   48.4    48.0  -0.4374   -0.90%   260  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│   1.44    1.01  -0.4291  -29.81%   690  rocq-stdlib/theories/setoid_ring/Field_theory.v.html                                             │
│   31.7    31.2  -0.4261   -1.35%   334  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                       │
│   34.2    33.8  -0.4210   -1.23%   960  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[ppedrot]

FTR, this kind of change is necessary for fixing #21526. Indeed, to prevent an explosive expansion of the rtree for nested inductive types, one needs a compact representation of rtree nesting. This can only be achieved for inductive types that are uniformly nesting, in which case we can precompute the nesting body as a kind of parameterized rtree.