fix: do not reverse subgoals of local instances

src/Lean/Data/Name.lean

@@ -96,16 +96,6 @@ def quickCmp (n₁ n₂ : Name) : Ordering :=
 def quickLt (n₁ n₂ : Name) : Bool :=
   quickCmp n₁ n₂ == Ordering.lt
 
-/-- Alternative HasLt instance. -/
-@[inline] protected def hasLtQuick : LT Name :=
-  ⟨fun a b => Name.quickLt a b = true⟩
-
-@[inline] def Name.decLt : DecidableRel (@LT.lt Name Name.hasLtQuick) :=
-  inferInstanceAs (DecidableRel fun a b => Name.quickLt a b = true)
-
-instance : DecidableRel (@LT.lt Name Name.hasLtQuick) :=
-  Name.decLt
-
 /-- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool

src/Lean/Meta/Coe.lean

@@ -54,18 +54,28 @@ def coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr) := do
 
 /-- Coerces `expr` to a function type. -/
 def coerceToFunction? (expr : Expr) : MetaM (Option Expr) := do
-  let result ← try mkAppM ``CoeFun.coe #[expr] catch _ => return none
-  let expanded ← expandCoe result
+  -- constructing expression manually because mkAppM wouldn't assign universe mvars
+  let α ← inferType expr
+  let u ← getLevel α
+  let v ← mkFreshLevelMVar
+  let γ ← mkFreshExprMVar (← mkArrow α (mkSort v))
+  let .some inst ← trySynthInstance (mkApp2 (.const ``CoeFun [u,v]) α γ) | return none
+  let expanded ← expandCoe (mkApp4 (.const ``CoeFun.coe [u,v]) α γ inst expr)
   unless (← whnf (← inferType expanded)).isForall do
-    throwError "failed to coerce{indentExpr expr}\nto a function, after applying `CoeFun.coe`, result is still not a function{indentExpr expanded}\nthis is often due to incorrect `CoeFun` instances, the synthesized instance was{indentExpr result.appFn!.appArg!}"
+    throwError "failed to coerce{indentExpr expr}\nto a function, after applying `CoeFun.coe`, result is still not a function{indentExpr expanded}\nthis is often due to incorrect `CoeFun` instances, the synthesized instance was{indentExpr inst}"
   return expanded
 
 /-- Coerces `expr` to a type. -/
 def coerceToSort? (expr : Expr) : MetaM (Option Expr) := do
-  let result ← try mkAppM ``CoeSort.coe #[expr] catch _ => return none
-  let expanded ← expandCoe result
+  -- constructing expression manually because mkAppM wouldn't assign universe mvars
+  let α ← inferType expr
+  let u ← getLevel α
+  let v ← mkFreshLevelMVar
+  let β ← mkFreshExprMVar (mkSort v)
+  let .some inst ← trySynthInstance (mkApp2 (.const ``CoeSort [u,v]) α β) | return none
+  let expanded ← expandCoe (mkApp4 (.const ``CoeSort.coe [u,v]) α β inst expr)
   unless (← whnf (← inferType expanded)).isSort do
-    throwError "failed to coerce{indentExpr expr}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr expanded}\nthis is often due to incorrect `CoeSort` instances, the synthesized instance was{indentExpr result.appFn!.appArg!}"
+    throwError "failed to coerce{indentExpr expr}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr expanded}\nthis is often due to incorrect `CoeSort` instances, the synthesized instance was{indentExpr inst}"
   return expanded
 
 /-- Return `some (m, α)` if `type` can be reduced to an application of the form `m α` using `[reducible]` transparency. -/

src/Lean/Meta/ExprDefEq.lean

@@ -1811,7 +1811,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
 builtin_initialize
   registerTraceClass `Meta.isDefEq
   registerTraceClass `Meta.isDefEq.stuck
