feat: unique sorries

Motivation: `sorry` should have an indeterminate value so that it's harder to make "fake" theorems about stubbed-out definitions. This PR makes each instance of `sorry` be non-defeq to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting variables to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```

Details:

Adds `Lean.Meta.mkUniqueSorry`, which creates a sorry that is not defeq to any other sorry. It also encodes the source position into the term.

Makes the `sorry` term and `sorry` tactic create unique sorries.

Adds support to the LSP so that "go to definition" on `sorry` in the Infoview goes to the origin of that particular `sorry`.

Fixes `sorry` pretty printing: no more `sorryAx` in the Infoview.

Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`.

pervasive mkUniqueSorry

unique -> labeled sorries. Turns out using unique sorries for elaboration errors can compound the issues. In any case, they can still be labeled.

improves addPPExplicitToExposeDiff when functions are overapplied

fixes mdata bugs in location RPC handler

fixes leanprover#4972

fix tests

revert comment

more unique

src/Init/NotationExtra.lean

@@ -168,11 +168,6 @@ end Lean
   | `($(_) $c $t $e) => `(if $c then $t else $e)
   | _                => throw ()
 
-@[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `($(_) $_)    => `(sorry)
-  | `($(_) $_ $_) => `(sorry)
-  | _             => throw ()
-
 @[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
   | _             => throw ()

src/Init/Prelude.lean

@@ -645,14 +645,13 @@ set_option linter.unusedVariables.funArgs false in
 @[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
 
 /--
-Auxiliary axiom used to implement `sorry`.
+Auxiliary axiom used to implement the `sorry` term and tactic.
 
-The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`. This is a
-proof of anything, which is intended for stubbing out incomplete parts of a
-proof while still having a syntactically correct proof skeleton. Lean will give
-a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but
-you can double check if a theorem depends on `sorry` by using
-`#print axioms my_thm` and looking for `sorryAx` in the axiom list.
+The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`.
+It intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
+Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
+but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
+of the `#print axioms my_thm` command.
 
 The `synthetic` flag is false when written explicitly by the user, but it is
 set to `true` when a tactic fails to prove a goal, or if there is a type error
@@ -661,7 +660,7 @@ suppresses follow-up errors in order to prevent one error from causing a cascade
 of other errors because the desired term was not constructed.
 -/
 @[extern "lean_sorry", never_extract]
-axiom sorryAx (α : Sort u) (synthetic := false) : α
+axiom sorryAx (α : Sort u) (synthetic : Bool) : α
 
 theorem eq_false_of_ne_true : {b : Bool} → Not (Eq b true) → Eq b false
   | true, h => False.elim (h rfl)

src/Init/Tactics.lean

@@ -408,16 +408,18 @@ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
 syntax (name := acRfl) "ac_rfl" : tactic
 
 /--
-The `sorry` tactic closes the goal using `sorryAx`. This is intended for stubbing out incomplete
-parts of a proof while still having a syntactically correct proof skeleton. Lean will give
-a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but
-you can double check if a theorem depends on `sorry` by using
-`#print axioms my_thm` and looking for `sorryAx` in the axiom list.
+The `sorry` tactic is a temporary placeholder for an incomplete tactic proof,
+closing the main goal using `exact sorry`.
+
+This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton.
+Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it,
+but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output
+of the `#print axioms my_thm` command, which is the axiom used by implementation of `sorry`.
 -/
-macro "sorry" : tactic => `(tactic| exact @sorryAx _ false)
+macro "sorry" : tactic => `(tactic| exact sorry)
 
-/-- `admit` is a shorthand for `exact sorry`. -/
-macro "admit" : tactic => `(tactic| exact @sorryAx _ false)
+/-- `admit` is a synonym for `sorry`. -/
+macro "admit" : tactic => `(tactic| sorry)
 
 /--
 `infer_instance` is an abbreviation for `exact inferInstance`.

src/Lean/Elab/BuiltinNotation.lean

@@ -212,9 +212,9 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
   | `(dbg_trace $arg:term; $body)            => `(dbgTrace (toString $arg) fun _ => $body)
   | _                                        => Macro.throwUnsupported
 
