From bdbab653fdccd1cf04a7af3ecb138a76daa914fb Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 28 Nov 2022 14:29:17 -0800
Subject: [PATCH] fix: synthesize tc instances before propagating expected type

---
 src/Lean/Elab/App.lean   | 28 ++++++++++++++++++++++------
 tests/lean/run/1892.lean | 14 ++++++++++++++
 2 files changed, 36 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/1892.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 48339fae33..edc7fb78ba 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -164,19 +164,33 @@ abbrev M := ReaderT Context (StateRefT State TermElabM)
 private def addInstMVar (mvarId : MVarId) : M Unit :=
   modify fun s => { s with instMVars := s.instMVars.push mvarId }
 
+/--
+  Try to synthesize metavariables are `instMVars` using type class resolution.
+  The ones that cannot be synthesized yet stay in the `instMVars` list.
+  Remark: we use this method
+    - before trying to apply coercions to function,
+    - before unifying the expected type.
+-/
+def trySynthesizeAppInstMVars : M Unit := do
+  let instMVars ← (← get).instMVars.filterM fun instMVar => do
+    unless (← instantiateMVars (← inferType (.mvar instMVar))).isMVar do try
+      if (← synthesizeInstMVarCore instMVar) then
+        return false
+      catch _ => pure ()
+    return true
+  modify ({ · with instMVars })
+
 /--
   Try to synthesize metavariables are `instMVars` using type class resolution.
   The ones that cannot be synthesized yet are registered.
-  Remark: we use this method before trying to apply coercions to function. -/
+-/
 def synthesizeAppInstMVars : M Unit := do
-  let s ← get
-  let instMVars := s.instMVars
-  modify fun s => { s with instMVars := #[] }
-  Term.synthesizeAppInstMVars instMVars s.f
+  Term.synthesizeAppInstMVars (← get).instMVars (← get).f
+  modify ({ · with instMVars := #[] })
 
 /-- fType may become a forallE after we synthesize pending metavariables. -/
 private def synthesizePendingAndNormalizeFunType : M Unit := do
-  synthesizeAppInstMVars
+  trySynthesizeAppInstMVars
   synthesizeSyntheticMVars
   let s ← get
   let fType ← whnfForall s.fType
@@ -348,6 +362,7 @@ private def propagateExpectedType (arg : Arg) : M Unit := do
           | some fTypeBody =>
             unless fTypeBody.hasLooseBVars do
               unless (← hasOptAutoParams fTypeBody) do
+                trySynthesizeAppInstMVars
                 trace[Elab.app.propagateExpectedType] "{expectedType} =?= {fTypeBody}"
                 if (← isDefEq expectedType fTypeBody) then
                   /- Note that we only set `propagateExpected := false` when propagation has succeeded. -/
@@ -389,6 +404,7 @@ private def finalize : M Expr := do
     else
       return e
   if let some expectedType := s.expectedType? then
+    trySynthesizeAppInstMVars
     -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
     trace[Elab.app.finalize] "expected type: {expectedType}"
     discard <| isDefEq expectedType eType
diff --git a/tests/lean/run/1892.lean b/tests/lean/run/1892.lean
new file mode 100644
index 0000000000..d273225f95
--- /dev/null
+++ b/tests/lean/run/1892.lean
@@ -0,0 +1,14 @@
+def OrderDual (α : Type u) : Type u := α
+
+variable (α : Type u) [LE α] {a b : α}
+instance : LE (OrderDual α) := ⟨fun x y : α => y ≤ x⟩
+
+theorem foo' (c : α) : a ≤ b := sorry
+
+example : a ≤ b :=
+  foo' (OrderDual α) a
+
+theorem foo : a ≤ b := sorry
+
+example : a ≤ b :=
+  foo (OrderDual α)