From cd032480dd512ae900e692912ec491c20fa2ec9b Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 17 Oct 2024 15:58:16 -0700
Subject: [PATCH] feat: unique sorries
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 #4972

fix tests

revert comment

more unique
---
 src/Init/NotationExtra.lean                   |   5 -
 src/Init/Prelude.lean                         |  15 +-
 src/Init/Tactics.lean                         |  18 ++-
 src/Lean/Elab/BuiltinNotation.lean            |   6 +-
 src/Lean/Elab/Extra.lean                      |   2 +-
 src/Lean/Elab/MutualDef.lean                  |   2 +-
 src/Lean/Elab/PreDefinition/Basic.lean        |   1 -
 src/Lean/Elab/PreDefinition/Main.lean         |   4 +-
 src/Lean/Elab/Tactic/Basic.lean               |   2 +-
 src/Lean/Elab/Tactic/LibrarySearch.lean       |   2 +-
 src/Lean/Elab/Term.lean                       |   6 +-
 src/Lean/Meta/AppBuilder.lean                 |  60 ++++++-
 src/Lean/Meta/Tactic/Util.lean                |   2 +-
 src/Lean/Parser/Term.lean                     |  18 ++-
 src/Lean/PrettyPrinter/Delaborator/Basic.lean |  18 ++-
 .../PrettyPrinter/Delaborator/Builtins.lean   |  29 +++-
 .../PrettyPrinter/Delaborator/Options.lean    |   6 +
 .../Server/FileWorker/RequestHandling.lean    |  39 +++--
 src/Lean/Util/Sorry.lean                      |  12 +-
 src/Lean/Widget/InteractiveCode.lean          |   1 +
 src/lake/Lake/CLI/Translate.lean              |   1 -
 tests/lean/815b.lean.expected.out             |   3 +-
 tests/lean/interactive/Diff.lean.expected.out | 151 ++++++++----------
 tests/lean/run/sorry.lean                     |  63 ++++++++
 tests/lean/shadow.lean.expected.out           |   2 +-
 25 files changed, 325 insertions(+), 143 deletions(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 5a8db9fb426e6..b5a362f279217 100644
--- a/src/Init/NotationExtra.lean
+++ b/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 ()
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 216d1762667c3..b4d7395278b27 100644
--- a/src/Init/Prelude.lean
+++ b/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)
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index ed9f3236ea7d1..e695710903470 100644
--- a/src/Init/Tactics.lean
+++ b/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`.
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 8ddba4ffb8441..3546d93218110 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/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 :=
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index c4d792c7c38e6..61edbb147a116 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/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
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index c345959a64e4c..36282c9eb0cde 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index b1b78b1a9aa50..572aaa8e1579d 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index fb94aa6ab9c9c..60ed87cc95944 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 067513b70a001..0dd02f8e093c6 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/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"
diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean
index 2f0320c2a404b..d4be2053f879a 100644
--- a/src/Lean/Elab/Tactic/LibrarySearch.lean
+++ b/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
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 2cf45a1748315..f199e067b6363 100644
--- a/src/Lean/Elab/Term.lean
+++ b/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
 
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 2dcdbbc44dac9..93c63c2ce7c34 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/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]
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 71a35af9fd4e1..a1e3210d82d39 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/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 -/
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 66b9a4d5d27f9..498b62f0fb3c5 100644
--- a/src/Lean/Parser/Term.lean
+++ b/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"
 /--
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 805044fcb8f71..63440abb1b1a5 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/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
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 56f91ee8c1d76..16dd40f25565e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/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`
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 216c5d6012523..cdfb6872395a0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/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)
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index ab0afc5e18c8a..abda84877f101 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -152,12 +152,21 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
   let i := ictx.info
   let ci := ictx.ctx
   let children := ictx.children
-  match i with
-  | .ofTermInfo ti =>
+
+  let locationLinksDefault : RequestM (Array LocationLink) := do
+    -- If other go-tos fail, we try to show the elaborator or parser
+    if let some ei := i.toElabInfo? then
+      if kind == declaration && ci.env.contains ei.stx.getKind then
+        return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
+      if kind == definition && ci.env.contains ei.elaborator then
+        return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
+    return #[]
+
+  let locationLinksFromTermInfo (ti : TermInfo) : RequestM (Array LocationLink) := do
     let mut expr := ti.expr
     if kind == type then
       expr ← ci.runMetaM i.lctx do
