From 6c1f8a8a63f1f65bda4e45a80dba4ba768c32e59 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 6 Aug 2024 15:27:51 -0700 Subject: [PATCH] fix: ensure autoparam errors have correct positions (#4926) Autoparam tactic scripts have no source positions, which until recently made it so that any errors or messages would be logged at the current ref, which was the application or structure instance being elaborated. However, with the new incrementality features the ref is now carefully managed to avoid leakage of outside data. This inhibits the elaborator's ref from being used for the tactic's ref, causing messages to be placed at the beginning of the file rather than on the syntax that triggered the autoparam. To fix this, now the elaborators insert the ref's source position everywhere into the autoparam tactic script. If in the future messages for synthetic tactics appear at the tops of files in other contexts, we should consider an approach where `Lean.Elab.Term.withReuseContext` uses something like `replaceRef` to set the ref while disabling incrementality when the tactic does not contain source position information. Closes #4880 --- src/Lean/Elab/App.lean | 20 ++++++++--- src/Lean/Elab/StructInst.lean | 4 +++ tests/lean/interactive/4880.lean | 36 +++++++++++++++++++ tests/lean/interactive/4880.lean.expected.out | 32 +++++++++++++++++ 4 files changed, 87 insertions(+), 5 deletions(-) create mode 100644 tests/lean/interactive/4880.lean create mode 100644 tests/lean/interactive/4880.lean.expected.out diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 4c49d4c792d4..ce07129b45f9 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -541,7 +541,7 @@ mutual /-- Process a `fType` of the form `(x : A) → B x`. This method assume `fType` is a function type -/ - private partial def processExplictArg (argName : Name) : M Expr := do + private partial def processExplicitArg (argName : Name) : M Expr := do match (← get).args with | arg::args => if (← anyNamedArgDependsOnCurrent) then @@ -586,6 +586,16 @@ mutual | Except.ok tacticSyntax => -- TODO(Leo): does this work correctly for tactic sequences? let tacticBlock ← `(by $(⟨tacticSyntax⟩)) + /- + We insert position information from the current ref into `stx` everywhere, simulating this being + a tactic script inserted by the user, which ensures error messages and logging will always be attributed + to this application rather than sometimes being placed at position (1,0) in the file. + Placing position information on `by` syntax alone is not sufficient since incrementality + (in particular, `Lean.Elab.Term.withReuseContext`) controls the ref to avoid leakage of outside data. + Note that `tacticSyntax` contains no position information itself, since it is erased by `Lean.Elab.Term.quoteAutoTactic`. + -/ + let info := (← getRef).getHeadInfo + let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info) let argNew := Arg.stx tacticBlock propagateExpectedType argNew elabAndAddNewArg argName argNew @@ -615,7 +625,7 @@ mutual This method assume `fType` is a function type -/ private partial def processImplicitArg (argName : Name) : M Expr := do if (← read).explicit then - processExplictArg argName + processExplicitArg argName else addImplicitArg argName @@ -624,7 +634,7 @@ mutual This method assume `fType` is a function type -/ private partial def processStrictImplicitArg (argName : Name) : M Expr := do if (← read).explicit then - processExplictArg argName + processExplicitArg argName else if (← hasArgsToProcess) then addImplicitArg argName else @@ -643,7 +653,7 @@ mutual addNewArg argName arg main else - processExplictArg argName + processExplicitArg argName else let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic addInstMVar arg.mvarId! @@ -668,7 +678,7 @@ mutual | .implicit => processImplicitArg binderName | .instImplicit => processInstImplicitArg binderName | .strictImplicit => processStrictImplicitArg binderName - | _ => processExplictArg binderName + | _ => processExplicitArg binderName else if (← hasArgsToProcess) then synthesizePendingAndNormalizeFunType main diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 53c881507122..cc4706f234ce 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -677,6 +677,10 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term | .error err => throwError err | .ok tacticSyntax => let stx ← `(by $tacticSyntax) + -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`. + -- We add info to get reliable positions for messages from evaluating the tactic script. + let info := field.ref.getHeadInfo + let stx := stx.raw.rewriteBottomUp (·.setInfo info) cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field | _ => if bi == .instImplicit then diff --git a/tests/lean/interactive/4880.lean b/tests/lean/interactive/4880.lean new file mode 100644 index 000000000000..6a463b4cf92a --- /dev/null +++ b/tests/lean/interactive/4880.lean @@ -0,0 +1,36 @@ +/-! +# Ensure autoparam errors are placed at elaboration position + +Before, errors were placed at the beginning of the file. +-/ + + +/-! +Testing `infer_instance`, which defers a typeclass problem beyond the tactic script execution. +-/ +class A + +-- For structure instance elaboration ... +structure B where + h1 : A := by infer_instance + +example : B where + --^ collectDiagnostics + +-- ... and for app elaboration. +def baz (_h1 : A := by infer_instance) : Nat := 1 + +example : Nat := baz + --^ collectDiagnostics + + +/-! +Testing a tactic that immediately throws an error, but incrementality resets the ref +from the syntax for the tactic (which would be a `.missing` position for autoparams). +-/ + +structure B' where + h1 : A := by done + +example : B' where + --^ collectDiagnostics diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out new file mode 100644 index 000000000000..bea102118361 --- /dev/null +++ b/tests/lean/interactive/4880.lean.expected.out @@ -0,0 +1,32 @@ +{"version": 1, + "uri": "file:///4880.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 16, "character": 12}, + "end": {"line": 16, "character": 17}}, + "message": + "failed to synthesize\n A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.", + "fullRange": + {"start": {"line": 16, "character": 12}, + "end": {"line": 16, "character": 17}}}, + {"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 22, "character": 17}, + "end": {"line": 22, "character": 20}}, + "message": + "failed to synthesize\n A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.", + "fullRange": + {"start": {"line": 22, "character": 17}, + "end": {"line": 22, "character": 20}}}, + {"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 34, "character": 13}, + "end": {"line": 34, "character": 18}}, + "message": "unsolved goals\n⊢ A", + "fullRange": + {"start": {"line": 34, "character": 13}, + "end": {"line": 34, "character": 18}}}]}