feat: add withSynthesize (postpone := partial) k

It forces pending elaboration problems and tactics to be executed, but
allows TC ones to be postponed.

src/Lean/Elab/Binders.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
+import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab.Term
@@ -646,7 +647,29 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
   let (type, val, binders) ← elabBindersEx binders fun xs => do
     let (binders, fvars) := xs.unzip
-    let type ← elabType typeStx
+    /-
+    We use `withSynthesize` to ensure that any postponed elaboration problem
+    and nested tactics in `type` are resolved before elaborating `val`.
+    Resolved: we want to avoid synthethic opaque metavariables in `type`.
+    Recall that this kind of metavariable is non-assignable, and `isDefEq`
+    may waste a lot of time unfolding declarations before failing.
+    See issue #4051 for an example.
+
+    Here is the analysis for issue #4051.
+    - Given `have x : type := value; body`, we were previously elaborating `value` even
+      if `type` contained postponed elaboration problems.
+    - Moreover, the metavariables in `type` corresponding to postponed elaboration
+      problems cannot be assigned by `isDefEq` since the elaborator is supposed to assign them.
+    - Then, when checking whether type of `value` is definitionally equal to `type`,
+      a very long-time was spent unfolding a bunch of declarations before it failed.
+      In #4051, it was unfolding `Array.swaps` which is defined by well-founded recursion.
+      After the failure, the elaborator inserted a postponed coercion
+      that would be resolved later as soon as the types don't have unassigned metavariables.
+
+    We use `postpone := .partial` to allow type class (TC) resolution problems to be postponed
+    Recall that TC resolution does **not** produce synthetic opaque metavariables.
+    -/
+    let type ← withSynthesize (postpone := .partial) <| elabType typeStx
     registerCustomErrorIfMVar type typeStx "failed to infer 'let' declaration type"
     if elabBodyFirst then
       let type ← mkForallFVars fvars type

src/Lean/Elab/BuiltinNotation.lean

@@ -98,7 +98,7 @@ open Meta
       show Nat from 0
     ```
     -/
-    let type ← withSynthesize (mayPostpone := true) do
+    let type ← withSynthesize (postpone := .yes) do
       let type ← elabType type
       if let some expectedType := expectedType? then
         -- Recall that a similar approach is used when elaborating applications
@@ -314,11 +314,11 @@ where
 
 @[builtin_term_elab typeAscription] def elabTypeAscription : TermElab
   | `(($e : $type)), _ => do
-    let type ← withSynthesize (mayPostpone := true) <| elabType type
+    let type ← withSynthesize (postpone := .yes) <| elabType type
     let e ← elabTerm e type
     ensureHasType type e
   | `(($e :)), expectedType? => do
-    let e ← withSynthesize (mayPostpone := false) <| elabTerm e none
+    let e ← withSynthesize (postpone := .no) <| elabTerm e none
     ensureHasType expectedType? e
   | _, _ => throwUnsupportedSyntax
 

src/Lean/Elab/Extra.lean

@@ -188,7 +188,7 @@ private partial def toTree (s : Syntax) : TermElabM Tree := do
   the macro declaration names in the `op` nodes.
   -/
   let result ← go s
-  synthesizeSyntheticMVars (mayPostpone := true)
+  synthesizeSyntheticMVars (postpone := .yes)
   return result
 where
   go (s : Syntax) := do
@@ -486,7 +486,6 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
   | some f => withSynthesizeLight do
     /-
     We used to use `withSynthesize (mayPostpone := true)` here instead of `withSynthesizeLight` here.
-    Recall that `withSynthesizeLight` is equivalent to `withSynthesize (mayPostpone := true) (synthesizeDefault := false)`.
     It seems too much to apply default instances at binary relations. For example, we cannot elaborate
     ```
     def as : List Int := [-1, 2, 0, -3, 4]

src/Lean/Elab/Inductive.lean

@@ -324,7 +324,7 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
           | some ctorType =>
             let type ← Term.elabType ctorType
             trace[Elab.inductive] "elabType {ctorView.declName} : {type} "
-            Term.synthesizeSyntheticMVars (mayPostpone := true)
+            Term.synthesizeSyntheticMVars (postpone := .yes)
             let type ← instantiateMVars type
             let type ← checkParamOccs type
             forallTelescopeReducing type fun _ resultingType => do

src/Lean/Elab/StructInst.lean

@@ -939,7 +939,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
 
      TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior.
   -/
-  let { val := r, struct, instMVars } ← withSynthesize (mayPostpone := true) <| elabStruct struct expectedType?
+  let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStruct struct expectedType?
   trace[Elab.struct] "before propagate {r}"
   DefaultFields.propagate struct
   synthesizeAppInstMVars instMVars r

src/Lean/Elab/SyntheticMVars.lean

@@ -288,6 +288,32 @@ private def processPostponedUniverseContraints : TermElabM Unit := do
 private def markAsResolved (mvarId : MVarId) : TermElabM Unit :=
   modify fun s => { s with syntheticMVars := s.syntheticMVars.erase mvarId }
 
+/--
+Auxiliary type for `synthesizeSyntheticMVars`. It specifies
+whether pending synthetic metavariables can be postponed or not.
+-/
+inductive PostponeBehavior where
+  /--
+  Any kind of pending synthetic metavariable can be postponed.
+  Universe constrains may also be postponed.
+  -/
+  | yes
+  /--
+  Pending synthetic metavariables cannot be postponed.
+  -/
+  | no
+  /--
+  Synthectic metavariables associated with type class resolution can be postponed.
+  Motivation: this kind of metavariable are not synthethic opaque, and can be assigned by `isDefEq`.
+  Unviverse constraints can also be postponed.
+  -/
+  | «partial»
+  deriving Inhabited, Repr, BEq
+
+def PostponeBehavior.ofBool : Bool → PostponeBehavior
+  | true  => .yes
+  | false => .no
+
 mutual
 
   /--
@@ -321,7 +347,7 @@ mutual
           -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
           withTacticInfoContext tacticCode[0] do
             evalTactic code
-        synthesizeSyntheticMVars (mayPostpone := false)
+        synthesizeSyntheticMVars (postpone := .no)
       unless remainingGoals.isEmpty do
         if report then
           reportUnsolvedGoals remainingGoals
@@ -388,25 +414,27 @@ mutual
     return numSyntheticMVars != remainingPendingMVars.length
 
   /--
-    Try to process pending synthetic metavariables. If `mayPostpone == false`,
-    then `pendingMVars` is `[]` after executing this method.
+    Try to process pending synthetic metavariables.
+
+    If `postpone == .no`,then `pendingMVars` is `[]` after executing this method.
+    If `postpone == .partial`, then `pendingMVars` contains only `.tc` and `.coe` kinds.
 
     It keeps executing `synthesizeSyntheticMVarsStep` while progress is being made.
-    If `mayPostpone == false`, then it applies default instances to `SyntheticMVarKind.typeClass` (if available)
+    If `postpone != .yes`, then it applies default instances to `SyntheticMVarKind.typeClass` (if available)
     metavariables that are still unresolved, and then tries to resolve metavariables
-    with `mayPostpone == false`. That is, we force them to produce error messages and/or commit to
-    a "best option". If, after that, we still haven't made progress, we report "stuck" errors.
+    with `postponeOnError == false`. That is, we force them to produce error messages and/or commit to
+    a "best option". If, after that, we still haven't made progress, we report "stuck" errors If `postpone == .no`.
 
     Remark: we set `ignoreStuckTC := true` when elaborating `simp` arguments. Then,
     pending TC problems become implicit parameters for the simp theorem.
   -/
-  partial def synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := false) : TermElabM Unit := do
+  partial def synthesizeSyntheticMVars (postpone := PostponeBehavior.yes) (ignoreStuckTC := false) : TermElabM Unit := do
     let rec loop (_ : Unit) : TermElabM Unit := do
       withRef (← getSomeSyntheticMVarsRef) <| withIncRecDepth do
         unless (← get).pendingMVars.isEmpty do
           if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then
             loop ()
-          else if !mayPostpone then
+          else if postpone != .yes then
             /- Resume pending metavariables with "elaboration postponement" disabled.
                We postpone elaboration errors in this step by setting `postponeOnError := true`.
                Example:
@@ -431,48 +459,58 @@ mutual
               loop ()
             else if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := true) then
               loop ()
-            else
+            else if postpone == .no then
               reportStuckSyntheticMVars ignoreStuckTC
     loop ()
-    unless mayPostpone do
+    if postpone == .no then
      processPostponedUniverseContraints
 end
 
 def synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := false) : TermElabM Unit :=
-  synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := ignoreStuckTC)
+  synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := ignoreStuckTC)
 
 /-- Keep invoking `synthesizeUsingDefault` until it returns false. -/
 private partial def synthesizeUsingDefaultLoop : TermElabM Unit := do
   if (← synthesizeUsingDefault) then
-    synthesizeSyntheticMVars (mayPostpone := true)
+    synthesizeSyntheticMVars (postpone := .yes)
     synthesizeUsingDefaultLoop
 
 def synthesizeSyntheticMVarsUsingDefault : TermElabM Unit := do
-  synthesizeSyntheticMVars (mayPostpone := true)
+  synthesizeSyntheticMVars (postpone := .yes)
   synthesizeUsingDefaultLoop
 
-private partial def withSynthesizeImp {α} (k : TermElabM α) (mayPostpone : Bool) (synthesizeDefault : Bool) : TermElabM α := do
-  let pendingMVarsSaved := (← get).pendingMVars
-  modify fun s => { s with pendingMVars := [] }
-  try
-    let a ← k
-    synthesizeSyntheticMVars mayPostpone
-    if mayPostpone && synthesizeDefault then
-      synthesizeUsingDefaultLoop
-    return a
-  finally
-    modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
+private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBehavior) : TermElabM α := do
+   let pendingMVarsSaved := (← get).pendingMVars
+   modify fun s => { s with pendingMVars := [] }
+   try
+     let a ← k
+     synthesizeSyntheticMVars (postpone := postpone)
+     if postpone == .yes then
+       synthesizeUsingDefaultLoop
+     return a
+   finally
+     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
 /--
   Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
   If `mayPostpone == false`, then all of them must be synthesized.
   Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
