feat: convert unassigned universe level mvars into parameters

src/Init/Lean/Elab/DeclModifiers.lean

@@ -126,6 +126,18 @@ pure {
   attrs           := attrs
 }
 
+def mkDeclName (modifiers : Modifiers) (atomicName : Name) : CommandElabM Name := do
+currNamespace ← getCurrNamespace;
+let declName := currNamespace ++ atomicName;
+match modifiers.visibility with
+| Visibility.private => do
+  env ← getEnv;
+  let (env, declName) := mkPrivateName env declName;
+  setEnv env;
+  -- TODO: alias?
+  pure declName
+| _                  => pure declName
+
 end Command
 end Elab
 end Lean

src/Init/Lean/Elab/Declaration.lean

@@ -90,14 +90,15 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
 let declId             := stx.getArg 1;
 let (binders, typeStx) := expandDeclSig (stx.getArg 2);
 withDeclId declId $ fun name => do
-  currNamespace ← getCurrNamespace;
-  univNames     ← getUniverseNames;
+  declName  ← mkDeclName modifiers name;
+  univNames ← getUniverseNames;
   runTermElabM $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do
     type ← Term.elabType typeStx;
     Term.synthesizeSyntheticMVars false;
     type ← Term.instantiateMVars typeStx type;
     type ← Term.mkForall typeStx xs type;
-    let fullName := currNamespace ++ name;
+    (type, _) ← Term.mkForallUsedOnly typeStx vars type;
+    type ← Term.levelMVarToParam type;
     -- TODO: unassigned universe metavariables to new parameters
     -- TODO: if theorem, filter unused vars
     Term.dbgTrace (">>> " ++ toString type);

src/Init/Lean/Elab/Term.lean

@@ -285,6 +285,7 @@ def mkFreshTypeMVar (ref : Syntax) (kind : MetavarKind := MetavarKind.natural) (
 liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
 def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
 def mkForall (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkForall xs e
+def mkForallUsedOnly (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM (Expr × Nat) := liftMetaM ref $ Meta.mkForallUsedOnly xs e
 def mkLambda (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkLambda xs e
 def mkLet (ref : Syntax) (x : Expr) (e : Expr) : TermElabM Expr := mkLambda ref #[x] e
 def trySynthInstance (ref : Syntax) (type : Expr) : TermElabM (LOption Expr) := liftMetaM ref $ Meta.trySynthInstance type
@@ -329,6 +330,14 @@ stx.ifNode x (fun _ => throwError stx ("term elaborator failed, unexpected synta
 def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
 mkNode `Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[ident], mkNullNode #[mkAtom ":", type], mkNullNode, mkAtom ")"]
 
+/-- Convert unassigned universe level metavariables into parameters. -/
+def levelMVarToParam (e : Expr) : TermElabM Expr := do
+ctx ← read;
+mctx ← getMCtx;
+let r := mctx.levelMVarToParam (fun n => ctx.univNames.elem n) e;
+modify $ fun s => { mctx := r.mctx, .. s };
+pure r.expr
+
 /--
   Auxiliary method for creating fresh binder names.
   Do not confuse with the method for creating fresh free/meta variable ids. -/

src/Init/Lean/MetavarContext.lean

@@ -894,7 +894,7 @@ partial def isWellFormed (mctx : MetavarContext) (lctx : LocalContext) : Expr
 | Expr.localE _ _ _ _      => unreachable!
 
 
-namespace UnivMVarToParam
+namespace LevelMVarToParam
 
 structure Context :=
 (paramNamePrefix : Name)
@@ -949,7 +949,7 @@ partial def main : Expr → M Expr
 | e@(Expr.sort u _)        => do u ← visitLevel u; pure (e.updateSort! u)
 | e                        => pure e
 
-end UnivMVarToParam
+end LevelMVarToParam
 
 structure UnivMVarParamResult :=
 (mctx          : MetavarContext)
@@ -957,9 +957,9 @@ structure UnivMVarParamResult :=
 (nextParamIdx  : Nat)
 (expr          : Expr)
 
-def univMVarToParam (mctx : MetavarContext) (alreadyUsedPred : Name → Bool) (e : Expr) (paramNamePrefix : Name := `u) (nextParamIdx : Nat := 1)
+def levelMVarToParam (mctx : MetavarContext) (alreadyUsedPred : Name → Bool) (e : Expr) (paramNamePrefix : Name := `u) (nextParamIdx : Nat := 1)
     : UnivMVarParamResult :=
-let (e, s) := UnivMVarToParam.main e { paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred } { mctx := mctx, nextParamIdx := nextParamIdx };
+let (e, s) := LevelMVarToParam.main e { paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred } { mctx := mctx, nextParamIdx := nextParamIdx };
 { mctx          := mctx,
   newParamNames := s.paramNames,
   nextParamIdx  := s.nextParamIdx,