-        return Expr.getAppFn (← instantiateMVars (← Meta.inferType expr))
+        return Expr.getAppFn (← instantiateMVars (← Meta.inferType expr)) |>.consumeMData
     match expr with
     | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
     | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
@@ -176,7 +185,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
       -- go-to-definition on a projection application of a typeclass
       -- should return all instances generated by TC
       expr ← ci.runMetaM i.lctx do instantiateMVars expr
-      if let .const n _ := expr.getAppFn then
+      if let .const n _ := expr.getAppFn.consumeMData then
         -- also include constant along with instance results
         let mut results ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
         if let some info := ci.env.getProjectionFnInfo? n then
@@ -193,12 +202,26 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
             | .const declName _ => do
               if ← ci.runMetaM i.lctx do Lean.Meta.isInstance declName then pure #[declName] else pure #[]
             | .app fn arg => do pure $ (← extractInstances fn).append (← extractInstances arg)
+            | .mdata _ e => extractInstances e
             | _ => pure #[]
           if let some instArg := appArgs.get? instIdx then
             for inst in (← extractInstances instArg) do
               results := results.append (← ci.runMetaM i.lctx <| locationLinksFromDecl i inst)
             results := results.append elaborators -- put elaborators at the end of the results
+        if let some view := Meta.isLabeledSorry? expr then
+          if let some (module, range) := view.module? then
+            let targetUri := (← documentUriFromModule rc.srcSearchPath module).getD doc.meta.uri
+            let result := {
+              targetUri, targetRange := range, targetSelectionRange := range,
+              originSelectionRange? := (·.toLspRange text) <$> i.range?
+            }
+            results := results.insertAt 0 result
         return results
+    locationLinksDefault
+
+  match i with
+  | .ofTermInfo ti => return ← locationLinksFromTermInfo ti
+  | .ofOmissionInfo ti => return ← locationLinksFromTermInfo ti.toTermInfo
   | .ofFieldInfo fi =>
     if kind == type then
       let expr ← ci.runMetaM i.lctx do
@@ -213,13 +236,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
     if kind == definition || kind == declaration then
       return ← ci.runMetaM i.lctx <| locationLinksFromImport i
   | _ => pure ()
-  -- If other go-tos fail, we try to show the elaborator or parser
-  if let some ei := i.toElabInfo? then
-    if kind == declaration && ci.env.contains ei.stx.getKind then
-      return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
-    if kind == definition && ci.env.contains ei.elaborator then
-      return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
-  return #[]
+  locationLinksDefault
 
 open Elab GoToKind in
 def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean
index 3341b13421772..3a8dc75cd8384 100644
--- a/src/Lean/Util/Sorry.lean
+++ b/src/Lean/Util/Sorry.lean
@@ -10,15 +10,21 @@ import Lean.Declaration
 namespace Lean
 
 def Expr.isSorry : Expr → Bool
-  | app (app (.const ``sorryAx ..) ..) .. => true
+  | mkApp2 (.const ``sorryAx ..) _ _ => true
+  -- A labeled sorry:
+  | mkApp3 (.const ``sorryAx ..) _ _ _ => true
   | _ => false
 
 def Expr.isSyntheticSorry : Expr → Bool
-  | app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) => true
+  | mkApp2 (const ``sorryAx ..) _ (const ``Bool.true ..) => true
+  -- A labeled sorry:
+  | mkApp3 (const ``sorryAx ..) _ (const ``Bool.true ..) _ => true
   | _ => false
 
 def Expr.isNonSyntheticSorry : Expr → Bool
-  | app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) => true
+  | mkApp2 (const ``sorryAx ..) _ (const ``Bool.false ..) => true
+  -- A labeled sorry:
+  | mkApp3 (const ``sorryAx ..) _ (const ``Bool.false ..) _ => true
   | _ => false
 
 def Expr.hasSorry (e : Expr) : Bool :=
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 7cd58e70dbfc1..65aaa5f3c2bb3 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -84,6 +84,7 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
         delabApp
     else
       withOptionAtCurrPos pp.proofs.name true do
+      withOptionAtCurrPos pp.sorrySource.name true do
         delab
   let mut e := e
   -- When hovering over a metavariable, we want to see its value, even if `pp.instantiateMVars` is false.