-@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (mayPostpone := false) : m α :=
-  monadMap (m := TermElabM) (withSynthesizeImp · mayPostpone (synthesizeDefault := true)) k
+@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
+  monadMap (m := TermElabM) (withSynthesizeImp · postpone) k
 
-/-- Similar to `withSynthesize`, but sets `mayPostpone` to `true`, and do not use `synthesizeUsingDefault` -/
+private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α := do
+  let pendingMVarsSaved := (← get).pendingMVars
+  modify fun s => { s with pendingMVars := [] }
+  try
+    let a ← k
+    synthesizeSyntheticMVars (postpone := .yes)
+    return a
+  finally
+    modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
+
+/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
 @[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] [Monad m] (k : m α) : m α :=
-  monadMap (m := TermElabM) (withSynthesizeImp · (mayPostpone := true) (synthesizeDefault := false)) k
+  monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 
 /-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
 def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -270,7 +270,7 @@ where
       pure (fvarId, [mvarId])
     if let some typeStx := typeStx? then
       withMainContext do
-        let type ← Term.withSynthesize (mayPostpone := true) <| Term.elabType typeStx
+        let type ← Term.withSynthesize (postpone := .yes) <| Term.elabType typeStx
         let fvar := mkFVar fvarId
         let fvarType ← inferType fvar
         unless (← isDefEqGuarded type fvarType) do

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -29,7 +29,7 @@ def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
   else
     Term.withoutErrToSorry go
 where
-  go := k <* Term.synthesizeSyntheticMVars (mayPostpone := mayPostpone)
+  go := k <* Term.synthesizeSyntheticMVars (postpone := .ofBool mayPostpone)
 
 /-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
 elaboration but not enforced (use `elabTermEnsuringType` to enforce an expected type). -/

src/Lean/Elab/Tactic/Induction.lean

@@ -524,7 +524,7 @@ private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
       return e
   Term.withoutErrToSorry <| Term.withoutHeedElabAsElim do
     let e ← Term.elabTerm stx none (implicitLambda := false)
-    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
     let e := e.eta
     if e.hasMVar then

src/Lean/Elab/Tactic/Meta.lean

@@ -14,7 +14,7 @@ open Term
 def runTactic (mvarId : MVarId) (tacticCode : Syntax) (ctx : Context := {}) (s : State := {}) : MetaM (List MVarId × State) := do
   instantiateMVarDeclMVars mvarId
   let go : TermElabM (List MVarId) :=
-    withSynthesize (mayPostpone := false) do Tactic.run mvarId (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
+    withSynthesize do Tactic.run mvarId (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
   go.run ctx s
 
 end Lean.Elab

src/Lean/Elab/Tactic/Simp.lean

@@ -46,7 +46,7 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
            So, we must not save references to them at `Term.State`.
         -/
         withoutModifyingStateWithInfoAndMessages do
-          Term.withSynthesize (mayPostpone := false) do
+          Term.withSynthesize (postpone := .no) do
             Term.runTactic (report := false) mvar.mvarId! tacticCode
           let result ← instantiateMVars mvar
           if result.hasExprMVar then
@@ -121,7 +121,7 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
 private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let (levelParams, proof) ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
     let e ← Term.elabTerm stx none
-    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
     let e := e.eta
     if e.hasMVar then

tests/lean/run/4051.lean

@@ -0,0 +1,21 @@
+def Array.swaps (a : Array α) : List (Fin a.size × Fin a.size) → Array α
+  | [] => a
+  | (i, j) :: ijs =>
+    have : (a.swap i j).size = a.size := a.size_swap _ _
+
+    swaps (a.swap i j) (ijs.map (fun p => ⟨⟨p.1.1, this.symm ▸ p.1.2⟩, ⟨p.2.1, this.symm ▸ p.2.2⟩⟩))
+termination_by l => l.length
+
+set_option maxHeartbeats 1000 in
+theorem Array.swaps_cancel (a : Array α) (l : List (Fin a.size × Fin a.size)) : a.swaps (l ++ l.reverse) = a :=
+  match l with
+  | [] => sorry
+  | c :: cs =>
+
+    have h : a.size = (a.swaps [c]).size := sorry
+
+    have ih1 : ((a.swaps [c]).swaps ((h ▸ cs) ++ (h ▸ cs).reverse)) = (a.swaps [c]) :=
+      swaps_cancel (a.swaps [c]) (h ▸ cs)
+    sorry
+termination_by l.length
+decreasing_by sorry

tests/lean/run/may_postpone_tc.lean

@@ -0,0 +1,11 @@
+import Lean
+
+open Lean
+def f (xs : List String) : CoreM (Array String) := do
+  let mut found : RBMap _ _ compare := {}
+  let mut result := #[]
+  for x in xs do
+    unless found.contains x do
+      result := result.push x
+      found := found.insert x ()
+  return result