-@[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
-  let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auto params
-  withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
+@[builtin_term_elab «sorry»] def elabSorry : TermElab := fun _ expectedType? => do
+  let type ← expectedType?.getDM mkFreshTypeMVar
+  mkLabeledSorry type (synthetic := false) (unique := true)
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkPairs (elems : Array Term) : MacroM Term :=

src/Lean/Elab/Extra.lean

@@ -581,7 +581,7 @@ def elabDefaultOrNonempty : TermElab :=  fun stx expectedType? => do
       else
         -- It is in the context of an `unsafe` constant. We can use sorry instead.
         -- Another option is to make a recursive application since it is unsafe.
-        mkSorry expectedType false
+        mkLabeledSorry expectedType false (unique := true)
 
 builtin_initialize
   registerTraceClass `Elab.binop

src/Lean/Elab/MutualDef.lean

@@ -1007,7 +1007,7 @@ where
             values.mapM (instantiateMVarsProfiling ·)
           catch ex =>
             logException ex
-            headers.mapM fun header => mkSorry header.type (synthetic := true)
+            headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true)
         let headers ← headers.mapM instantiateMVarsAtHeader
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift

src/Lean/Elab/PreDefinition/Basic.lean

@@ -9,7 +9,6 @@ import Lean.Compiler.NoncomputableAttr
 import Lean.Util.CollectLevelParams
 import Lean.Util.NumObjs
 import Lean.Util.NumApps
-import Lean.PrettyPrinter
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
 import Lean.Meta.Eqns

src/Lean/Elab/PreDefinition/Main.lean

@@ -20,7 +20,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
     let all := preDefs.toList.map (·.declName)
     forallTelescope preDef.type fun xs type => do
       let value ← if useSorry then
-        mkLambdaFVars xs (← mkSorry type (synthetic := true))
+        mkLambdaFVars xs (← withRef preDef.ref <| mkLabeledSorry type (synthetic := true) (unique := true))
       else
         liftM <| mkInhabitantFor preDef.declName xs type
       addNonRec { preDef with
@@ -114,7 +114,7 @@ private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition
 private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do
   let pendingMVarIds ← getMVarsAtPreDef preDef
   if (← logUnassignedUsingErrorInfos pendingMVarIds) then
-    let preDef := { preDef with value := (← mkSorry preDef.type (synthetic := true)) }
+    let preDef := { preDef with value := (← withRef preDef.ref <| mkLabeledSorry preDef.type (synthetic := true) (unique := true)) }
     if (← getMVarsAtPreDef preDef).isEmpty then
       return preDef
     else

src/Lean/Elab/Tactic/Basic.lean

@@ -14,7 +14,7 @@ open Meta
 def admitGoal (mvarId : MVarId) : MetaM Unit :=
   mvarId.withContext do
     let mvarType ← inferType (mkMVar mvarId)
-    mvarId.assign (← mkSorry mvarType (synthetic := true))
+    mvarId.assign (← mkLabeledSorry mvarType (synthetic := true) (unique := true))
 
 def goalsToMessageData (goals : List MVarId) : MessageData :=
   MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -70,7 +70,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
       if let some suggestions ← librarySearch introdGoal then
         if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
         else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
-        mkSorry expectedType (synthetic := true)
+        mkLabeledSorry expectedType (synthetic := true) (unique := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta
         instantiateMVars goal

src/Lean/Elab/Term.lean

@@ -1154,7 +1154,7 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr :
   let expectedType ← match expectedType? with
     | none              => mkFreshTypeMVar
     | some expectedType => pure expectedType
-  mkSyntheticSorry expectedType
+  mkLabeledSorry expectedType (synthetic := true) (unique := false)
 
 /--
   Log the given exception, and create a synthetic sorry for representing the failed
@@ -1260,7 +1260,7 @@ The `tacticCode` syntax is the full `by ..` syntax.
 -/
 def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do
   if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
-    mkSorry type false
+    withRef tacticCode <| mkLabeledSorry type false (unique := true)
   else
     let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
     let mvarId := mvar.mvarId!
@@ -1851,7 +1851,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPo
     withRef stx <| ensureHasType expectedType? e errorMsgHeader?
   catch ex =>
     if (← read).errToSorry && ex matches .error .. then
-      exceptionToSorry ex expectedType?
+      withRef stx <| exceptionToSorry ex expectedType?
     else
       throw ex
 

src/Lean/Meta/AppBuilder.lean

@@ -9,6 +9,7 @@ import Lean.Util.Recognizers
 import Lean.Meta.SynthInstance
 import Lean.Meta.Check
 import Lean.Meta.DecLevel
+import Lean.Data.Lsp.Utf16
 
 namespace Lean.Meta
 
@@ -513,10 +514,65 @@ def mkSome (type value : Expr) : MetaM Expr := do
   let u ← getDecLevel type
   return mkApp2 (mkConst ``Option.some [u]) type value
 
+/--
+Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
+-/
 def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
   let u ← getLevel type
   return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
 
+structure SorryLabelView where
+  module? : Option (Name × Lsp.Range) := none
+
+def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
+  let name :=
+    if let some (mod, range) := view.module? then
+      mod |>.num range.start.line |>.num range.start.character |>.num range.end.line |>.num range.end.character
+    else
+      .anonymous
+  mkFreshUserName (name.str "_unique_sorry")
+
+def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
+  guard <| name.hasMacroScopes
+  let .str name "_unique_sorry" := name.eraseMacroScopes | failure
+  if let .num (.num (.num (.num name startLine) startChar) endLine) endChar := name then
+    return { module? := some (name, ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩) }
+  else
+    failure
+
+/--
+Makes a `sorryAx` that encodes the current ref into the term to support "go to definition" for the `sorry`.
+If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
+-/
+def mkLabeledSorry (type : Expr) (synthetic : Bool) (unique : Bool) : MetaM Expr := do
+  let tag ←
+    if let (some pos, some endPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
+      let range := (← getFileMap).utf8RangeToLspRange ⟨pos, endPos⟩
+      SorryLabelView.encode { module? := (← getMainModule, range) }
+    else
+      SorryLabelView.encode {}
+  if unique then
+    let e ← mkSorry (mkForall `tag .default (mkConst ``Lean.Name) type) synthetic
+    return .app e (toExpr tag)
+  else
+    let e ← mkSorry (mkForall `tag .default (mkConst ``Unit) type) synthetic
+    return .app e (mkApp4 (mkConst ``Function.const [levelOne, levelOne])
+      (mkConst ``Unit) (mkConst ``Lean.Name) (mkConst ``Unit.unit) (toExpr tag))
+
+/--
+Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
+-/
+def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
+  guard <| e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 3
+  let arg := e.getArg! 2
+  if let some tag := arg.name? then
+    SorryLabelView.decode? tag
+  else
+    guard <| arg.isAppOfArity ``Function.const 4
+    guard <| arg.appFn!.appArg!.isAppOfArity ``Unit.unit 0
+    let some tag := arg.appArg!.name? | failure
+    SorryLabelView.decode? tag
+
 /-- Return `Decidable.decide p` -/
 def mkDecide (p : Expr) : MetaM Expr :=
   mkAppOptM ``Decidable.decide #[p, none]
@@ -545,10 +601,6 @@ def mkDefault (α : Expr) : MetaM Expr :=
 def mkOfNonempty (α : Expr) : MetaM Expr := do
   mkAppOptM ``Classical.ofNonempty #[α, none]
 
-/-- Return `sorryAx type` -/
-def mkSyntheticSorry (type : Expr) : MetaM Expr :=
-  return mkApp2 (mkConst ``sorryAx [← getLevel type]) type (mkConst ``Bool.true)
-
 /-- Return `funext h` -/
 def mkFunExt (h : Expr) : MetaM Expr :=
   mkAppM ``funext #[h]

src/Lean/Meta/Tactic/Util.lean

@@ -60,7 +60,7 @@ def _root_.Lean.MVarId.admit (mvarId : MVarId) (synthetic := true) : MetaM Unit
   mvarId.withContext do
     mvarId.checkNotAssigned `admit
     let mvarType ← mvarId.getType
-    let val ← mkSorry mvarType synthetic
+    let val ← mkLabeledSorry mvarType synthetic (unique := true)
     mvarId.assign val
 
 /-- Beta reduce the metavariable type head -/

src/Lean/Parser/Term.lean

@@ -215,7 +215,23 @@ However, in case it is copied and pasted from the Infoview, `⋯` logs a warning
 @[builtin_term_parser] def omission := leading_parser
   "⋯"
 def binderIdent : Parser  := ident <|> hole
-/-- A temporary placeholder for a missing proof or value. -/
+/--
+The `sorry` term is a temporary placeholder for a missing proof or value.
+
+The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
+Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
+but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
+of the `#print axioms my_thm` command, which is the axiom used by implementation of `sorry`.
+
+"Go to definition" on `sorry` will go to the source position where it was introduced.
+
+Each `sorry` is guaranteed to be unique, so for example the following fails:
+```lean
+example : (sorry : Nat) = sorry := rfl -- fails
+```
+
+See also the `sorry` tactic, which is short for `exact sorry`.
+-/
 @[builtin_term_parser] def «sorry» := leading_parser
   "sorry"
 /--

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -221,8 +221,18 @@ def annotateTermInfo (stx : Term) : Delab := do
   pure stx
 
 /--
-Modifies the delaborator so that it annotates the resulting term with the current expression
-position and registers `TermInfo` to associate the term to the current expression.
+Annotates the term with the current expression position and registers `TermInfo`
+to associate the term to the current expression, unless the syntax has a synthetic position
+and associated `Info` already.
+-/
+def annotateTermInfoUnlessAnnotated (stx : Term) : Delab := do
+  if let .synthetic ⟨pos⟩ ⟨pos'⟩ := stx.raw.getHeadInfo then
+    if pos == pos' && (← get).infos.contains pos then
+      return stx
+  annotateTermInfo stx
+
+/--
+Modifies the delaborator so that it annotates the resulting term using `annotateTermInfo`.
 -/
 def withAnnotateTermInfo (d : Delab) : Delab := do
   let stx ← d
@@ -287,11 +297,13 @@ inductive OmissionReason
   | deep
   | proof
   | maxSteps
+  | uniqueSorry
 
 def OmissionReason.toString : OmissionReason → String
   | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
   | proof => "Proof omitted (see option `pp.proofs`)."
   | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
+  | uniqueSorry => "This is a `sorry` term associated to a source position. Use 'Go to definition' to go there."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
   let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
@@ -381,7 +393,7 @@ def omission (reason : OmissionReason) : Delab := do
 partial def delabFor : Name → Delab
   | Name.anonymous => failure
   | k              =>
-    (do annotateTermInfo (← (delabAttribute.getValues (← getEnv) k).firstM id))
+    (do annotateTermInfoUnlessAnnotated (← (delabAttribute.getValues (← getEnv) k).firstM id))
     -- have `app.Option.some` fall back to `app` etc.
     <|> if k.isAtomic then failure else delabFor k.getRoot
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -587,7 +587,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
   else
     let delabHead (insertExplicit : Bool) : Delab := do
       guard <| !insertExplicit
-      withAnnotateTermInfo x
+      withAnnotateTermInfoUnlessAnnotated x
     delabAppCore (n - arity) delabHead (unexpand := false)
 
 @[builtin_delab app]
@@ -1287,6 +1287,33 @@ def delabNameMkStr : Delab := whenPPOption getPPNotation do
 @[builtin_delab app.Lean.Name.num]
 def delabNameMkNum : Delab := delabNameMkStr
 
+@[builtin_delab app.sorryAx]
+def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExplicit do
+  guard <| (← getExpr).getAppNumArgs ≥ 2
+  let sorrySource ← getPPOption getPPSorrySource
+  -- If this is constructed by `Lean.Meta.mkLabeledSorry`, then don't print the unique tag.
+  -- But, if `pp.explicit` is false and `pp.sorrySource` is true, then print a simplified version of the tag.
+  if let some view := isLabeledSorry? (← getExpr) then
+    withOverApp 3 do
+      if let some (module, range) := view.module? then
+        if ← pure sorrySource <||> getPPOption getPPSorrySource then
+          -- LSP line numbers start at 0, so add one to it.
+          -- Technically using the character as the column is incorrect since this is UTF-16 position, but we have no filemap to work with.
+          let posAsName := Name.mkSimple s!"{module}:{range.start.line + 1}:{range.start.character}"
+          let pos := mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{posAsName}"]
+          let src ← withAppArg <| annotateTermInfo pos
+          `(sorry $src)
+        else
+          -- Hack: use omission info so that the first hover gives the sorry source.
+          let stx ← `(sorry)
+          let stx ← annotateCurPos stx
+          addOmissionInfo (← getPos) stx (← getExpr) .uniqueSorry
+          return stx
+      else
+        `(sorry)
+  else
+    withOverApp 2 `(sorry)
+
 open Parser Command Term in
 @[run_builtin_parser_attribute_hooks]
 -- use `termParser` instead of `declId` so we can reuse `delabConst`

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -39,6 +39,11 @@ register_builtin_option pp.match : Bool := {
   group    := "pp"
   descr    := "(pretty printer) disable/enable 'match' notation"
 }
+register_builtin_option pp.sorrySource : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) if true, pretty print 'sorry' with its originating source position, if available"
+}
 register_builtin_option pp.coercions : Bool := {
   defValue := true
   group    := "pp"
@@ -262,6 +267,7 @@ def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
 def getPPParens (o : Options) : Bool := o.get pp.parens.name pp.parens.defValue
 def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false
 def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o)
+def getPPSorrySource (o : Options) : Bool := o.get pp.sorrySource.name pp.sorrySource.defValue
 def getPPFieldNotation (o : Options) : Bool := o.get pp.fieldNotation.name (!getPPAll o)
 def getPPFieldNotationGeneralized (o : Options) : Bool := o.get pp.fieldNotation.generalized.name pp.fieldNotation.generalized.defValue
 def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o)