fix: expression tree elaborator for relations now localizes error messages to the LHS or RHS (#3442)

Added `withRef` when processing the LHS or RHS. Without this, in an
expression such as `true = ()` the entire expression would be
highlighted with "type mismatch, `()` has type `Unit` but is expected to
have type `Bool`". Now the error is localized to `()`.

This behavior was pointed out [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/error.20location.20bug/near/422665805).

src/Lean/Elab/Extra.lean

@@ -488,8 +488,10 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
     ```
     We can improve this failure in the future by applying default instances before reporting a type mismatch.
     -/
-    let lhs ← withRef stx[2] <| toTree stx[2]
-    let rhs ← withRef stx[3] <| toTree stx[3]
+    let lhsStx := stx[2]
+    let rhsStx := stx[3]
+    let lhs ← withRef lhsStx <| toTree lhsStx
+    let rhs ← withRef rhsStx <| toTree rhsStx
     let tree := .binop stx .regular f lhs rhs
     let r ← analyze tree none
     trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
@@ -497,10 +499,10 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       -- Use default elaboration strategy + `toBoolIfNecessary`
       let lhs ← toExprCore lhs
       let rhs ← toExprCore rhs
-      let lhs ← toBoolIfNecessary lhs
-      let rhs ← toBoolIfNecessary rhs
+      let lhs ← withRef lhsStx <| toBoolIfNecessary lhs
+      let rhs ← withRef rhsStx <| toBoolIfNecessary rhs
       let lhsType ← inferType lhs
-      let rhs ← ensureHasType lhsType rhs
+      let rhs ← withRef rhsStx <| ensureHasType lhsType rhs
       elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
     else
       let mut maxType := r.max?.get!

tests/lean/binrelTypeMismatch.lean

@@ -0,0 +1,20 @@
+/-!
+# Testing that type mismatch errors for binary operations are localized to the LHS or RHS
+
+Before #3442, the error was placed on the entire expression than just the RHS.
+-/
+
+/-!
+When there's no max type, the ensureHasType failure is localized to the RHS.
+-/
+#check true = ()
+
+/-!
+When there's no max type, toBoolIfNecessary error is localized to LHS.
+-/
+#check ∀ (p : Prop), p == ()
+
+/-!
+When there's no max type, toBoolIfNecessary error is localized to RHS.
+-/
+#check ∀ (p : Prop), () == p

tests/lean/binrelTypeMismatch.lean.expected.out

@@ -0,0 +1,20 @@
+binrelTypeMismatch.lean:10:14-10:16: error: type mismatch
+  ()
+has type
+  Unit : Type
+but is expected to have type
+  Bool : Type
+binrelTypeMismatch.lean:15:21-15:22: error: type mismatch
+  p
+has type
+  Prop : Type
+but is expected to have type
+  Bool : Type
+Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
+binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
+  p
+has type
+  Prop : Type
+but is expected to have type
+  Bool : Type
+Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)