feat: improve let error locality

src/Lean/Elab/Binders.lean

@@ -546,13 +546,13 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     if useLetExpr then
       withLetDecl id.getId type val fun x => do
         addLocalVarInfo id x
-        let body ← elabTerm body expectedType?
+        let body ← elabTermEnsuringType body expectedType?
         let body ← instantiateMVars body
         mkLetFVars #[x] body
     else
       let f ← withLocalDecl id.getId BinderInfo.default type fun x => do
         addLocalVarInfo id x
-        let body ← elabTerm body expectedType?
+        let body ← elabTermEnsuringType body expectedType?
         let body ← instantiateMVars body
         mkLambdaFVars #[x] body
       pure <| mkApp f val

tests/lean/have.lean

@@ -1,2 +1,7 @@
 example : False :=
   have False := _
+
+example : 5 = 3 :=
+  have t : True := _
+  have f : 5 = 6 := _
+  f

tests/lean/have.lean.expected.out

@@ -1,4 +1,10 @@
-have.lean:3:0: error: unexpected end of input
+have.lean:4:0: error: expected term
 have.lean:2:16-2:17: error: don't know how to synthesize placeholder
 context:
 ⊢ False
+have.lean:7:2-7:3: error: type mismatch
+  f
+has type
+  5 = 6 : Prop
+but is expected to have type
+  5 = 3 : Prop