diff --git a/src/lake/Lake/CLI/Translate.lean b/src/lake/Lake/CLI/Translate.lean
index 9a75e638cfd94..d74276cbf63b3 100644
--- a/src/lake/Lake/CLI/Translate.lean
+++ b/src/lake/Lake/CLI/Translate.lean
@@ -8,7 +8,6 @@ import Lake.Config.Package
 import Lake.CLI.Translate.Toml
 import Lake.CLI.Translate.Lean
 import Lake.Load.Lean.Elab
-import Lean.PrettyPrinter
 
 namespace Lake
 open Toml Lean System PrettyPrinter
diff --git a/tests/lean/815b.lean.expected.out b/tests/lean/815b.lean.expected.out
index 6642d853a3247..ee8ffaf1896af 100644
--- a/tests/lean/815b.lean.expected.out
+++ b/tests/lean/815b.lean.expected.out
@@ -77,8 +77,7 @@
         Transformer
           fun redf a a => redf
   [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
-    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
-          f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
   [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] ∀ (a : α), δ → IsSmooth fun g => f (g a)
diff --git a/tests/lean/interactive/Diff.lean.expected.out b/tests/lean/interactive/Diff.lean.expected.out
index 68c66141372e2..f11ff86ff24a8 100644
--- a/tests/lean/interactive/Diff.lean.expected.out
+++ b/tests/lean/interactive/Diff.lean.expected.out
@@ -1,20 +1,18 @@
-{ goals := #[{ type := Lean.Widget.TaggedText.tag
-                         { subexprPos := "/", diffStatus? := none }
-                         (Lean.Widget.TaggedText.append
-                           #[Lean.Widget.TaggedText.tag
-                               { subexprPos := "/0", diffStatus? := none }
-                               (Lean.Widget.TaggedText.append
-                                 #[Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/0/0/1", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.text "x"),
-                                   Lean.Widget.TaggedText.text " = ",
-                                   Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/0/1", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.text "x")]),
-                             Lean.Widget.TaggedText.text " → ",
-                             Lean.Widget.TaggedText.tag
-                               { subexprPos := "/1", diffStatus? := none }
-                               (Lean.Widget.TaggedText.text "True")]),
+{ goals := #[{ type := Lean.Widget.TaggedText.append
+                         #[Lean.Widget.TaggedText.tag
+                             { subexprPos := "/0", diffStatus? := none }
+                             (Lean.Widget.TaggedText.append
+                               #[Lean.Widget.TaggedText.tag
+                                   { subexprPos := "/0/0/1", diffStatus? := none }
+                                   (Lean.Widget.TaggedText.text "x"),
+                                 Lean.Widget.TaggedText.text " = ",
+                                 Lean.Widget.TaggedText.tag
+                                   { subexprPos := "/0/1", diffStatus? := none }
+                                   (Lean.Widget.TaggedText.text "x")]),
+                           Lean.Widget.TaggedText.text " → ",
+                           Lean.Widget.TaggedText.tag
+                             { subexprPos := "/1", diffStatus? := none }
+                             (Lean.Widget.TaggedText.text "True")],
                isInserted? := some false,
                isRemoved? := none,
                hyps := #[{ type := Lean.Widget.TaggedText.tag
@@ -24,23 +22,21 @@
                            isInserted? := some true,
                            isRemoved? := none }] }] }
 
-{ goals := #[{ type := Lean.Widget.TaggedText.tag
-                         { subexprPos := "/", diffStatus? := none }
-                         (Lean.Widget.TaggedText.append
-                           #[Lean.Widget.TaggedText.tag
-                               { subexprPos := "/0", diffStatus? := some "willDelete" }
-                               (Lean.Widget.TaggedText.append
-                                 #[Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/0/0/1", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.text "x"),
-                                   Lean.Widget.TaggedText.text " = ",
-                                   Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/0/1", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.text "x")]),
-                             Lean.Widget.TaggedText.text " → ",
-                             Lean.Widget.TaggedText.tag
-                               { subexprPos := "/1", diffStatus? := none }
-                               (Lean.Widget.TaggedText.text "True")]),
+{ goals := #[{ type := Lean.Widget.TaggedText.append
+                         #[Lean.Widget.TaggedText.tag
+                             { subexprPos := "/0", diffStatus? := some "willDelete" }
+                             (Lean.Widget.TaggedText.append
+                               #[Lean.Widget.TaggedText.tag
+                                   { subexprPos := "/0/0/1", diffStatus? := none }
+                                   (Lean.Widget.TaggedText.text "x"),
+                                 Lean.Widget.TaggedText.text " = ",
+                                 Lean.Widget.TaggedText.tag
+                                   { subexprPos := "/0/1", diffStatus? := none }
+                                   (Lean.Widget.TaggedText.text "x")]),
+                           Lean.Widget.TaggedText.text " → ",
+                           Lean.Widget.TaggedText.tag
+                             { subexprPos := "/1", diffStatus? := none }
+                             (Lean.Widget.TaggedText.text "True")],
                isInserted? := some false,
                isRemoved? := none,
                hyps := #[{ type := Lean.Widget.TaggedText.tag
