From 3acd77a1544c5f6e485bb36dac04c4d5e02e4b4f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 9 Mar 2024 07:30:47 -0800 Subject: [PATCH] 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 | 21 ++++++++++++---- tests/lean/issue2260.lean.expected.out | 7 ++++++ .../mulcommErrorMessage.lean.expected.out | 6 +++++ tests/lean/run/haveTactic.lean | 24 +++++++++++++++++++ tests/lean/struct1.lean | 4 ++-- 5 files changed, 56 insertions(+), 6 deletions(-) create mode 100644 tests/lean/run/haveTactic.lean diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 3fe086dd9c..c1abb89cb5 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/tests/lean/issue2260.lean.expected.out b/tests/lean/issue2260.lean.expected.out index 66e493b51c..fdcd0e62cb 100644 --- a/tests/lean/issue2260.lean.expected.out +++ b/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 diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out index 11c697d680..c84c427000 100644 --- a/tests/lean/mulcommErrorMessage.lean.expected.out +++ b/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 diff --git a/tests/lean/run/haveTactic.lean b/tests/lean/run/haveTactic.lean new file mode 100644 index 0000000000..54edb02fb6 --- /dev/null +++ b/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 diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean index f6cc3037f4..143da10cc0 100644 --- a/tests/lean/struct1.lean +++ b/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 :=