-  registerTraceClass `Meta.isDefEq.stuck.mvar (inherited := true)
+  registerTraceClass `Meta.isDefEq.stuckMVar (inherited := true)
   registerTraceClass `Meta.isDefEq.cache
   registerTraceClass `Meta.isDefEq.foApprox (inherited := true)
   registerTraceClass `Meta.isDefEq.onFailure (inherited := true)

src/Lean/Meta/SynthInstance.lean

@@ -312,14 +312,11 @@ private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInst
 def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) (inst : Expr) : MetaM SubgoalsResult := do
   let instType ← inferType inst
   let result ← getSubgoalsAux lctx localInsts xs #[] 0 [] inst instType
-  match inst.getAppFn with
-  | Expr.const constName _ =>
+  if let .const constName _ := inst.getAppFn then
     let env ← getEnv
     if hasInferTCGoalsRLAttribute env constName then
       return result
-    else
-      return { result with subgoals := result.subgoals.reverse }
-  | _ => return result
+  return { result with subgoals := result.subgoals.reverse }
 
 /--
   Try to synthesize metavariable `mvar` using the instance `inst`.
@@ -327,29 +324,6 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do
-  if ← mvar.mvarId!.isAssigned then
-    /- The metavariable `mvar` may have been assigned when solving typing constraints.
-       This may happen when a local instance type depends on other local instances.
-       For example, in Mathlib, we have
-       ```
-       @Submodule.setLike : {R : Type u_1} → {M : Type u_2} →
-         [_inst_1 : Semiring R] →
-         [_inst_2 : AddCommMonoid M] →
-         [_inst_3 : @ModuleS R M _inst_1 _inst_2] →
-         SetLike (@Submodule R M _inst_1 _inst_2 _inst_3) M
-       ```
-       TODO: discuss what is the correct behavior here. There are other possibilities.
-       1) We could try to synthesize the instances `_inst_1` and `_inst_2` and check
-          whether it is defeq to the one inferred by typing constraints. That is, we
-          remove this `if`-statement. We discarded this one because some Mathlib theorems
-          failed to be elaborated using it.
-       2) Generate an error/warning message when instances such as `Submodule.setLike` are declared,
-          and instruct user to use `{}` binder annotation for `_inst_1` `_inst_2`.
-
-       It is important to check here whether `mvar` is *assigned*, it might
-       still contain metavariables (such as universe mvars etc.).
-     -/
-    return some ((← getMCtx), [])
   let mvarType   ← inferType mvar
   let lctx       ← getLCtx
   let localInsts ← getLocalInstances
@@ -477,6 +451,21 @@ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM
 
 /-- Process the next subgoal in the given consumer node. -/
 def consume (cNode : ConsumerNode) : SynthM Unit := do
+  /- Filter out subgoals that have already been assigned when solving typing constraints.
+    This may happen when a local instance type depends on other local instances.
+    For example, in Mathlib, we have
+    ```
+    @Submodule.setLike : {R : Type u_1} → {M : Type u_2} →
+      [_inst_1 : Semiring R] →
+      [_inst_2 : AddCommMonoid M] →
+      [_inst_3 : @ModuleS R M _inst_1 _inst_2] →
+      SetLike (@Submodule R M _inst_1 _inst_2 _inst_3) M
+    ```
+  -/
+  let cNode := { cNode with
+    subgoals := ← withMCtx cNode.mctx do
+      cNode.subgoals.filterM (not <$> ·.mvarId!.isAssigned)
+  }
   match cNode.subgoals with
   | []      => addAnswer cNode
   | mvar::_ =>
@@ -672,6 +661,8 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
+  withTraceNode `Meta.synthInstance
+    (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   /-
     We disable eta for structures that are not classes during TC resolution because it allows us to find unintended solutions.
     See discussion at
@@ -685,10 +676,10 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     let type ← preprocess type
     let s ← get
     match s.cache.synthInstance.find? type with
-    | some result => pure result
+    | some result =>
+      trace[Meta.synthInstance] "result {result} (cached)"
+      pure result
     | none        =>
-      withTraceNode `Meta.synthInstance
-        (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
       let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize