fix: levelMVarToParam must update levelNames

src/Lean/Elab/BuiltinCommand.lean

@@ -233,7 +233,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
     let e ← Term.elabTerm term none
     Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := ignoreStuckTC)
-    let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
+    let e ← Term.levelMVarToParam (← instantiateMVars e)
     let type ← inferType e
     unless e.isSyntheticSorry do
       logInfoAt tk m!"{e} : {type}"
@@ -245,7 +245,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
     let e ← Term.elabTerm term none
     Term.synthesizeSyntheticMVarsNoPostponing
-    let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
+    let e ← Term.levelMVarToParam (← instantiateMVars e)
     -- TODO: add options or notation for setting the following parameters
     withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
       let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := false) (skipTypes := false)
@@ -318,7 +318,7 @@ unsafe def elabEvalUnsafe : CommandElab
   | `(#eval%$tk $term) => do
     let declName := `_eval
     let addAndCompile (value : Expr) : TermElabM Unit := do
-      let (value, _) ← Term.levelMVarToParam (← instantiateMVars value)
+      let value ← Term.levelMVarToParam (← instantiateMVars value)
       let type ← inferType value
       let us := collectLevelParams {} value |>.params
       let value ← instantiateMVars value

src/Lean/Elab/Declaration.lean

@@ -112,7 +112,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
       let type ← instantiateMVars type
       let type ← mkForallFVars xs type
       let type ← mkForallFVars vars type (usedOnly := true)
-      let (type, _) ← Term.levelMVarToParam type
+      let type ← Term.levelMVarToParam type
       let usedParams  := collectLevelParams {} type |>.params
       match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
       | Except.error msg      => throwErrorAt stx msg

src/Lean/Elab/Inductive.lean

@@ -408,18 +408,15 @@ def shouldInferResultUniverse (u : Level) : TermElabM (Option LMVarId) := do
   it should be inferred later using `inferResultingUniverse`.
 -/
 private def levelMVarToParam (indTypes : List InductiveType) (univToInfer? : Option LMVarId) : TermElabM (List InductiveType) :=
-  go |>.run' 1
+  indTypes.mapM fun indType => do
+    let type  ← levelMVarToParam' indType.type
+    let ctors ← indType.ctors.mapM fun ctor => do
+      let ctorType ← levelMVarToParam' ctor.type
+      return { ctor with type := ctorType }
+    return { indType with ctors, type }
 where
-  levelMVarToParam' (type : Expr) : StateRefT Nat TermElabM Expr := do
-    Term.levelMVarToParam' type (except := fun mvarId => univToInfer? == some mvarId)
-
-  go : StateRefT Nat TermElabM (List InductiveType) := do
-    indTypes.mapM fun indType => do
-      let type  ← levelMVarToParam' indType.type
-      let ctors ← indType.ctors.mapM fun ctor => do
-        let ctorType ← levelMVarToParam' ctor.type
-        return { ctor with type := ctorType }
-      return { indType with ctors, type }
+  levelMVarToParam' (type : Expr) : TermElabM Expr := do
+    Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId)
 
 def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level :=
   if us.isEmpty && rOffset == 0 then

src/Lean/Elab/MutualDef.lean

@@ -710,8 +710,9 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
     let mut newHeaders := #[]
     for view in views, header in headers do
       if view.kind.isTheorem then
