doc: document (and rename) the new configuration option ignoreLevelMVarDepth

src/Lean/Meta/Basic.lean

@@ -65,7 +65,16 @@ structure Config where
      the type of `t` with the goal target type. We claim this is not a hack and is defensible behavior because
      this last unification step is not really part of the term elaboration. -/
   assignSyntheticOpaque : Bool := false
-  ignoreLevelDepth      : Bool := false
+  /- When `ignoreLevelDepth` is `false`, only universe level metavariables with depth == metavariable context depth
+     can be assigned.
+     We used to have `ignoreLevelDepth == false` always, but this setting produced counterintuitive behavior in a few
+     cases. Recall that universe levels are often ignored by users, they may not even be aware they exist.
+     We still use this restriction for regular metavariables. See discussion at the beginning of `MetavarContext.lean`.
+     We claim it is reasonable to ignore this restriction for universe metavariables because their values are often
+     contrained by the terms is instances and simp theorems.
+     TODO: we should delete this configuration option and the method `isReadOnlyLevelMVar` after we have more tests.
+  -/
+  ignoreLevelMVarDepth  : Bool := true
 
 structure ParamInfo where
   binderInfo     : BinderInfo := BinderInfo.default
@@ -381,7 +390,7 @@ def getLevelMVarDepth (mvarId : MVarId) : MetaM Nat := do
   | _          => throwError "unknown universe metavariable '?{mvarId}'"
 
 def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool := do
-  if (← getConfig).ignoreLevelDepth then
+  if (← getConfig).ignoreLevelMVarDepth then
     return false
   else
     return (← getLevelMVarDepth mvarId) != (← getMCtx).depth

src/Lean/Meta/LevelDefEq.lean

@@ -101,7 +101,7 @@ mutual
     | Level.mvar mvarId _, _ =>
       if (← isReadOnlyLevelMVar mvarId) then
         return LBool.undef
-      else if (← getConfig).ignoreLevelDepth && (← isMVarWithGreaterDepth v mvarId) then
+      else if (← getConfig).ignoreLevelMVarDepth && (← isMVarWithGreaterDepth v mvarId) then
         -- If both `u` and `v` are both metavariables, but depth of v is greater, then we assign `v := u`.
         -- This can only happen when `ignoreLevelDepth` is set to true.
         assignLevelMVar v.mvarId! u

src/Lean/Meta/SynthInstance.lean

@@ -582,7 +582,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
   let inputConfig ← getConfig
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false,
-                                          ignoreLevelDepth := true }) do
+                                          ignoreLevelMVarDepth := true }) do
     let type ← instantiateMVars type
     let type ← preprocess type
     let s ← get