feat: show signature elaboration errors on body parse error (#4267)

Fixes #3556

---------

Co-authored-by: Joachim Breitner <[email protected]>

Author: Kha

src/Lean/Elab/DefView.lean

@@ -84,10 +84,10 @@ instance : Language.ToSnapshotTree HeaderProcessedSnapshot where
 /-- State before elaboration of a mutual definition. -/
 structure DefParsed where
   /--
-  Input substring uniquely identifying header elaboration result given the same `Environment`.
-  If missing, results should never be reused.
+  Unstructured syntax object comprising the full "header" of the definition from the modifiers
+  (incl. docstring) up to the value, used for determining header elaboration reuse.
   -/
-  headerSubstr? : Option Substring
+  fullHeaderRef : Syntax
   /-- Elaboration result, unless fatal exception occurred. -/
   headerProcessedSnap : SnapshotTask (Option HeaderProcessedSnapshot)
 deriving Nonempty
@@ -106,6 +106,11 @@ end Snapshots
 structure DefView where
   kind          : DefKind
   ref           : Syntax
+  /--
+  An unstructured syntax object that comprises the "header" of the definition, i.e. everything up
+  to the value. Used as a more specific ref for header elaboration.
+  -/
+  headerRef     : Syntax
   modifiers     : Modifiers
   declId        : Syntax
   binders       : Syntax
@@ -132,20 +137,20 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[2]
   let modifiers       := modifiers.addAttribute { name := `inline }
   let modifiers       := modifiers.addAttribute { name := `reducible }
-  { ref := stx, kind := DefKind.abbrev, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3] }
 
 def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
   let (binders, type) := expandOptDeclSig stx[2]
   let deriving? := if stx[4].isNone then none else some stx[4][1].getSepArgs
-  { ref := stx, kind := DefKind.def, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.def, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3], deriving? }
 
 def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "theorem " >> declId >> declSig >> declVal
   let (binders, type) := expandDeclSig stx[2]
-  { ref := stx, kind := DefKind.theorem, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.theorem, modifiers,
     declId := stx[1], binders, type? := some type, value := stx[3] }
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
@@ -166,7 +171,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
       trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}"
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
   return {
-    ref := stx, kind := DefKind.def, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.def, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[5]
   }
 
@@ -179,7 +184,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
       let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%)
       `(Parser.Command.declValSimple| := $val)
   return {
-    ref := stx, kind := DefKind.opaque, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.opaque, modifiers := modifiers,
     declId := stx[1], binders := binders, type? := some type, value := val
   }
 
@@ -188,7 +193,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[1]
   let id              := mkIdentFrom stx `_example
   let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
-  { ref := stx, kind := DefKind.example, modifiers := modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:2], kind := DefKind.example, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[2] }
 
 def isDefLike (stx : Syntax) : Bool :=

src/Lean/Elab/MutualDef.lean

@@ -131,7 +131,7 @@ private def elabHeaders (views : Array DefView)
     (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot)))
     (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) :
     TermElabM (Array DefViewElabHeader) := do
-  let expandedDeclIds ← views.mapM fun view => withRef view.ref do
+  let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
     Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
   withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do
     let mut headers := #[]
@@ -181,9 +181,13 @@ private def elabHeaders (views : Array DefView)
           reuseBody := false
 
       let header ← withRestoreOrSaveFull reusableResult? fun save => do
-        withRef view.ref do
-        addDeclarationRanges declName view.ref
+        withRef view.headerRef do
+        addDeclarationRanges declName view.ref  -- NOTE: this should be the full `ref`
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
+        -- do not hide header errors on partial body syntax as these two elaboration parts are
+        -- sufficiently independent
+        withTheReader Core.Context ({ · with suppressElabErrors :=
+          view.headerRef.hasMissing && !Command.showPartialSyntaxErrors.get (← getOptions) }) do
         withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
@@ -961,40 +965,41 @@ end Term
 namespace Command
 
 def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
+  let opts ← getOptions
   withAlwaysResolvedPromises ds.size fun headerPromises => do
-    let substr? := (mkNullNode ds).getSubstring?
     let snap? := (← read).snap?
     let mut views := #[]
     let mut defs := #[]
