fix: correct universe used in below/brecOn for non-reflexive inductive types (#8937)

This PR changes the output universe of the generated `below`
implementation for non-reflexive inductive types to match the
implementation for reflexive inductive types in #7639.

This fixes the `below`/`brecOn` implementations for certain nested
inductive types, as reported in
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Universes/near/525030149.

src/Lean/Meta/Constructions/BRecOn.lean

@@ -57,7 +57,7 @@ fun {α} {motive} t =>
   List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
 ```
 -/
-private def mkBelowFromRec (recName : Name) (reflexive : Bool) (nParams : Nat)
+private def mkBelowFromRec (recName : Name) (nParams : Nat)
   (belowName : Name) : MetaM Unit := do
   -- The construction follows the type of `ind.rec`
   let .recInfo recVal ← getConstInfo recName
@@ -81,11 +81,7 @@ private def mkBelowFromRec (recName : Name) (reflexive : Bool) (nParams : Nat)
       | throwError "type of type of major premise {major} not a type former"
 
     -- universe level of the resultant type
-    let rlvl : Level :=
-      if reflexive then
-        mkLevelMax ilvl lvl
-      else
-        mkLevelMax 1 lvl
+    let rlvl : Level := mkLevelMax ilvl lvl
 
     let mut val := .const recName (rlvl.succ :: lvls)
     -- add parameters
@@ -122,7 +118,7 @@ def mkBelow (indName : Name) : MetaM Unit := do
 
   let recName := mkRecName indName
   let belowName := mkBelowName indName
-  mkBelowFromRec recName indVal.isReflexive indVal.numParams belowName
+  mkBelowFromRec recName indVal.numParams belowName
 
   -- If this is the first inductive in a mutual group with nested inductives,
   -- generate the constructions for the nested inductives now
@@ -130,7 +126,7 @@ def mkBelow (indName : Name) : MetaM Unit := do
     for i in [:indVal.numNested] do
       let recName := recName.appendIndexAfter (i + 1)
       let belowName := belowName.appendIndexAfter (i + 1)
-      mkBelowFromRec recName indVal.isReflexive indVal.numParams belowName
+      mkBelowFromRec recName indVal.numParams belowName
 
 /--
 If `minorType` is the type of a minor premies of a recursor, such as
@@ -188,7 +184,7 @@ fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
   ).1
 ```
 -/
-private def mkBRecOnFromRec (recName : Name) (reflexive : Bool) (nParams : Nat)
+private def mkBRecOnFromRec (recName : Name) (nParams : Nat)
     (all : Array Name) (brecOnName : Name) : MetaM Unit := do
   let .recInfo recVal ← getConstInfo recName | return
   let lvl::lvls := recVal.levelParams.map (Level.param ·)
@@ -215,11 +211,7 @@ private def mkBRecOnFromRec (recName : Name) (reflexive : Bool) (nParams : Nat)
       | throwError "type of type of major premise {major} not a type former"
 
     -- universe level of the resultant type
-    let rlvl : Level :=
-      if reflexive then
-        mkLevelMax ilvl lvl
-      else
-        mkLevelMax 1 lvl
+    let rlvl : Level := mkLevelMax ilvl lvl
 
     -- One `below` for each motive, with the same motive parameters
     let blvls := lvl::lvls
@@ -283,7 +275,7 @@ def mkBRecOn (indName : Name) : MetaM Unit := do
 
   let recName := mkRecName indName
   let brecOnName := mkBRecOnName indName
-  mkBRecOnFromRec recName indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
+  mkBRecOnFromRec recName indVal.numParams indVal.all.toArray brecOnName
 
   -- If this is the first inductive in a mutual group with nested inductives,
   -- generate the constructions for the nested inductives now.
@@ -291,4 +283,4 @@ def mkBRecOn (indName : Name) : MetaM Unit := do
     for i in [:indVal.numNested] do
       let recName := recName.appendIndexAfter (i + 1)
       let brecOnName := brecOnName.appendIndexAfter (i + 1)
-      mkBRecOnFromRec recName indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
+      mkBRecOnFromRec recName indVal.numParams indVal.all.toArray brecOnName

tests/lean/run/issue4650.lean

@@ -28,20 +28,20 @@ inductive Foo3 : Sort (u+1) where
 inductive Foo4 : Sort (max 1 u) where
   | intro: Foo4 → Foo4
 
-/-- info: Foo4.below.{u_1, u} {motive : Foo4.{u} → Sort u_1} (t : Foo4.{u}) : Sort (max 1 u_1) -/
+/-- info: Foo4.below.{u_1, u} {motive : Foo4.{u} → Sort u_1} (t : Foo4.{u}) : Sort (max (max 1 u) u_1) -/
 #guard_msgs in
 #check Foo4.below
 
 inductive Foo5 : Sort (max u 1) where
   | intro: Foo5 → Foo5
 
-/-- info: Foo5.below.{u_1, u} {motive : Foo5.{u} → Sort u_1} (t : Foo5.{u}) : Sort (max 1 u_1) -/
+/-- info: Foo5.below.{u_1, u} {motive : Foo5.{u} → Sort u_1} (t : Foo5.{u}) : Sort (max (max u 1) u_1) -/
 #guard_msgs in
 #check Foo5.below
 
 inductive Foo6 : Sort (u+1) where
   | intro: Foo6 → Foo6
 
-/-- info: Foo6.below.{u_1, u} {motive : Foo6.{u} → Sort u_1} (t : Foo6.{u}) : Sort (max 1 u_1) -/
+/-- info: Foo6.below.{u_1, u} {motive : Foo6.{u} → Sort u_1} (t : Foo6.{u}) : Sort (max (u + 1) u_1) -/
 #guard_msgs in
 #check Foo6.below

tests/lean/run/nestedInductiveConstructions.lean

@@ -135,12 +135,13 @@ inductive Tree : Type u where | node : List Tree → Tree
 
 /--
 info: @[reducible] protected def Ex3.Tree.below.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
-  {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max 1 u_1) :=
+  {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max (u + 1) u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
+  Tree.rec.{(max (u + 1) u_1) + 1, u} (fun a a_ih => PProd.{u_1, max (u + 1) u_1} (motive_2 a) a_ih)
+    PUnit.{max (u + 1) u_1}
     (fun head tail head_ih tail_ih =>
-      PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
+      PProd.{max (max 1 u_1) (u + 1) u_1, max (max 1 u_1) (u + 1) u_1}
+        (PProd.{u_1, max (u + 1) u_1} (motive_1 head) head_ih) (PProd.{u_1, max (u + 1) u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -148,12 +149,13 @@ fun {motive_1} {motive_2} t =>
 
 /--
 info: @[reducible] protected def Ex3.Tree.below_1.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
-  {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max 1 u_1) :=
+  {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max (u + 1) u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
+  Tree.rec_1.{(max (u + 1) u_1) + 1, u} (fun a a_ih => PProd.{u_1, max (u + 1) u_1} (motive_2 a) a_ih)
+    PUnit.{max (u + 1) u_1}
     (fun head tail head_ih tail_ih =>
-      PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
+      PProd.{max (max 1 u_1) (u + 1) u_1, max (max 1 u_1) (u + 1) u_1}
+        (PProd.{u_1, max (u + 1) u_1} (motive_1 head) head_ih) (PProd.{u_1, max (u + 1) u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in

tests/lean/run/nestedInductiveUniverse.lean

@@ -0,0 +1,7 @@
+/-!
+Tests a bug in the generated below/brecOn implementations for nested inductive types
+Reported at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Universes/near/525030149
+-/
+
+inductive TCTree : Type (u + 1)
+  | node : (Σ (I : Type u), I → TCTree) → TCTree