@@ -63,22 +59,19 @@
                                (Lean.Widget.TaggedText.text "Nat"),
                              Lean.Widget.TaggedText.text "), ",
                              Lean.Widget.TaggedText.tag
-                               { subexprPos := "/1", diffStatus? := none }
+                               { subexprPos := "/1/0", diffStatus? := some "willDelete" }
                                (Lean.Widget.TaggedText.append
                                  #[Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/1/0", diffStatus? := some "willDelete" }
-                                     (Lean.Widget.TaggedText.append
-                                       #[Lean.Widget.TaggedText.tag
-                                           { subexprPos := "/1/0/0/1", diffStatus? := none }
-                                           (Lean.Widget.TaggedText.text "x"),
-                                         Lean.Widget.TaggedText.text " = ",
-                                         Lean.Widget.TaggedText.tag
-                                           { subexprPos := "/1/0/1", diffStatus? := none }
-                                           (Lean.Widget.TaggedText.text "x")]),
-                                   Lean.Widget.TaggedText.text " → ",
+                                     { subexprPos := "/1/0/0/1", diffStatus? := none }
+                                     (Lean.Widget.TaggedText.text "x"),
+                                   Lean.Widget.TaggedText.text " = ",
                                    Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/1/1", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.text "True")])]),
+                                     { subexprPos := "/1/0/1", diffStatus? := none }
+                                     (Lean.Widget.TaggedText.text "x")]),
+                             Lean.Widget.TaggedText.text " → ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/1/1", diffStatus? := none }
+                               (Lean.Widget.TaggedText.text "True")]),
                isInserted? := some false,
                isRemoved? := none,
                hyps := #[] }] }
@@ -100,23 +93,21 @@
                            names := #["x", "y"],
                            isInserted? := none,
                            isRemoved? := none },
-                         { type := Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.append
-                                       #[Lean.Widget.TaggedText.tag
-                                           { subexprPos := "/0", diffStatus? := none }
-                                           (Lean.Widget.TaggedText.text "α"),
-                                         Lean.Widget.TaggedText.text " → ",
-                                         Lean.Widget.TaggedText.tag
-                                           { subexprPos := "/1", diffStatus? := none }
-                                           (Lean.Widget.TaggedText.append
-                                             #[Lean.Widget.TaggedText.tag
-                                                 { subexprPos := "/1/0/1", diffStatus? := none }
-                                                 (Lean.Widget.TaggedText.text "x"),
-                                               Lean.Widget.TaggedText.text " = ",
-                                               Lean.Widget.TaggedText.tag
-                                                 { subexprPos := "/1/1", diffStatus? := some "willChange" }
-                                                 (Lean.Widget.TaggedText.text "y")])]),
+                         { type := Lean.Widget.TaggedText.append
+                                     #[Lean.Widget.TaggedText.tag
+                                         { subexprPos := "/0", diffStatus? := none }
+                                         (Lean.Widget.TaggedText.text "α"),
+                                       Lean.Widget.TaggedText.text " → ",
+                                       Lean.Widget.TaggedText.tag
+                                         { subexprPos := "/1", diffStatus? := none }
+                                         (Lean.Widget.TaggedText.append
+                                           #[Lean.Widget.TaggedText.tag
+                                               { subexprPos := "/1/0/1", diffStatus? := none }
+                                               (Lean.Widget.TaggedText.text "x"),
+                                             Lean.Widget.TaggedText.text " = ",
+                                             Lean.Widget.TaggedText.tag
+                                               { subexprPos := "/1/1", diffStatus? := some "willChange" }
+                                               (Lean.Widget.TaggedText.text "y")])],
                            names := #["f"],
                            isInserted? := none,
                            isRemoved? := none },
@@ -151,23 +142,21 @@
                            names := #["x", "y"],
                            isInserted? := none,
                            isRemoved? := none },