-        newHeaders := newHeaders.push { header with type :=
-          (← monadMap (@withLevelNames (levelNames := header.levelNames)) (levelMVarToParam' header.type)) }
+        newHeaders ←
+          withLevelNames header.levelNames do
+            return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }
       else
         newHeaders := newHeaders.push header
     return newHeaders

src/Lean/Elab/PreDefinition/Basic.lean

@@ -33,12 +33,9 @@ def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Arra
   preDefs.mapM fun preDef => do
     pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }
 
-private def levelMVarToParamPreDeclsAux (preDefs : Array PreDefinition) : StateRefT Nat TermElabM (Array PreDefinition) :=
-  preDefs.mapM fun preDef => do
-    pure { preDef with type := (← levelMVarToParam' preDef.type), value := (← levelMVarToParam' preDef.value) }
-
 def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
-  (levelMVarToParamPreDeclsAux preDefs).run' 1
+  preDefs.mapM fun preDef => do
+    pure { preDef with type := (← levelMVarToParam preDef.type), value := (← levelMVarToParam preDef.value) }
 
 private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (List Name) := do
   let mut s : CollectLevelParams.State := {}

src/Lean/Elab/Structure.lean

@@ -595,27 +595,24 @@ private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldI
   let (lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos
   withLCtx lctx localInsts <| k vars
 
-private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (univToInfer? : Option LMVarId) : TermElabM (Array StructFieldInfo) :=
-  go |>.run' 1
+private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (univToInfer? : Option LMVarId) : TermElabM (Array StructFieldInfo) := do
+  levelMVarToParamFVars scopeVars
+  levelMVarToParamFVars params
+  fieldInfos.mapM fun info => do
+    levelMVarToParamFVar info.fvar
+    match info.value? with
+    | none       => pure info
+    | some value =>
+      let value ← levelMVarToParam' value
+      pure { info with value? := value }
 where
-  levelMVarToParam' (type : Expr) : StateRefT Nat TermElabM Expr := do
-    Term.levelMVarToParam' type (except := fun mvarId => univToInfer? == some mvarId)
+  levelMVarToParam' (type : Expr) : TermElabM Expr := do
+    Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId)
 
-  go : StateRefT Nat TermElabM (Array StructFieldInfo) := do
-    levelMVarToParamFVars scopeVars
-    levelMVarToParamFVars params
-    fieldInfos.mapM fun info => do
-      levelMVarToParamFVar info.fvar
-      match info.value? with
-      | none       => pure info
-      | some value =>
-        let value ← levelMVarToParam' value
-        pure { info with value? := value }
-
-  levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit :=
+  levelMVarToParamFVars (fvars : Array Expr) : TermElabM Unit :=
     fvars.forM levelMVarToParamFVar
 
-  levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
+  levelMVarToParamFVar (fvar : Expr) : TermElabM Unit := do
     let type ← inferType fvar
     discard <| levelMVarToParam' type
 

src/Lean/Elab/Term.lean

@@ -582,22 +582,13 @@ def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
 
 /--
   Convert unassigned universe level metavariables into parameters.
-  The new parameter names are of the form `u_i` where `i >= nextParamIdx`.
-  The method returns the updated expression and new `nextParamIdx`.
-
-  Remark: we make sure the generated parameter names do not clash with the universe at `ctx.levelNames`. -/
-def levelMVarToParam (e : Expr) (nextParamIdx : Nat := 1) (except : LMVarId → Bool := fun _ => false) : TermElabM (Expr × Nat) := do
+  The new parameter names are fresh names of the form `u_i` with regard to `ctx.levelNames`, which is updated with the new names. -/
+def levelMVarToParam (e : Expr) (except : LMVarId → Bool := fun _ => false) : TermElabM Expr := do
   let levelNames ← getLevelNames
-  let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u nextParamIdx
+  let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u 1
+  setLevelNames (levelNames ++ r.newParamNames.toList)
   setMCtx r.mctx
-  return (r.expr, r.nextParamIdx)
-
-/-- Variant of `levelMVarToParam` where `nextParamIdx` is stored in a state monad. -/
-def levelMVarToParam' (e : Expr) (except : LMVarId → Bool := fun _ => false) : StateRefT Nat TermElabM Expr := do
-  let nextParamIdx ← get
-  let (e, nextParamIdx) ← levelMVarToParam e nextParamIdx except
-  set nextParamIdx
-  return e
+  return r.expr
 
 /--
   Auxiliary method for creating fresh binder names.

tests/lean/levelNGen.lean

@@ -2,3 +2,5 @@ opaque test1 {α : Sort _} : α → Sort u_1
 #check @test1
 def test2 {α : Sort _} : α → Sort u_1 := sorry
 #check @test2
+variable {α : Sort _} in theorem test3 : α → Sort _ := sorry
+#check @test3

tests/lean/levelNGen.lean.expected.out

@@ -1,3 +1,5 @@
 @test1 : {α : Sort u_2} → α → Sort u_1
 levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry'
 @test2 : {α : Sort u_2} → α → Sort u_1
+levelNGen.lean:5:33-5:38: warning: declaration uses 'sorry'
+@test3 : {α : Sort u_2} → α → Sort u_1

tests/lean/run/PPTopDownAnalyze.lean

@@ -43,7 +43,7 @@ syntax (name := testDelabTD) "#testDelab " term " expecting " term : command
 @[commandElab testDelabTD] def elabTestDelabTD : CommandElab
   | `(#testDelab $stx:term expecting $tgt:term) => liftTermElabM do withDeclName `delabTD do
      let e ← elabTerm stx none
-     let ⟨e, _⟩ ← levelMVarToParam e
+     let e ← levelMVarToParam e
      let e ← instantiateMVars e
      checkDelab e (some tgt)
   | _ => throwUnsupportedSyntax