diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 5a8db9fb426e..b5a362f27921 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 67191231bbf0..e6a408253f70 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -645,23 +645,22 @@ 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 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 check if a declaration depends on `sorry` either directly or indirectly 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
+The `synthetic` flag is false when a `sorry` is 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
 in the expression. A synthetic `sorry` acts like a regular one, except that it
-suppresses follow-up errors in order to prevent one error from causing a cascade
+suppresses follow-up errors in order to prevent an 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)
@@ -3932,6 +3931,13 @@ def getId : Syntax → Name
   | ident _ _ val _ => val
   | _               => Name.anonymous
 
+/-- Retrieve the immediate info from the Syntax node. -/
+def getInfo? : Syntax → Option SourceInfo
+  | atom info ..  => some info
+  | ident info .. => some info
+  | node info ..  => some info
+  | missing       => none
+
 /-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
 partial def getHeadInfo? : Syntax → Option SourceInfo
   | atom info _   => some info
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 2d35522f1ac4..05b0fe9aecad 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, the axiom used by the 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/Data/DeclarationRange.lean b/src/Lean/Data/DeclarationRange.lean
new file mode 100644
index 000000000000..cae8ab30da1d
--- /dev/null
+++ b/src/Lean/Data/DeclarationRange.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Data.Position
+
+/-!
+# Data types for declaration ranges
+
+The environment extension for declaration ranges is in `Lean.DeclarationRange`.
+-/
+
+namespace Lean
+
+/-- Store position information for declarations. -/
+structure DeclarationRange where
+  pos          : Position
+  /-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
+  because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
+  codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
+  file, which is IO-heavy. -/
+  charUtf16    : Nat
+  endPos       : Position
+  /-- See `charUtf16`. -/
+  endCharUtf16 : Nat
+  deriving Inhabited, DecidableEq, Repr
+
+instance : ToExpr DeclarationRange where
+  toExpr r   := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
+  toTypeExpr := mkConst ``DeclarationRange
+
+structure DeclarationRanges where
+  range          : DeclarationRange
+  selectionRange : DeclarationRange
+  deriving Inhabited, Repr
+
+instance : ToExpr DeclarationRanges where
+  toExpr r   := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
+  toTypeExpr := mkConst ``DeclarationRanges
+
+/--
+A declaration location is a declaration range along with the name of the module the declaration resides in.
+-/
+structure DeclarationLocation where
+  module : Name
+  range : DeclarationRange
+  deriving Inhabited, DecidableEq, Repr
diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean
index 9a0e14465200..76566d950bce 100644
--- a/src/Lean/DeclarationRange.lean
+++ b/src/Lean/DeclarationRange.lean
@@ -4,37 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Data.DeclarationRange
 import Lean.MonadEnv
-import Lean.AuxRecursor
-import Lean.ToExpr
 
-namespace Lean
+/-!
+# Environment extension for declaration ranges
+-/
 
-/-- Store position information for declarations. -/
-structure DeclarationRange where
-  pos          : Position
-  /-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
-  because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
-  codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
-  file, which is IO-heavy. -/
-  charUtf16    : Nat
-  endPos       : Position
-  /-- See `charUtf16`. -/
-  endCharUtf16 : Nat
-  deriving Inhabited, DecidableEq, Repr
-
-instance : ToExpr DeclarationRange where
-  toExpr r   := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
-  toTypeExpr := mkConst ``DeclarationRange
-
-structure DeclarationRanges where
-  range          : DeclarationRange
-  selectionRange : DeclarationRange
-  deriving Inhabited, Repr
-
-instance : ToExpr DeclarationRanges where
-  toExpr r   := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
-  toTypeExpr := mkConst ``DeclarationRanges
+namespace Lean
 
 builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
 builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 8ddba4ffb844..3546d9321811 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 c4d792c7c38e..61edbb147a11 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/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index eb129079d45e..2069c7138a97 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -192,8 +192,12 @@ def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
 
-def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
-  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
+def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
+  let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
+  return f!"DelabTermInfo @ {← TermInfo.format ctx info.toTermInfo}\n\
+    Location: {loc}\n\
+    Docstring: {repr info.docString?}\n\
+    Explicit: {info.explicit}"
 
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
   f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