-                         { type := Lean.Widget.TaggedText.tag
-                                     { subexprPos := "/", diffStatus? := none }
-                                     (Lean.Widget.TaggedText.append
-                                       #[Lean.Widget.TaggedText.tag
-                                           { subexprPos := "/0", diffStatus? := none }
-                                           (Lean.Widget.TaggedText.text "α"),
-                                         Lean.Widget.TaggedText.text " → ",
-                                         Lean.Widget.TaggedText.tag
-                                           { subexprPos := "/1", diffStatus? := none }
-                                           (Lean.Widget.TaggedText.append
-                                             #[Lean.Widget.TaggedText.tag
-                                                 { subexprPos := "/1/0/1", diffStatus? := none }
-                                                 (Lean.Widget.TaggedText.text "x"),
-                                               Lean.Widget.TaggedText.text " = ",
-                                               Lean.Widget.TaggedText.tag
-                                                 { subexprPos := "/1/1", diffStatus? := some "wasChanged" }
-                                                 (Lean.Widget.TaggedText.text "x")])]),
+                         { type := Lean.Widget.TaggedText.append
+                                     #[Lean.Widget.TaggedText.tag
+                                         { subexprPos := "/0", diffStatus? := none }
+                                         (Lean.Widget.TaggedText.text "α"),
+                                       Lean.Widget.TaggedText.text " → ",
+                                       Lean.Widget.TaggedText.tag
+                                         { subexprPos := "/1", diffStatus? := none }
+                                         (Lean.Widget.TaggedText.append
+                                           #[Lean.Widget.TaggedText.tag
+                                               { subexprPos := "/1/0/1", diffStatus? := none }
+                                               (Lean.Widget.TaggedText.text "x"),
+                                             Lean.Widget.TaggedText.text " = ",
+                                             Lean.Widget.TaggedText.tag
+                                               { subexprPos := "/1/1", diffStatus? := some "wasChanged" }
+                                               (Lean.Widget.TaggedText.text "x")])],
                            names := #["f"],
                            isInserted? := none,
                            isRemoved? := none },
diff --git a/tests/lean/run/sorry.lean b/tests/lean/run/sorry.lean
index 7940d9e0181ce..9b0094eb97247 100644
--- a/tests/lean/run/sorry.lean
+++ b/tests/lean/run/sorry.lean
@@ -24,3 +24,66 @@ Pretty printing
 
 /-- info: fun x => sorry (x + 1) : Nat → Nat -/
 #guard_msgs in #check fun x : Nat => (sorry : Nat → Nat) (x + 1)
+
+/-!
+Uniqueness
+-/
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+example : (sorry : Nat) = sorry := by
+  fail_if_success rfl
+  sorry
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+def f (n : Nat) : Nat → Nat := sorry
+
+example : f 0 0 = f 0 0 := rfl -- succeeds
+
+/-!
+If `sorry` is used for a function type, then one gets a family of unique `sorry`s.
+-/
+/--
+error: type mismatch
+  rfl
+has type
+  f 0 1 = f 0 1 : Prop
+but is expected to have type
+  f 0 1 = f 0 0 : Prop
+-/
+#guard_msgs in example : f 0 1 = f 0 0 := rfl
+
+/-!
+It is not completely unique though. The `sorry` did not pay attention to variables in the local context.
+-/
+#guard_msgs in example : f 1 0 = f 0 0 := rfl
+
+/-!
+Showing source position when surfacing differences.
+-/
+-- note: the module name is `sorry` and not `lean.run.sorry` in the testing environment,
+-- so this test fails in VS Code.
+/--
+error: type mismatch
+  rfl
+has type
+  sorry = sorry `«sorry:75:26» : Prop
+but is expected to have type
+  sorry = sorry `«sorry:75:41» : Prop
+-/
+#guard_msgs in example : (sorry : Nat) = sorry := rfl
+
+/-!
+Elaboration errors are just labeled, not unique, to limit cascading errors.
+-/
+/--
+error: unknown identifier 'a'
+---
+error: unknown identifier 'b'
+---
+info: ⊢ sorry = sorry
+-/
+#guard_msgs in
+set_option autoImplicit false in
+example : a = b := by trace_state; rfl
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index 8d1685226a75c..db3cdf24fcf04 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -19,7 +19,7 @@ inst✝ inst : α
 shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst.75 : Inhabited α
+inst.78 : Inhabited α
 inst inst : α
 ⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder