chore: improve inferInstanceAs error message on missing expected type and back compat (#13051)

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

src/Lean/Elab/BuiltinTerm.lean

@@ -315,9 +315,16 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => panic! "resolveId? returned an unexpected expression"
 
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
-  let expectedType ← tryPostponeIfHasMVars expectedType? "`inferInstanceAs` failed"
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
+  if !backward.inferInstanceAs.wrap.get (← getOptions) then
+    return (← elabTerm (← `(_root_.inferInstanceAs $(⟨typeStx⟩))) expectedType?)
+
+  let some expectedType ← tryPostponeIfHasMVars? expectedType? |
+    throwError (m!"`inferInstanceAs` failed, expected type contains metavariables{indentD expectedType?}" ++
+      .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
+        instance translation. If you do not intend to transport instances between two types, \
+        consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
   let type ← withSynthesize (postpone := .yes) <| elabType typeStx
   -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
   discard <| isDefEq type expectedType

tests/elab/inferInstanceAs.lean

@@ -13,6 +13,12 @@ def D := I
 
 instance : C D := inferInstanceAs (C I)
 
+-- We can still use it as an `inferInstance` synonym in the old mode
+set_option backward.inferInstanceAs.wrap false in
+/-- info: «inferInstanceAs» (C D) : C D -/
+#guard_msgs in
+#check inferInstanceAs (C D)
+
 /--
 info: @[implicit_reducible] private def instCD : C D :=
 { c := instCD._aux_1 }