diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 6bedad5ea8..7d3711b758 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/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 diff --git a/tests/elab/inferInstanceAs.lean b/tests/elab/inferInstanceAs.lean index 3447581d6e..97beeeacc6 100644 --- a/tests/elab/inferInstanceAs.lean +++ b/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 }