refactor: replace ignoreLevelMVarDepth by levelAssignDepth

src/Lean/Meta/Basic.lean

@@ -97,13 +97,6 @@ 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
-  /-- 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 set `ignoreLevelMVarDepth := false` during `simp`. See comment at `withSimpConfig` and issue #1829.
-  -/
-  ignoreLevelMVarDepth  : Bool := true
   /-- Enable/Disable support for offset constraints such as `?x + 1 =?= e` -/
   offsetCnstrs          : Bool := true
   /-- Eta for structures configuration mode. -/
@@ -613,11 +606,8 @@ def getLevelMVarDepth (mvarId : LMVarId) : MetaM Nat :=
 Return true if the given universe metavariable is "read-only".
 That is, its `depth` is different from the current metavariable context depth.
 -/
-def _root_.Lean.LMVarId.isReadOnly (mvarId : LMVarId) : MetaM Bool := do
-  if (← getConfig).ignoreLevelMVarDepth then
-    return false
-  else
-    return (← mvarId.getLevel) != (← getMCtx).depth
+def _root_.Lean.LMVarId.isReadOnly (mvarId : LMVarId) : MetaM Bool :=
+  return (← mvarId.getLevel) < (← getMCtx).levelAssignDepth
 
 @[deprecated LMVarId.isReadOnly]
 def isReadOnlyLevelMVar (mvarId : LMVarId) : MetaM Bool := do
@@ -1313,9 +1303,9 @@ private def withExistingLocalDeclsImp (decls : List LocalDecl) (k : MetaM α) :
 def withExistingLocalDecls (decls : List LocalDecl) : n α → n α :=
   mapMetaM <| withExistingLocalDeclsImp decls
 
-private def withNewMCtxDepthImp (x : MetaM α) : MetaM α := do
+private def withNewMCtxDepthImp (allowLevelAssignments : Bool) (x : MetaM α) : MetaM α := do
   let saved ← get
-  modify fun s => { s with mctx := s.mctx.incDepth, postponed := {} }
+  modify fun s => { s with mctx := s.mctx.incDepth allowLevelAssignments, postponed := {} }
   try
     x
   finally
@@ -1324,11 +1314,12 @@ private def withNewMCtxDepthImp (x : MetaM α) : MetaM α := do
 /--
   `withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
   where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
-  Note that this does not affect level metavariables (by default).
-  See the docstring of `isDefEq` for more information.
+  If `allowLevelAssignments` is set to true, then the level metavariable depth
+  is not increased, and level metavariables from the outer scope can be
+  assigned.  (This is used by TC synthesis.)
 -/
-def withNewMCtxDepth : n α → n α :=
-  mapMetaM withNewMCtxDepthImp
+def withNewMCtxDepth (k : n α) (allowLevelAssignments := false) : n α :=
+  mapMetaM (withNewMCtxDepthImp allowLevelAssignments) k
 
 private def withLocalContextImp (lctx : LocalContext) (localInsts : LocalInstances) (x : MetaM α) : MetaM α := do
   let localInstsCurr ← getLocalInstances
@@ -1666,10 +1657,6 @@ def isExprDefEq (t s : Expr) : MetaM Bool :=
   So, `withNewMCtxDepth (isDefEq a b)` is `isDefEq` without any mvar assignment happening
   whereas `isDefEq a b` will assign any metavariables of the current depth in `a` and `b` to unify them.
 
-  By default, level metavariables can be assigned at any depth.
-  That is, `withNewMCtxDepth (isDefEq a b)` will still assign level mvars in `a` and `b`.
-  Setting the option `ignoreLevelMVarDepth := false` will disable this behavior.
-
   For matching (where only mvars in `b` should be assigned), we create the term inside the `withNewMCtxDepth`.
   For an example, see [Lean.Meta.Simp.tryTheoremWithExtraArgs?](https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L100-L106)
  -/

src/Lean/Meta/Coe.lean

@@ -161,7 +161,15 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
   else if autoLift.get (← getOptions) then
     try
       -- Construct lift from `m` to `n`
-      let monadLiftType ← mkAppM ``MonadLiftT #[m, n]
+      -- Note: we cannot use mkAppM here because mkAppM does not assign universe metavariables,
+      -- but we need to make sure that the domains of `m` and `n` have the same level.
+      let .forallE _ (.sort um₁) (.sort um₂) _ ← whnf (← inferType m) | return none
+      let .forallE _ (.sort un₁) (.sort un₂) _ ← whnf (← inferType n) | return none
+      let u ← decLevel um₁
+      let .true ← isLevelDefEq u (← decLevel un₁) | return none
+      let v ← decLevel um₂
+      let w ← decLevel un₂
+      let monadLiftType := mkAppN (.const ``MonadLiftT [u, v, w]) #[m, n]
       let .some monadLiftVal ← trySynthInstance monadLiftType | return none
       let u_1 ← getDecLevel α
       let u_2 ← getDecLevel eType

src/Lean/Meta/LevelDefEq.lean

@@ -53,9 +53,9 @@ mutual
     | Level.mvar mvarId, _ =>
       if (← mvarId.isReadOnly) then
         return LBool.undef
-      else if (← getConfig).ignoreLevelMVarDepth && (← isMVarWithGreaterDepth v mvarId) then
+      else if (← 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.
+        -- This can only happen when levelAssignDepth is set to a smaller value than depth (e.g. during TC synthesis)
         assignLevelMVar v.mvarId! u
         return LBool.true
       else if !u.occurs v then

src/Lean/Meta/SynthInstance.lean

@@ -682,7 +682,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     | none        =>
       withTraceNode `Meta.synthInstance
         (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
-      let result? ← withNewMCtxDepth do
+      let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize
       let resultHasUnivMVars := if let some result := result? then !result.paramNames.isEmpty else false
@@ -698,7 +698,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
           if (← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType) then
             let result ← instantiateMVars result
             /- We use `check` to propogate universe constraints implied by the `result`.
-               Recall that we use `ignoreLevelMVarDepth := true` which allows universe metavariables in the current depth to be assigned,
+               Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
                but these assignments are discarded by `withNewMCtxDepth`.
 
                TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether

src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean

@@ -10,6 +10,8 @@ namespace Lean.Meta.Linear.Nat
 
 namespace Collect
 
+inductive LinearArith
+
 structure Cnstr where
   cnstr : LinearArith
   proof : Expr

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -724,26 +724,7 @@ where
     return r
 
 @[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
-  /-
-  We set `ignoreLevelMVarDepth := false` because we don't want a `simp` theorem to constraint a universe level metavariable.
-  For example, consider the following example from issue #1829
-  ```
-  @[simp] theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
-  ⟨fun _ => ⟨⟩, fun _ => (Subsingleton.elim ..)⟩
-
-  structure Func' (α : Sort _) (β : Sort _) :=
-  (toFun    : α → β)
-
-  def r : Func' α α := ⟨id⟩
-
-  example (x y : α) (h : x = y) : r.toFun x = y := by simp <;> rw [h]
-  ```
-  `α` has type `Sort ?u`. If `ignoreLevelMVarDepth := true`, then `eq_iff_true_of_subsingleton` is applicable
-  by setting `?u := 0` and using instance `instance (p : Prop) : Subsingleton p`.
-  Moreover, the assignment is lost since `simp`, and a type error is produced later. Even if we prevented the assignment
-  from being lost, the situation is far from ideal since `simp` would be restricting the universe level.
-  -/
-  withConfig (fun c => { c with etaStruct := ctx.config.etaStruct, ignoreLevelMVarDepth := false }) <| withReducible x
+  withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
 def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
   let ctx := { ctx with config := (← ctx.config.updateArith) }

src/Lean/MetavarContext.lean

@@ -308,6 +308,8 @@ For more information on specifics see the comment in the file that `MetavarConte
 structure MetavarContext where
   /-- Depth is used to control whether an mvar can be assigned in unification. -/
   depth          : Nat := 0
+  /-- At what depth level mvars can be assigned. -/
+  levelAssignDepth : Nat := 0
   /-- Counter for setting the field `index` at `MetavarDecl` -/
   mvarCounter    : Nat := 0
   lDepth         : PersistentHashMap LMVarId Nat := {}
@@ -384,7 +386,7 @@ def isMVarDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
 def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do
   let mctx ← getMCtx
   match mctx.lDepth.find? mvarId with
-  | some d => return d == mctx.depth
+  | some d => return d >= mctx.levelAssignDepth
   | _      => panic! "unknown universe metavariable"
 
 def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
@@ -838,8 +840,11 @@ def isAnonymousMVar (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
   | none          => false
   | some mvarDecl => mvarDecl.userName.isAnonymous
 
-def incDepth (mctx : MetavarContext) : MetavarContext :=
-  { mctx with depth := mctx.depth + 1 }
+def incDepth (mctx : MetavarContext) (allowLevelAssignments := false) : MetavarContext :=
+  let depth := mctx.depth + 1
+  let levelAssignDepth :=
+    if allowLevelAssignments then mctx.levelAssignDepth else depth
+  { mctx with depth, levelAssignDepth }
 
 instance : MonadMCtx (StateRefT MetavarContext (ST ω)) where
   getMCtx    := get

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -59,8 +59,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias _uniq.659 -> _uniq.299
-        • FVarAlias _uniq.658 -> _uniq.297
+        • FVarAlias _uniq.634 -> _uniq.299
+        • FVarAlias _uniq.633 -> _uniq.297
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -74,8 +74,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias _uniq.690 -> _uniq.299
-        • FVarAlias _uniq.689 -> _uniq.297
+        • FVarAlias _uniq.665 -> _uniq.299
+        • FVarAlias _uniq.664 -> _uniq.297
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/389.lean.expected.out

@@ -5,5 +5,5 @@ argument
 has type
   Bar Nat : Type
 but is expected to have type
-  Foo ?m : Sort (max 1 ?u)
+  Foo ?m : Type
 getFoo bar.toFoo : Nat

tests/lean/run/1951.lean

@@ -0,0 +1,13 @@
+class FunLike (F : Type _) (A : outParam (Type _)) (B : outParam (A → Type _)) where toFun : F → ∀ a, B a
+instance [FunLike F A B] : CoeFun F fun _ => ∀ a, B a where coe := FunLike.toFun
+class One (M) where one : M
+instance [One M] : OfNat M (nat_lit 1) where ofNat := One.one
+class OneHomClass (F) (A B : outParam _) [One A] [One B] extends FunLike F A fun _ => B where
+  map_one (f : F) : f 1 = 1
+class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends FunLike F A fun _ => B
+class Monoid (M) extends Mul M, One M
+class MonoidHomClass (F) (A B : outParam _) [Monoid A] [Monoid B] extends MulHomClass F A B, OneHomClass F A B
+
+theorem map_one [Monoid A] [Monoid B] [OneHomClass F A B] (f : F) : f 1 = 1 := OneHomClass.map_one f
+example [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) : f 1 = 1 := by
+  simp only [map_one]