@@ -211,7 +215,7 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofCustomInfo i         => pure <| Std.ToFormat.format i
   | ofFVarAliasInfo i      => pure <| i.format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
-  | ofOmissionInfo i       => i.format ctx
+  | ofDelabTermInfo i      => i.format ctx
   | ofChoiceInfo i         => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
@@ -227,7 +231,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofCustomInfo _         => none
   | ofFVarAliasInfo _      => none
   | ofFieldRedeclInfo _    => none
-  | ofOmissionInfo i       => some i.toElabInfo
+  | ofDelabTermInfo i      => some i.toElabInfo
   | ofChoiceInfo i         => some i.toElabInfo
 
 /--
diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
index 5ecdd7dde97d..dd22148866c6 100644
--- a/src/Lean/Elab/InfoTree/Types.lean
+++ b/src/Lean/Elab/InfoTree/Types.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.Data.Position
+import Lean.Data.DeclarationRange
 import Lean.Data.OpenDecl
 import Lean.MetavarContext
 import Lean.Environment
@@ -168,14 +168,22 @@ structure FieldRedeclInfo where
   stx : Syntax
 
 /--
-Denotes information for the term `⋯` that is emitted by the delaborator when omitting a term
-due to `pp.deepTerms false` or `pp.proofs false`. Omission needs to be treated differently from regular terms because
+Denotes TermInfo with additional configurations to control interactions with delaborated terms.
+
+For example, the omission term `⋯` that is emitted by the delaborator when omitting a term
+due to `pp.deepTerms false` or `pp.proofs false` uses this.
+Omission needs to be treated differently from regular terms because
 it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
 Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
-regular delaboration settings.
+regular delaboration settings. Additionally, omissions come with a reason for omission.
 -/
-structure OmissionInfo extends TermInfo where
-  reason : String
+structure DelabTermInfo extends TermInfo where
+  /-- A source position to use for "go to definition", to override the default. -/
+  location? : Option DeclarationLocation := none
+  /-- Text to use to override the docstring. -/
+  docString? : Option String := none
+  /-- Whether to use explicit mode when pretty printing the term on hover. -/
+  explicit : Bool := true
 
 /--
 Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
@@ -198,7 +206,7 @@ inductive Info where
   | ofCustomInfo (i : CustomInfo)
   | ofFVarAliasInfo (i : FVarAliasInfo)
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
-  | ofOmissionInfo (i : OmissionInfo)
+  | ofDelabTermInfo (i : DelabTermInfo)
   | ofChoiceInfo (i : ChoiceInfo)
   deriving Inhabited
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index dae2f1fea891..79d589ddf426 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 b1b78b1a9aa5..572aaa8e1579 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 97056437088a..0e4f09bea1cc 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
         let msg := m!"failed to compile 'partial' definition '{preDef.declName}'"
         liftM <| mkInhabitantFor msg xs type
@@ -115,7 +115,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 067513b70a00..0dd02f8e093c 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 2f0320c2a404..d4be2053f879 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 2cf45a174831..f199e067b636 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.lean b/src/Lean/Meta.lean
index 790db52ba14b..39efe3f028ef 100644
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -17,6 +17,7 @@ import Lean.Meta.Instances
 import Lean.Meta.AbstractMVars
 import Lean.Meta.SynthInstance
 import Lean.Meta.AppBuilder
+import Lean.Meta.Sorry
 import Lean.Meta.Tactic
 import Lean.Meta.KAbstract
 import Lean.Meta.RecursorInfo
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 2dcdbbc44dac..d25b556595da 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Structure
-import Lean.Util.Recognizers
 import Lean.Meta.SynthInstance
 import Lean.Meta.Check
 import Lean.Meta.DecLevel
@@ -513,10 +512,6 @@ def mkSome (type value : Expr) : MetaM Expr := do
   let u ← getDecLevel type
   return mkApp2 (mkConst ``Option.some [u]) type value
 
-def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
-  let u ← getLevel type
-  return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
-
 /-- Return `Decidable.decide p` -/
 def mkDecide (p : Expr) : MetaM Expr :=
   mkAppOptM ``Decidable.decide #[p, none]
