[jasisz]

Adds a test to corner-cases/ with outcome: either: the nested inductive

inductive NestedRedex
| leaf : NestedRedex
| a : List ((fun _ : Bool => NestedRedex) true) → NestedRedex
| b : List NestedRedex → NestedRedex

built with addDecl (the elaborator never writes such a field), and a theorem nestedRedex that reduces NestedRedex.rec on a [b [leaf]] to 11. The kernel finds nested occurrences syntactically, so the two List occurrences become two auxiliary types and the recursor has three motives. No checker entry changes.

A checker that normalises constructor types before collecting nested occurrences merges the two, derives a recursor with two motives and rejects the theorem. sokonanoda does this; its author considers such fields not valid nested inductives and the official kernel's answer an artefact of its syntactic test (intgrah/sokonanoda#12), hence either rather than accept. The official kernel, lean4lean, nanoda, nanobruijn, nanoclo, Pestka, tenet, kefir, con-leche and con-ron accept it (checked locally against an export made with Lean 4.35.0). The file compiles on the arena's 4.34.1 toolchain; I have not run lka.py.

The theorem is built as a term too, because the elaborator does not see the auxiliary recursor NestedRedex.rec_1 in the file that added the block.

---

Second commit: other/vanishing-occurrence, also outcome: accept. Two inductive types whose constructor field mentions the type being declared only inside a redex that reduces it away:

| node : (fun _ : Type => Nat) VanishPos → VanishPos
| node : (fun _ : Type => Nat) (VanishNeg → Nat) → VanishNeg

The kernel puts the field in weak head normal form before it looks for occurrences, finds Nat and accepts both, the second one even though the unreduced field has a negative occurrence. kefir (8fb94a9) rejects both inductives; the other 15 checkers I ran accept. kefir also rejects let X := VanishPos; Nat and Nat → (fun _ : Type => Nat) VanishPos, and accepts (fun X : Type => X) VanishPos, where the occurrence survives reduction. kefir has issues disabled, so this test is the report.

[jasisz]

@DmitryKorolev: other/vanishing-occurrence is rejected by kefir (also at 8fb94a9) and accepted by the official kernel. kefir's issues are disabled, so mentioning it here. The rejection is at the inductive declaration itself; variants with let and under Nat → behave the same, while (fun X : Type => X) VanishPos is accepted.

[intgrah]

I wouldn't recommend writing a test based on this behaviour. What the official kernel does is not really sane in the first place. It all comes down to whether you preprocess an inductive signature into beta-normal form, and do a syntactic check. It's highly implementation specific and cursed

[jasisz]

Fair, it may not be sane, but agreed: I've moved nested-redex-aux to corner-cases with outcome: either (52f95f3).

[jasisz]

I just found that other/vanishing-occurrence is essentially the same case as the existing corner-cases/positivity-whnf, so it should not be an accept test. I'm closing this one and will prepare a single, larger batch of corner cases instead. Sorry for the trouble.