fix: make elabTermEnsuringType respect errToSorry when there is a…

… type mismatch (#3633)

Floris van Doorn [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/have.20tactic.20error.20recovery/near/425283053)
that it is confusing that the `have : T := e` tactic completely fails if
the body `e` is not of type `T`. This is in contrast to `have : T := by
exact e`, which does not completely fail when `e` is not of type `T`.

This ends up being caused by `elabTermEnsuringType` throwing an error
when it fails to insert a coercion. Now, it detects this case, and it
checks the `errToSorry` flag to decide whether to throw the error or to
log the error and insert a `sorry`.

This is justified by `elabTermEnsuringType` being a frontend to
`elabTerm`, which inserts `sorry` on error.

An alternative would be to make `ensureType` respect `errToSorry`, but
there exists code that expects being able to catch when `ensureType`
fails. Making such code manipulate `errToSorry` seems error prone, and
this function is not a main entry point to the term elaborator, unlike
`elabTermEnsuringType`.

src/Lean/Elab/Term.lean

@@ -793,10 +793,10 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
     | _            => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
 
 /--
-  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
-  If they are not, then try coercions.
+If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.
 
-  Argument `f?` is used only for generating error messages. -/
+Argument `f?` is used only for generating error messages when inserting coercions fails.
+-/
 def ensureHasType (expectedType? : Option Expr) (e : Expr)
     (errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr := do
   let some expectedType := expectedType? | return e
@@ -1432,9 +1432,22 @@ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr)
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
   withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx
 
+/--
+Similar to `Lean.Elab.Term.elabTerm`, but ensures that the type of the elaborated term is `expectedType?`
+by inserting coercions if necessary.
+
+If `errToSorry` is true, then if coercion insertion fails, this function returns `sorry` and logs the error.
+Otherwise, it throws the error.
+-/
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
-  withRef stx <| ensureHasType expectedType? e errorMsgHeader?
+  try
+    withRef stx <| ensureHasType expectedType? e errorMsgHeader?
+  catch ex =>
+    if (← read).errToSorry && ex matches .error .. then
+      exceptionToSorry ex expectedType?
+    else
+      throw ex
 
 /-- Execute `x` and return `some` if no new errors were recorded or exceptions were thrown. Otherwise, return `none`. -/
 def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do

tests/lean/issue2260.lean.expected.out

@@ -13,3 +13,10 @@ The termination argument has type
   DNat i : Type
 but is expected to have type
   Nat : Type
+issue2260.lean:26:15-26:21: error: failed to prove termination, possible solutions:
+  - Use `have`-expressions to prove the remaining goals
+  - Use `termination_by` to specify a different well-founded relation
+  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+n✝ : Nat
+n : DNat n✝
+⊢ sorryAx Nat true < 1 + n✝ + sizeOf n

tests/lean/mulcommErrorMessage.lean.expected.out

@@ -14,6 +14,12 @@ has type
   true = true : Prop
 but is expected to have type
   true = false : Prop
+mulcommErrorMessage.lean:12:22-12:25: error: type mismatch
+  rfl
+has type
+  false = false : Prop
+but is expected to have type
+  false = true : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
   fun a b => ?m a b
 has type

tests/lean/run/haveTactic.lean

@@ -0,0 +1,24 @@
+/-!
+# Tests for the `have` tactic.
+-/
+
+/-!
+If the body of a `have` fails to elaborate, the tactic completes with a `sorry` for the proof.
+-/
+/--
+error: type mismatch
+  False.elim
+has type
+  False → ?m.6 : Sort ?u.5
+but is expected to have type
+  True : Prop
+---
+info: h : True
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  have h : True :=
+    False.elim
+  trace_state
+  assumption

tests/lean/struct1.lean

@@ -31,13 +31,13 @@ structure S :=
 structure S extends A Nat :=
 (x : Nat) -- error
 
-structure S extends A Nat :=
+structure S' extends A Nat :=
 (x := true) -- error type mismatch
 
 structure S extends A Nat :=
 (x : Bool := true) -- error omit type
 
-structure S :=
+structure S'' :=
 (x : Nat := true) -- error type mismatch
 
 private structure S :=