@@ -545,10 +540,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/Check.lean b/src/Lean/Meta/Check.lean
index 741c4fe84212..b6d7c2771076 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.InferType
+import Lean.Meta.Sorry
 
 /-!
 This is not the Kernel type checker, but an auxiliary method for checking
@@ -133,6 +134,12 @@ where
           if fn? == ``OfNat.ofNat && as.size ≥ 3 && firstImplicitDiff? == some 0 then
             -- Even if there is an explicit diff, it is better to see that the type is different.
             return (a.setPPNumericTypes true, b.setPPNumericTypes true)
+          if fn? == ``sorryAx then
+            -- If these are `sorry`s with differing source positions, make sure the delaborator shows the positions.
+            if let some { module? := moda? } := isLabeledSorry? a then
+              if let some { module? := modb? } := isLabeledSorry? b then
+                if moda? != modb? then
+                  return (a.setOption `pp.sorrySource true, b.setOption `pp.sorrySource true)
           -- General case
           if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
             let (ai, bi) ← visit as[i]! bs[i]!
diff --git a/src/Lean/Meta/Sorry.lean b/src/Lean/Meta/Sorry.lean
new file mode 100644
index 000000000000..e5f600063bff
--- /dev/null
+++ b/src/Lean/Meta/Sorry.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Data.Lsp.Utf16
+import Lean.Meta.InferType
+import Lean.Util.Recognizers
+
+/-!
+# Utilities for creating and recognizing `sorry`
+
+This module develops material for creating and recognizing `sorryAx` terms that encode originating source positions.
+There are three orthogonal configurations for sorries:
+
+- The sorry could be *synthetic*. When elaboration fails on some subterm, then we can use a sorry to fill in the missing subterm.
+  In this case elaboration marks the sorry as being "synthetic" while logging an error.
+  The presence of synthetic sorries tends to suppress further errors. For example, the "this declaration contains sorry" error
+  is not triggered for synthetic sorries as we assume there is already an error message logged.
+
+- The sorry could be *unique*. A unique sorry is not definitionally equal to any other sorry, even if they have the same type.
+  Normally `sorryAx α s = sorryAx α s` is a definitional equality. Unique sorries insert a unique tag `t` using the encoding `sorryAx (τ → α) s t`.
+
+- The sorry could be *labeled*. A labeled sorry contains source position information, supporting the LSP "go to definition" feature in the Infoview,
+  and also supporting pretty printing the sorry with an indication of source position when the option `pp.sorrySource` is true.
+-/
+
+namespace Lean.Meta
+
+/--
+Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
+
+See also `Lean.Meta.mkLabeledSorry`, for creating a `sorry` that is labeled or unique.
+-/
+def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
+  let u ← getLevel type
+  return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
+
+structure SorryLabelView where
+  /--
+  Records the origin module name, logical source position, and LSP range for the `sorry`.
+  The logical source position is used when displaying the sorry when the `pp.sorrySource` option is true,
+  and the LSP range is used for "go to definition" in the Infoview.
+  -/
+  module? : Option DeclarationLocation := none
+
+def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
+  let name :=
+    if let some { module, range := { pos, endPos, charUtf16, endCharUtf16 } } := view.module? then
+      module
+        |>.num pos.line |>.num pos.column
+        |>.num endPos.line |>.num endPos.column
+        |>.num charUtf16 |>.num endCharUtf16
+    else
+      .anonymous
+  mkFreshUserName (name.str "_sorry")
+
+def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
+  guard <| name.hasMacroScopes
+  let .str name "_sorry" := name.eraseMacroScopes | failure
+  if let .num (.num (.num (.num (.num (.num module posLine) posCol) endLine) endCol) charUtf16) endCharUtf16 := name then
+    return { module? := some { module, range := { pos := ⟨posLine, posCol⟩, endPos := ⟨endLine, endCol⟩, charUtf16, endCharUtf16 } } }
+  else
+    failure
+
+/--
+Constructs a `sorryAx`.
+* If the current ref has a source position, then creates a labeled sorry.
+  This supports "go to definition" in the InfoView and pretty printing a source position when the `pp.sorrySource` option is true.
+* If `synthetic` is true, then the `sorry` is regarded as being generated by the elaborator.
+  The caller should ensure that there is an associated error logged.
+* 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 startSPos, some endSPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
+      let fileMap ← getFileMap
+      SorryLabelView.encode {
+        module? := some {
+          module := (← getMainModule)
+          range := {
+            pos := fileMap.toPosition startSPos
+            endPos := fileMap.toPosition endSPos
+            charUtf16 := (fileMap.utf8PosToLspPos startSPos).character
+            endCharUtf16 := (fileMap.utf8PosToLspPos endSPos).character
+          }
+        }
+      }
+    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
+    let tag' := mkApp4 (mkConst ``Function.const [levelOne, levelOne]) (mkConst ``Unit) (mkConst ``Lean.Name) (mkConst ``Unit.unit) (toExpr tag)
+    return .app e tag'
+
+/--
+Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
+If it is, then the `sorry` takes the first three arguments, and the tag is at argument 3.
+-/
+def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
+  guard <| e.isAppOf ``sorryAx
+  let numArgs := e.getAppNumArgs
+  guard <| numArgs ≥ 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 tag ← arg.appArg!.name?
+    SorryLabelView.decode? tag
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 71a35af9fd4e..a1e3210d82d3 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 2cad961e35f3..be6ef089444f 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, the axiom used by the implementation of `sorry`.
+
+"Go to definition" on `sorry` in the Infoview will go to the source position where it was introduced, if such information is available.
+
+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 805044fcb8f7..a89ab65456a9 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -211,6 +211,16 @@ where
     stx := stx
   }
 
