From f8e4dce341a2fdc261839adfb4edaa93c0c5b172 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 4 Dec 2025 11:14:19 -0500 Subject: [PATCH 1/2] feat: simpler error message when sorries complicate universe inference --- src/Lean/Elab/MutualInductive.lean | 4 ++++ tests/lean/univInference.lean | 12 +++++++++++ tests/lean/univInference.lean.expected.out | 23 ++++++++++++++++++++++ 3 files changed, 39 insertions(+) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index acffab1b27d4..81caa61f93b6 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -614,6 +614,10 @@ private def collectUniverses (views : Array InductiveView) (r : Level) (rOffset let (_, acc) ← go |>.run {} if !acc.badLevels.isEmpty then withViewTypeRef views do + if indTypes.any (·.ctors.any (·.type.hasSyntheticSorry)) then + throwError "Type cannot be determined: some part of the definition contains an error" + if indTypes.any (·.ctors.any (·.type.hasSorry)) then + throwError "Type cannot be determined: some part of the definition contains `sorry`" let goodPart := Level.addOffset (Level.mkNaryMax acc.levels.toList) rOffset let badPart := Level.mkNaryMax (acc.badLevels.toList.map fun (u, k) => Level.max (Level.ofNat rOffset) (Level.addOffset u (rOffset - k))) let inferred := (Level.max goodPart badPart).normalize diff --git a/tests/lean/univInference.lean b/tests/lean/univInference.lean index 40b16d73fe24..67b97102be6b 100644 --- a/tests/lean/univInference.lean +++ b/tests/lean/univInference.lean @@ -90,3 +90,15 @@ def ex7 (h : Stx = Nat) : True := trivial end Induct + +inductive Sorry1 where + | x (a : Bool) + | y (b : sorry) + +inductive Sorry2 where + | x (a : Array Sorry2) + | y (b : sorry) + +inductive Sorry3 where + | x (a : Array Sorry3) + | y {x} (b : x Err3) diff --git a/tests/lean/univInference.lean.expected.out b/tests/lean/univInference.lean.expected.out index 7e6a36532b30..994eb89a5421 100644 --- a/tests/lean/univInference.lean.expected.out +++ b/tests/lean/univInference.lean.expected.out @@ -31,3 +31,26 @@ univInference.lean:81:48-81:62: error: Invalid universe polymorphic resulting ty Sort (max u v) Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _` +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:94:0-96:17: warning: declaration uses 'sorry' +univInference.lean:98:0-100:17: error: Type cannot be determined: some part of the definition contains `sorry` +univInference.lean:104:15-104:21: error: Function expected at + x +but this term has type + ?m + +Note: Expected a function because this term is being applied to the argument + Err3 +univInference.lean:102:0-104:22: error: Type cannot be determined: some part of the definition contains an error From aa354493a1be62b30caaf8edaec290d514b60587 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 4 Dec 2025 16:57:44 -0500 Subject: [PATCH 2/2] Test: always give a warning for autobound implicits. This may be more difficult than desired. --- src/Lean/Elab/App.lean | 9 ++- src/Lean/Elab/ErrorUtils.lean | 61 ++++++++++++++----- src/Lean/Elab/SyntheticMVars.lean | 8 +-- src/Lean/Elab/Term/TermElabM.lean | 50 ++++++++++++++- src/Lean/Message.lean | 9 +++ tests/lean/302.lean.expected.out | 2 + tests/lean/3989_1.lean.expected.out | 2 + tests/lean/3989_2.lean.expected.out | 2 + .../autoBoundImplicits1.lean.expected.out | 4 +- .../autoBoundImplicits3.lean.expected.out | 4 +- .../autoBoundPostponeLoop.lean.expected.out | 2 + tests/lean/run/4920.lean | 2 + tests/lean/univInference.lean | 2 +- tests/lean/univInference.lean.expected.out | 6 +- .../DiamondExampleA/Ring/Lemmas.lean | 2 +- 15 files changed, 138 insertions(+), 27 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 3087bd867aab..1695f6e5d613 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -240,6 +240,11 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do let validNames ← getFoundNamedArgs let fnName? := if f.isConst then some f.constName! else none throwInvalidNamedArg namedArg fnName? validNames +/- + let ctx ← readThe Term.Context + withTraceNode `Elab (fun _ => pure m!"throwinerror {s.f} {ctx.autoBoundImplicitContext.map (·.boundVariables.toArray)}") do + logInfo m!"quirky {repr s.f} {ctx.autoBoundImplicitContext.isSome}" +-/ -- Help users see if this is actually due to an indentation mismatch/other parsing mishaps: let extra := if let some (arg : Arg) := s.args[0]? then .note m!"Expected a function because this term is being applied to the argument\ @@ -1338,9 +1343,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which has no fields." let tupleHint ← mkTupleHint eType idx ref throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; \ - {numFields.plural "the only valid index is 1" s!"it must be between 1 and {numFields}"}" + {plural numFields "the only valid index is 1" s!"it must be between 1 and {numFields}"}" ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \ - {numFields} field{numFields.plural}" + {numFields} field{plural numFields}" ++ tupleHint | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do let env ← getEnv diff --git a/src/Lean/Elab/ErrorUtils.lean b/src/Lean/Elab/ErrorUtils.lean index c9397d2801f7..c219764a176e 100644 --- a/src/Lean/Elab/ErrorUtils.lean +++ b/src/Lean/Elab/ErrorUtils.lean @@ -6,8 +6,9 @@ Authors: Rob Simmons module prelude -import Init.Notation -import Init.Data.String +import Lean.Message + +namespace Lean /-- Translate numbers (1, 2, 3, 212, 322 ...) to ordinals with appropriate English-language names for @@ -35,6 +36,24 @@ def _root_.Nat.toOrdinal : Nat -> String else s!"{n}th" +class HasOxfordStrings α where + emp : α + and : α + comma : α + commaAnd : α + +instance : HasOxfordStrings String where + emp := "" + and := " and " + comma := ", " + commaAnd := ", and " + +instance : HasOxfordStrings MessageData where + emp := "" + and := " and " + comma := ", " + commaAnd := ", and " + /-- Make an oxford-comma-separated list of strings. @@ -42,24 +61,38 @@ Make an oxford-comma-separated list of strings. - `["eats", "shoots"].toOxford == "eats and shoots"` - `["eats", "shoots", "leaves"] == "eats, shoots, and leaves"` -/ -def _root_.List.toOxford : List String -> String - | [] => "" +def toOxford [Append α] [HasOxfordStrings α] : List α -> α + | [] => HasOxfordStrings.emp | [a] => a - | [a, b] => a ++ " and " ++ b - | [a, b, c] => a ++ ", " ++ b ++ ", and " ++ c - | a :: as => a ++ ", " ++ toOxford as + | [a, b] => a ++ HasOxfordStrings.and ++ b + | [a, b, c] => a ++ HasOxfordStrings.comma ++ b ++ HasOxfordStrings.commaAnd ++ c + | a :: as => a ++ HasOxfordStrings.comma ++ toOxford as + +class HasPluralDefaults α where + singular : α + plural : α → α + +instance : HasPluralDefaults String where + singular := "" + plural := (· ++ "s") + +instance : HasPluralDefaults MessageData where + singular := .nil + plural := (m!"{·}s") /-- Give alternative forms of a string if the `count` is 1 or not. - - `(1).plural == ""` - - `(2).plural == "s"` - - `(1).plural "wug" == "wug"` - - `(2).plural "wug" == "wugs"` - - `(1).plural "it" "they" == "it"` - - `(2).plural "it" "they" == "they"` + - `(1) |> plural == ""` + - `(2) |> plural == "s"` + - `(1) |> plural "wug" == "wug"` + - `(2) |> plural "wug" == "wugs"` + - `(1) |> plural "it" "they" == "it"` + - `(2) |> plural "it" "they" == "they"` -/ -def _root_.Nat.plural (count : Nat) (singular : String := "") (plural : String := singular ++ "s") := +def plural [HasPluralDefaults α] (count : Nat) + (singular : α := HasPluralDefaults.singular) + (plural : α := HasPluralDefaults.plural singular) := if count = 1 then singular else diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 147d18447dfc..9723d2175e18 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -262,17 +262,17 @@ def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option M -- Formulate error message let containMVars := if simpleMVars then - nStuck.plural "is a metavariable" "are metavariables" + plural nStuck "is a metavariable" "are metavariables" else - nStuck.plural "contains metavariables" "contain metavariables" + plural nStuck "contains metavariables" "contain metavariables" let theTypeArguments := if args.length = 1 then "the type argument" else - s!"the {(stuckArguments.toList.map (·.succ.toOrdinal)).toOxford} type {nStuck.plural "argument" "arguments"}" + s!"the {(stuckArguments.toList.map (·.succ.toOrdinal)) |> toOxford} type {plural nStuck "argument" "arguments"}" - return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {nStuck.plural "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass." + return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {plural nStuck "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass." ++ .hint' m!"Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `{MessageData.ofConstName ``Nat}`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.") /-- diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index 45355bf1ca39..bf8ee9f96130 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -17,6 +17,7 @@ public import Lean.Elab.DeclarationRange public import Lean.Elab.WhereFinally public import Lean.Elab.InfoTree.InlayHints public meta import Lean.Parser.Term +import all Lean.Elab.ErrorUtils @@ -1276,7 +1277,28 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr : elaboration step with exception `ex`. -/ def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do - logException ex + let autoBoundNames ← + (← readThe Term.Context).autoBoundImplicitContext + |>.map (·.boundVariables.toList) + |>.getD [] + |>.mapM (·.fvarId!.getUserName) + if autoBoundNames.length > 0 then + if let .error ref msg := ex then + if msg.isTagged || msg.hasTag (· = `suppressAutoImplicitWarning) then + logException ex + else + let extra := m!"This error occurred after the identifier{plural autoBoundNames.length} \ + {autoBoundNames.map (m!"`{.ofName ·}`") |> toOxford} had been identified as \ + {plural autoBoundNames.length "a free variable" "free variables"} and automatically \ + given {plural autoBoundNames.length "an implicit binding" "implicit bindings"}. \ + {plural autoBoundNames.length m!"Is `{.ofName autoBoundNames[0]!}`" m!"Are those identifiers all"} \ + supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to \ + typos or missing `import` or `open` statements, and this may cause unexpected errors." + logException (.error ref (msg ++ .hint' extra)) + else + logException ex + else + logException ex mkSyntheticSorryFor expectedType? /-- If `mayPostpone == true`, throw `Exception.postpone`. -/ @@ -1885,6 +1907,32 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do withLocalDecl n .implicit (← mkFreshTypeMVar) fun x => do loop (← saveState) (ctx.push x) | none => throw ex + +/- + withTraceNode `Elab (fun _ => pure m!"withabi {ctx.boundVariables.toList.length}") do + try + withReader ({ · with autoBoundImplicitContext := .some ctx }) <| + withSaveAutoImplicitInfoContext k + catch + | ex@(.internal id k) => + if id == autoBoundImplicitExceptionId then + withTraceNode `Elab (fun _ => pure m!"catchInternal {k.getName `localId `x}") do + -- Restore state, declare a new temporary local variable, and try again + let n := k.getName `localId `x + s.restore (restoreInfo := true) + withLocalDecl n .implicit (← mkFreshTypeMVar) fun x => do + loop (← saveState) (ctx.push x) + else throw ex + | .error ref msg => + withTraceNode `Elab (fun _ => pure m!"catchError {ref}") do + logInfo m!"ERROR AFTER BOUND: {ctx.autoImplicitEnabled} {ctx.boundVariables.toArray}" + throwErrorAt ref (msg ++ .hint' m!"warning {ref}") + + | ex => match isAutoBoundImplicitLocalException? ex with + | some n => + | none => throw ex +-/ + loop (← saveState) initCtx else -- Track whether we are in an auto-bound context regardless of whether diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index f8e1ec8fb0fc..9b15a94a9dea 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -172,6 +172,15 @@ def kind : MessageData → Name | tagged n _ => n | _ => .anonymous +/-- +Check if the *outermost* constructor is `.tagged`. +To check if a tag exists anywhere in the message, use `MessageData.hasTag (fun _ => true)`. +-/ +def isTagged : MessageData → Bool + | .tagged .. => true + | _ => false + + def isTrace : MessageData → Bool | withContext _ msg => msg.isTrace | withNamingContext _ msg => msg.isTrace diff --git a/tests/lean/302.lean.expected.out b/tests/lean/302.lean.expected.out index ef98a9c30f8a..56025f2e968d 100644 --- a/tests/lean/302.lean.expected.out +++ b/tests/lean/302.lean.expected.out @@ -5,3 +5,5 @@ but this term has type Note: Expected a function because this term is being applied to the argument 0 + +Hint: This error occurred after the identifiers `m`, `a`, and `t` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. diff --git a/tests/lean/3989_1.lean.expected.out b/tests/lean/3989_1.lean.expected.out index 584f740cf070..c7f1dbb7bf76 100644 --- a/tests/lean/3989_1.lean.expected.out +++ b/tests/lean/3989_1.lean.expected.out @@ -6,3 +6,5 @@ but this term has type Note: Expected a function because this term is being applied to the argument Expr + +Hint: This error occurred after the identifiers `Expr` and `MetaM` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. diff --git a/tests/lean/3989_2.lean.expected.out b/tests/lean/3989_2.lean.expected.out index 0903b387bad8..488254fb9ca5 100644 --- a/tests/lean/3989_2.lean.expected.out +++ b/tests/lean/3989_2.lean.expected.out @@ -6,4 +6,6 @@ but this term has type Note: Expected a function because this term is being applied to the argument Expr + +Hint: This error occurred after the identifiers `Expr` and `MetaM` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. Nat : Type diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out index d3d67c241d94..a8259edbb84b 100644 --- a/tests/lean/autoBoundImplicits1.lean.expected.out +++ b/tests/lean/autoBoundImplicits1.lean.expected.out @@ -1,9 +1,11 @@ myid 10 : Nat myid true : Bool autoBoundImplicits1.lean:16:4-16:11: warning: declaration uses 'sorry' -autoBoundImplicits1.lean:20:25-20:29: error(lean.unknownIdentifier): Unknown identifier `size` +autoBoundImplicits1.lean:20:25-20:29: error: Unknown identifier `size` Note: It is not possible to treat `size` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`. + +Hint: This error occurred after the identifiers `α`, `β`, and `n` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. autoBoundImplicits1.lean:24:23-24:24: error(lean.unknownIdentifier): Unknown identifier `α` Note: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`. diff --git a/tests/lean/autoBoundImplicits3.lean.expected.out b/tests/lean/autoBoundImplicits3.lean.expected.out index e604d06139d1..bfb6a0b4bd1d 100644 --- a/tests/lean/autoBoundImplicits3.lean.expected.out +++ b/tests/lean/autoBoundImplicits3.lean.expected.out @@ -1,6 +1,8 @@ -autoBoundImplicits3.lean:9:29-9:34: error(lean.unknownIdentifier): Unknown identifier `size₂` +autoBoundImplicits3.lean:9:29-9:34: error: Unknown identifier `size₂` Note: It is not possible to treat `size₂` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`. + +Hint: This error occurred after the identifier `α₂` had been identified as a free variable and automatically given an implicit binding. Is `α₂` supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. autoBoundImplicits3.lean:13:24-13:26: error(lean.unknownIdentifier): Unknown identifier `α₃` Note: It is not possible to treat `α₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`. diff --git a/tests/lean/autoBoundPostponeLoop.lean.expected.out b/tests/lean/autoBoundPostponeLoop.lean.expected.out index fc2a505b94a8..12af4a2f4b63 100644 --- a/tests/lean/autoBoundPostponeLoop.lean.expected.out +++ b/tests/lean/autoBoundPostponeLoop.lean.expected.out @@ -3,3 +3,5 @@ autoBoundPostponeLoop.lean:5:12-5:18: error: invalid `▸` notation, argument has type ?m equality expected + +Hint: This error occurred after the identifiers `α`, `β`, and `h` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. diff --git a/tests/lean/run/4920.lean b/tests/lean/run/4920.lean index eb3baa276b15..f76cec74b7f2 100644 --- a/tests/lean/run/4920.lean +++ b/tests/lean/run/4920.lean @@ -14,6 +14,8 @@ has type Vect m A but is expected to have type A + +Hint: This error occurred after the identifiers `A`, `m`, `i`, and `j` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. --- error: Type mismatch: After simplification, term ih diff --git a/tests/lean/univInference.lean b/tests/lean/univInference.lean index 67b97102be6b..c7e195ac732d 100644 --- a/tests/lean/univInference.lean +++ b/tests/lean/univInference.lean @@ -101,4 +101,4 @@ inductive Sorry2 where inductive Sorry3 where | x (a : Array Sorry3) - | y {x} (b : x Err3) + | y (b : x Err3) diff --git a/tests/lean/univInference.lean.expected.out b/tests/lean/univInference.lean.expected.out index 994eb89a5421..54140e685fee 100644 --- a/tests/lean/univInference.lean.expected.out +++ b/tests/lean/univInference.lean.expected.out @@ -46,11 +46,13 @@ univInference.lean:94:0-96:17: warning: declaration uses 'sorry' univInference.lean:94:0-96:17: warning: declaration uses 'sorry' univInference.lean:94:0-96:17: warning: declaration uses 'sorry' univInference.lean:98:0-100:17: error: Type cannot be determined: some part of the definition contains `sorry` -univInference.lean:104:15-104:21: error: Function expected at +univInference.lean:104:11-104:17: error: Function expected at x but this term has type ?m Note: Expected a function because this term is being applied to the argument Err3 -univInference.lean:102:0-104:22: error: Type cannot be determined: some part of the definition contains an error + +Hint: This error occurred after the identifier `x` had been identified as a free variable and automatically given an implicit binding. Is `x` supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors. +univInference.lean:102:0-104:18: error: Type cannot be determined: some part of the definition contains an error diff --git a/tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean b/tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean index 0221e15cd310..4e5421fc1671 100644 --- a/tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean +++ b/tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean @@ -4,7 +4,7 @@ public import DiamondExampleA.Ring.Defs namespace Ring -public theorem add_left_comm [Ring α] : ∀ a b c : α, a + (b + c) = b + (a + c) := by +public theorem poorly_named_lemma [Ring α] : ∀ a b c : α, a + (b + c) = b + (a + c) := by intros a b c rw [← add_assoc a b c] rw [add_comm a b]