reduce breakage related to coerce?

Author: datokrat

src/Lean/Elab/SyntheticMVars.lean

@@ -574,7 +574,7 @@ mutual
         if (← occursCheck mvarId e) then
           mvarId.assign e
           return true
-      if let .some (coerced, expandedCoeDecls) ← coerce? e expectedType then
+      if let .some (coerced, expandedCoeDecls) ← coerceCollectingNames? e expectedType then
         pushInfoLeaf (.ofCustomInfo {
           stx := mvarSyntheticDecl.stx
           value := Dynamic.mk <| CoeExpansionTrace.mk expandedCoeDecls

src/Lean/Elab/Tactic/NormCast.lean

@@ -43,7 +43,7 @@ def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
 
 /-- Constructs the expression `(e : ty)`. -/
 def mkCoe (e : Expr) (ty : Expr) : MetaM Expr := do
-  let .some (e', _) ← coerce? e ty | failure
+  let .some e' ← coerce? e ty | failure
   return e'
 
 /--

src/Lean/Elab/Term/TermElabM.lean

@@ -1193,7 +1193,7 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
   try
     withoutMacroStackAtErr do
-      match ← coerce? e expectedType with
+      match ← coerceCollectingNames? e expectedType with
       | .some (eNew, expandedCoeDecls) =>
         pushInfoLeaf (.ofCustomInfo {
           stx := ← getRef

src/Lean/Meta/Coe.lean

@@ -252,7 +252,7 @@ or `.undef` if we need more metavariable assignments.
 `appliedCoeDecls` is a list of names representing the names of the `Coe` instances that were
 applied.
 -/
-def coerce? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) := do
+def coerceCollectingNames? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) := do
   if let some lifted ← coerceMonadLift? expr expectedType then
     return .some (lifted, [])
   if (← whnfR expectedType).isForall then
@@ -261,4 +261,16 @@ def coerce? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) :=
         return .some (fn, [])
   coerceSimple? expr expectedType
 
+/--
+Coerces `expr` to the type `expectedType`.
+Returns `.some coerced` on successful coercion,
+`.none` if the expression cannot by coerced to that type,
+or `.undef` if we need more metavariable assignments.
+-/
+def coerce? (expr expectedType : Expr) : MetaM (LOption Expr) := do
+  match ← coerceCollectingNames? expr expectedType with
+  | .some (result, _) => return .some result
+  | .none => return .none
+  | .undef => return .undef
+
 end Lean.Meta