feat: use Coe in the new frontend

src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean

@@ -70,6 +70,15 @@ withMVarContext instMVar $ catch
     | Exception.ex (Elab.Exception.error errMsg) => do logMessage errMsg; pure true
     | _ => unreachable!)
 
+/--
+  Similar to `synthesizePendingInstMVar`, but generates type mismatch error message. -/
+private def synthesizePendingCoeInstMVar (ref : Syntax) (instMVar : MVarId) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Bool := do
+withMVarContext instMVar $ catch
+  (synthesizeInstMVarCore ref instMVar)
+  (fun ex => match ex with
+    | Exception.ex (Elab.Exception.error errMsg) => throwTypeMismatchError ref expectedType eType e f? errMsg.data
+    | _ => unreachable!)
+
 /--
   Return `true` iff `mvarId` is assigned to a term whose the
   head is not a metavariable. We use this method to process `SyntheticMVarKind.withDefault`. -/
@@ -80,11 +89,12 @@ pure $ !val.getAppFn.isMVar
 /-- Try to synthesize the given pending synthetic metavariable. -/
 private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool :=
 match mvarSyntheticDecl.kind with
-| SyntheticMVarKind.typeClass            => synthesizePendingInstMVar mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId
+| SyntheticMVarKind.typeClass                   => synthesizePendingInstMVar mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId
+| SyntheticMVarKind.coe expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId expectedType eType e f?
 -- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
-| SyntheticMVarKind.withDefault _        => checkWithDefault mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId
-| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId postponeOnError
-| SyntheticMVarKind.tactic tacticCode    => do runTactic mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId tacticCode; pure true
+| SyntheticMVarKind.withDefault _               => checkWithDefault mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId
+| SyntheticMVarKind.postponed macroStack        => resumePostponed macroStack mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId postponeOnError
+| SyntheticMVarKind.tactic tacticCode           => do runTactic mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId tacticCode; pure true
 
 /--
   Try to synthesize the current list of pending synthetic metavariables.
@@ -137,6 +147,10 @@ s.syntheticMVars.forM $ fun mvarSyntheticDecl =>
       mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId;
       logError mvarSyntheticDecl.ref $
         "failed to create type class instance for " ++ indentExpr mvarDecl.type
+  | SyntheticMVarKind.coe expectedType eType e f? =>
+    withMVarContext mvarSyntheticDecl.mvarId $ do
+      mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId;
+      throwTypeMismatchError mvarSyntheticDecl.ref expectedType eType e f? (some ("failed to create type class instance for " ++ indentExpr mvarDecl.type))
   | _ => unreachable! -- TODO handle other cases.
 
 private def getSomeSynthethicMVarsRef : TermElabM Syntax := do

src/Init/Lean/Elab/Term.lean

@@ -38,6 +38,9 @@ structure Context extends Meta.Context :=
 inductive SyntheticMVarKind
 -- typeclass instance search
 | typeClass