+    let mut reusedAllHeaders := true
     for h : i in [0:ds.size], headerPromise in headerPromises do
       let d := ds[i]
       let modifiers ← elabModifiers d[0]
       if ds.size > 1 && modifiers.isNonrec then
         throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
       let mut view ← mkDefView modifiers d[1]
+      let fullHeaderRef := mkNullNode #[d[0], view.headerRef]
       if let some snap := snap? then
-        -- overapproximation: includes previous bodies as well
-        let headerSubstr? := return { (← substr?) with stopPos := (← view.value.getPos?) }
         view := { view with headerSnap? := some {
           old? := do
-            -- transitioning from `Context.snap?` to `DefView.snap?` invariant: if the elaboration
-            -- context and state are unchanged, and the substring from the beginning of the first
-            -- header to the beginning of the current body is unchanged, then the elaboration result for
-            -- this header (which includes state from elaboration of previous headers!) should be
-            -- unchanged.
+            -- transitioning from `Context.snap?` to `DefView.headerSnap?` invariant: if the
+            -- elaboration context and state are unchanged, and the syntax of this as well as all
+            -- previous headers is unchanged, then the elaboration result for this header (which
+            -- includes state from elaboration of previous headers!) should be unchanged.
+            guard reusedAllHeaders
             let old ← snap.old?
             -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
             let old ← old.val.get.toTyped? DefsParsedSnapshot
             let oldParsed ← old.defs[i]?
-            guard <| (← headerSubstr?).sameAs (← oldParsed.headerSubstr?)
+            guard <| fullHeaderRef.structRangeEqWithTraceReuse opts oldParsed.fullHeaderRef
             -- no syntax guard to store, we already did the necessary checks
             return ⟨.missing, oldParsed.headerProcessedSnap⟩
           new := headerPromise
         } }
         defs := defs.push {
-          headerSubstr?
+          fullHeaderRef
           headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
         }
+        reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
       views := views.push view
     if let some snap := snap? then
       -- no non-fatal diagnostics at this point

tests/lean/3989_1.lean.expected.out

@@ -1 +1,5 @@
 3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`
+3989_1.lean:1:22-1:32: error: function expected at
+  MetaM
+term has type
+  ?m

tests/lean/3989_2.lean.expected.out

@@ -1,2 +1,6 @@
 3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`
+3989_2.lean:1:22-1:32: error: function expected at
+  MetaM
+term has type
+  ?m
 Nat : Type

tests/lean/799.lean.expected.out

@@ -1,5 +1,5 @@
-799.lean:3:0-3:11: error: invalid declaration name 'p', there is a section variable with the same name
+799.lean:3:0-3:5: error: invalid declaration name 'p', there is a section variable with the same name
 p : Prop
-799.lean:7:0-7:13: error: invalid declaration name 'p', there is a section variable with the same name
+799.lean:7:0-7:5: error: invalid declaration name 'p', there is a section variable with the same name
 p : Prop
 p : Nat

tests/lean/mutualdef1.lean.expected.out

@@ -1,3 +1,3 @@
-mutualdef1.lean:9:0-11:12: error: invalid mutually recursive definitions, cannot mix theorems and definitions
-mutualdef1.lean:21:0-22:4: error: invalid mutually recursive definitions, cannot mix examples and definitions
-mutualdef1.lean:32:7-34:12: error: invalid mutually recursive definitions, cannot mix unsafe and safe definitions
+mutualdef1.lean:9:0-9:31: error: invalid mutually recursive definitions, cannot mix theorems and definitions
+mutualdef1.lean:21:0-21:13: error: invalid mutually recursive definitions, cannot mix examples and definitions
+mutualdef1.lean:32:7-32:34: error: invalid mutually recursive definitions, cannot mix unsafe and safe definitions

tests/lean/sanitychecks.lean.expected.out

@@ -4,8 +4,8 @@ with errors
 structural recursion cannot be used
 
 well-founded recursion cannot be used, 'unsound' does not take any (non-fixed) arguments
-sanitychecks.lean:4:8-5:10: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
-sanitychecks.lean:7:7-8:10: error: 'unsafe' theorems are not allowed
+sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
+sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
 sanitychecks.lean:10:0-10:23: error: failed to synthesize
   Inhabited False
 use `set_option diagnostics true` to get diagnostic information

tests/lean/syntheticOpaqueReadOnly.lean.expected.out

@@ -1 +1 @@
-false
+false