+def addDelabTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
+    (location? : Option DeclarationLocation := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit := do
+  let info := Info.ofDelabTermInfo {
+    toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := isBinder)
+    location?  := location?
+    docString? := docString?
+    explicit   := explicit
+  }
+  modify fun s => { s with infos := s.infos.insert pos info }
+
 /--
 Annotates the term with the current expression position and registers `TermInfo`
 to associate the term to the current expression.
@@ -221,13 +231,30 @@ 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 some (.synthetic ⟨pos⟩ ⟨pos'⟩) := stx.raw.getInfo? 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
   annotateTermInfo stx
 
+/--
+Modifies the delaborator so that it ensures resulting term is annotated using `annotateTermInfoUnlessAnnotated`.
+-/
+def withAnnotateTermInfoUnlessAnnotated (d : Delab) : Delab := do
+  let stx ← d
+  annotateTermInfoUnlessAnnotated stx
+
 /--
 Gets an name based on `suggestion` that is unused in the local context.
 Erases macro scopes.
@@ -294,13 +321,7 @@ def OmissionReason.toString : OmissionReason → String
   | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
-  let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
-  modify fun s => { s with infos := s.infos.insert pos info }
-where
-  mkOmissionInfo stx e := return {
-    toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := false)
-    reason := reason.toString
-  }
+  addDelabTermInfo pos stx e (docString? := reason.toString) (explicit := false)
 
 /--
 Runs the delaborator `act` with increased depth.
@@ -381,7 +402,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
 