+-- Similar to typeClass, but error messages are different,
+-- we use "type mismatch" or "application type mismatch" (when `f?` is some) instead of "failed to synthesize"
+| coe (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr)
 -- tactic block execution
 | tactic (tacticCode : Syntax)
 -- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`)
@@ -550,43 +553,6 @@ ctx       ← read;
 let needReset := ctx.localInstances == mvarDecl.localInstances;
 withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x
 
-/--
-  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
-  If they are not, then try coercions.
-  Return `some e'` if successful, where `e'` may be different from `e` if coercions have been applied,
-  and `none` otherwise
- -/
-def tryEnsureHasType? (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) :=
-match expectedType? with
-| none              => pure (some e)
-| some expectedType =>
-  condM (isDefEq ref eType expectedType)
-    (pure (some e))
-    -- TODO try `HasCoe`
-    (pure none)
-
-/--
-  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
-  If they are not, then try coercions. -/
-def ensureHasTypeAux (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM Expr := do
-e? ← tryEnsureHasType? ref expectedType? eType e;
-match e? with
-| some e => pure e
-| none   =>
-  let msg : MessageData :=
-    "type mismatch" ++ indentExpr e
-    ++ Format.line ++ "has type" ++ indentExpr eType
-    ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType?.get!;
-  throwError ref msg
-
-/--
-  If `expectedType?` is `some t`, then ensure `t` and type of `e` are definitionally equal.
-  If they are not, then try coercions. -/
-def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : TermElabM Expr :=
-match expectedType? with
-| none => pure e
-| _    => do eType ← inferType ref e; ensureHasTypeAux ref expectedType? eType e
-
 /- Try to synthesize metavariable using type class resolution.
    This method assumes the local context and local instances of `instMVar` coincide
    with the current local context and local instances.
@@ -619,6 +585,68 @@ unlessM (synthesizeInstMVarCore ref mvarId) $
   registerSyntheticMVar ref mvarId SyntheticMVarKind.typeClass;
 pure mvar
 
+def throwTypeMismatchError {α} (ref : Syntax) (expectedType : Expr) (eType : Expr) (e : Expr)
+    (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
+let extraMsg : MessageData := match extraMsg? with
+  | none          => Format.nil
+  | some extraMsg => Format.line ++ extraMsg;
+match f? with
+| none =>
+  let msg : MessageData :=
+    "type mismatch" ++ indentExpr e
+    ++ Format.line ++ "has type" ++ indentExpr eType
+    ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType
+    ++ extraMsg;
+  throwError ref msg
+| some f => do
+  env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
+  throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f e { env := env, mctx := mctx, lctx := lctx, opts := opts } ++ extraMsg
+
+/--
+  Try to apply coercion to make sure `e` has type `expectedType`.
+  Relevant definitions:
+  ```
+  class CoeT (α : Sort u) (a : α) (β : Sort v)
+  abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
+  ``` -/
+def tryCoe (ref : Syntax) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Expr := do
+u ← getLevel ref eType;
+v ← getLevel ref expectedType;
+let coeTInstType := mkAppN (mkConst `CoeT [u, v]) #[eType, e, expectedType];
+mvar ← mkFreshExprMVar ref coeTInstType MetavarKind.synthetic;
+let eNew := mkAppN (mkConst `coe [u, v]) #[eType, expectedType, e, mvar];
+let mvarId := mvar.mvarId!;
+catch
+  (do
+    unlessM (synthesizeInstMVarCore ref mvarId) $
+      registerSyntheticMVar ref mvarId (SyntheticMVarKind.coe expectedType eType e f?);
+    pure eNew)
+  (fun ex =>
+    match ex with
+    | Exception.ex (Elab.Exception.error errMsg) => throwTypeMismatchError ref expectedType eType e f? errMsg.data
+    | _ => throwTypeMismatchError ref expectedType eType e f?)
+
+/--
+  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
+  If they are not, then try coercions.
+
+  Argument `f?` is used only for generating error messages. -/
+def ensureHasTypeAux (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) (f? : Option Expr := none) : TermElabM Expr :=
+match expectedType? with
+| none              => pure e
+| some expectedType =>
+  condM (isDefEq ref eType expectedType)
+    (pure e)
+    (tryCoe ref expectedType eType e f?)
+
+/--
+  If `expectedType?` is `some t`, then ensure `t` and type of `e` are definitionally equal.
+  If they are not, then try coercions. -/
+def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : TermElabM Expr :=
+match expectedType? with
+| none => pure e
+| _    => do eType ← inferType ref e; ensureHasTypeAux ref expectedType? eType e
+
 /- =======================================
        Builtin elaboration functions
    ======================================= -/

src/Init/Lean/Elab/TermApp.lean

@@ -47,12 +47,7 @@ instMVars.forM $ fun mvarId =>
 
 private def ensureArgType (ref : Syntax) (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do
 argType ← inferType ref arg;
-arg? ← tryEnsureHasType? ref expectedType argType arg;
-match arg? with
-| some arg => pure arg
-| none     => do
-  env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
-  throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f arg { env := env, mctx := mctx, lctx := lctx, opts := opts }
+ensureHasTypeAux ref expectedType argType arg f
 
 private def elabArg (ref : Syntax) (f : Expr) (arg : Arg) (expectedType : Expr) : TermElabM Expr :=
 match arg with