@@ -433,7 +454,7 @@ open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze DelabM)
 
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM α) :
-  MetaM (α × PosMap Elab.Info) := do
+    MetaM (α × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
   let e ← Meta.erasePatternRefAnnotations e
@@ -453,7 +474,8 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM 
         topDownAnalyze e
       else pure optionsPerPos
     let (stx, {infos := infos, ..}) ← catchInternalId Delaborator.delabFailureId
-        (delab
+        -- Clear the ref to ensure that quotations in delaborators start with blank source info.
+        (MonadRef.withRef .missing delab
           { optionsPerPos := optionsPerPos
             currNamespace := (← getCurrNamespace)
             openDecls := (← getOpenDecls)
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 56f91ee8c1d7..5dc3aa3ee97f 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,35 @@ 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
+  let numArgs := (← getExpr).getAppNumArgs
+  guard <| numArgs ≥ 2
+  -- Cache the current position's value, since it might be applied to the entire application.
+  let sorrySource ← getPPOption getPPSorrySource
+  -- If this is constructed by `Lean.Meta.mkLabeledSorry`, then normally we 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 loc := view.module? then
+        let (stx, explicit) ←
+          if ← pure sorrySource <||> getPPOption getPPSorrySource then
+            let posAsName := Name.mkSimple s!"{loc.module}:{loc.range.pos.line}:{loc.range.pos.column}"
+            let pos := mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{posAsName}"]
+            let src ← withAppArg <| annotateTermInfo pos
+            pure (← `(sorry $src), true)
+          else
+            -- Set `explicit` to false so that the first hover sets `pp.sorrySource` to true in `Lean.Widget.ppExprTagged`
+            pure (← `(sorry), false)
+        let stx ← annotateCurPos stx
+        addDelabTermInfo (← getPos) stx (← getExpr) (explicit := explicit) (location? := loc)
+          (docString? := "This is a `sorry` term associated to a source position. Use 'Go to definition' to go there.")
+        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 216c5d601252..cdfb6872395a 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 ab0afc5e18c8..3c1c6c5a1089 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -152,13 +152,22 @@ 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))
-    match expr with
+    match expr.consumeMData with
     | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
     | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
     | _ => pure ()
@@ -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,29 @@ 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
         return results
+    locationLinksDefault
+
+  match i with
+  | .ofTermInfo ti =>
+    return ← locationLinksFromTermInfo ti
+  | .ofDelabTermInfo { toTermInfo := ti, location?, .. } =>
+    if let some location := location? then
+      if let some targetUri ← documentUriFromModule rc.srcSearchPath location.module then
+        let range := location.range.toLspRange
+        let result : LocationLink := {
+          targetUri, targetRange := range, targetSelectionRange := range,
+          originSelectionRange? := (·.toLspRange text) <$> i.range?
+        }
+        return #[result]
+      -- If we fail to find a DocumentUri, fall through and use the default method to at least try to have something to jump to.
+    return ← locationLinksFromTermInfo ti
   | .ofFieldInfo fi =>
     if kind == type then
       let expr ← ci.runMetaM i.lctx do
@@ -213,13 +239,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/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index fc18bb35d683..dd877fdbbb82 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -53,13 +53,12 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
         | some type => some <$> ppExprTagged type
         | none => pure none
       let exprExplicit? ← match i.info with
-        | Elab.Info.ofTermInfo ti =>
-          pure <| some <| ← ppExprTaggedWithoutTopLevelHighlight ti.expr (explicit := true)
-        | Elab.Info.ofOmissionInfo { toTermInfo := ti, .. } =>
-          -- Omitted terms are simply to be expanded, not printed explicitly.
-          -- Keep the top-level tag so that users can also see the explicit version
-          -- of the omitted term.
-          pure <| some <| ← ppExprTagged ti.expr (explicit := false)
+        | Elab.Info.ofTermInfo ti
+        | Elab.Info.ofDelabTermInfo { toTermInfo := ti, explicit := true, ..} =>
+          some <$> ppExprTaggedWithoutTopLevelHighlight ti.expr (explicit := true)
+        | Elab.Info.ofDelabTermInfo { toTermInfo := ti, explicit := false, ..} =>
+          -- Keep the top-level tag so that users can also see the explicit version of the term on an additional hover.
+          some <$> ppExprTagged ti.expr (explicit := false)
         | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
         | _ => pure none
       return {
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index b642d7384911..5ef83835ae90 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -146,13 +146,13 @@ def Info.stx : Info → Syntax
   | ofUserWidgetInfo i     => i.stx
   | ofFVarAliasInfo _      => .missing
   | ofFieldRedeclInfo i    => i.stx
-  | ofOmissionInfo i       => i.stx
+  | ofDelabTermInfo i      => i.stx
   | ofChoiceInfo i         => i.stx
 
 def Info.lctx : Info → LocalContext
   | .ofTermInfo i           => i.lctx
   | .ofFieldInfo i          => i.lctx
-  | .ofOmissionInfo i       => i.lctx
+  | .ofDelabTermInfo i      => i.lctx
   | .ofMacroExpansionInfo i => i.lctx
   | .ofCompletionInfo i     => i.lctx
   | _                       => LocalContext.empty
@@ -251,15 +251,17 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
 
 def Info.type? (i : Info) : MetaM (Option Expr) :=
   match i with
-  | Info.ofTermInfo ti     => Meta.inferType ti.expr
-  | Info.ofFieldInfo fi    => Meta.inferType fi.val
-  | Info.ofOmissionInfo oi => Meta.inferType oi.expr
+  | Info.ofTermInfo ti      => Meta.inferType ti.expr
+  | Info.ofFieldInfo fi     => Meta.inferType fi.val
+  | Info.ofDelabTermInfo ti => Meta.inferType ti.expr
   | _ => return none
 
 def Info.docString? (i : Info) : MetaM (Option String) := do
   let env ← getEnv
   match i with
-  | .ofTermInfo ti =>
+  | .ofDelabTermInfo { docString? := some s, .. } => return s
+  | .ofTermInfo ti
+  | .ofDelabTermInfo ti =>
     if let some n := ti.expr.constName? then
       return (← findDocString? env n)
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
@@ -269,7 +271,6 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     if let some decl := (← getOptionDecls).find? oi.optionName then
       return decl.descr
     return none
-  | .ofOmissionInfo { reason := s, .. } => return s -- Show the omission reason for the docstring.
   | _ => pure ()
   if let some ei := i.toElabInfo? then
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
@@ -418,7 +419,7 @@ where go ci?
   | .node i cs =>
     match ci?, i with
     | some ci, .ofTermInfo ti
-    | some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
+    | some ci, .ofDelabTermInfo ti => do
       -- NOTE: `instantiateMVars` can potentially be expensive but we rely on the elaborator
       -- creating a fully instantiated `MutualDef.body` term info node which has the implicit effect
       -- of making the `instantiateMVars` here a no-op and avoids further recursing into the body
diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean
index 3341b1342177..b97e91c8fb9b 100644
--- a/src/Lean/Util/Sorry.lean
+++ b/src/Lean/Util/Sorry.lean
@@ -9,17 +9,17 @@ import Lean.Declaration
 
 namespace Lean
 
-def Expr.isSorry : Expr → Bool
-  | app (app (.const ``sorryAx ..) ..) .. => true
-  | _ => false
+/-- Returns `true` if the expression is an application of `sorryAx`. -/
+def Expr.isSorry (e : Expr) : Bool :=
+  e.isAppOf ``sorryAx
 
-def Expr.isSyntheticSorry : Expr → Bool
-  | app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) => true
-  | _ => false
+/-- Returns `true` if the expression is of the form `sorryAx _ true ..`. -/
+def Expr.isSyntheticSorry (e : Expr) : Bool :=
+  e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 2 && (e.getArg! 1).isConstOf ``Bool.true
 
-def Expr.isNonSyntheticSorry : Expr → Bool
-  | app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) => true
-  | _ => false
+/-- Returns `true` if the expression is of the form `sorryAx _ false ..`. -/
+def Expr.isNonSyntheticSorry (e : Expr) : Bool :=
+  e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 2 && (e.getArg! 1).isConstOf ``Bool.false
 
 def Expr.hasSorry (e : Expr) : Bool :=
   Option.isSome <| e.find? (·.isConstOf ``sorryAx)
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 7cd58e70dbfc..65aaa5f3c2bb 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 943b4d195bbd..fee3b344074e 100644
--- a/src/lake/Lake/CLI/Translate.lean
+++ b/src/lake/Lake/CLI/Translate.lean
@@ -9,7 +9,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/run/sorry.lean b/tests/lean/run/sorry.lean
index 7940d9e0181c..feb53480bbe9 100644
--- a/tests/lean/run/sorry.lean
+++ b/tests/lean/run/sorry.lean
@@ -2,6 +2,8 @@
 # Tests of the `sorry` term elaborator
 -/
 
+set_option pp.mvars false
+
 /-!
 Basic usage.
 -/
@@ -24,3 +26,81 @@ 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
+  ?_ = ?_ : 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
+  sorry
+has type
+  sorry `«sorry:77:43» : Sort _
+but is expected to have type
+  sorry `«sorry:77:25» : Sort _
+-/
+#guard_msgs in example : sorry := (sorry : sorry)
+
+/-!
+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
+
+/-!
+Showing that the sorries in the previous test are labeled.
+-/
+/--
+error: unknown identifier 'a'
+---
+error: unknown identifier 'b'
+---
+info: ⊢ sorry `«sorry:106:10» = sorry `«sorry:106:14»
+-/
+#guard_msgs in
+set_option autoImplicit false in
+set_option pp.sorrySource true 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 8d1685226a75..db3cdf24fcf0 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