feat: unique sorries

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

Details:

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

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

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

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

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

src/Init/NotationExtra.lean

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

src/Init/Prelude.lean

@@ -645,14 +645,15 @@ 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)`.
+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.
+
+"Go to definition" on `sorry` will go to the source position where it was introduced.
 
 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 +662,7 @@ suppresses follow-up errors in order to prevent one error from causing a cascade
 of other errors because the desired term was not constructed.
 -/
 @[extern "lean_sorry", never_extract]
-axiom sorryAx (α : Sort u) (synthetic := false) : α
+axiom sorryAx (α : Sort u) (synthetic : Bool) : α
 
 theorem eq_false_of_ne_true : {b : Bool} → Not (Eq b true) → Eq b false
   | true, h => False.elim (h rfl)

src/Init/Tactics.lean

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

src/Lean/Elab/BuiltinNotation.lean

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

src/Lean/Elab/PreDefinition/Basic.lean

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

src/Lean/Elab/Term.lean

@@ -1107,7 +1107,7 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr :
   let expectedType ← match expectedType? with
     | none              => mkFreshTypeMVar
     | some expectedType => pure expectedType
-  mkSyntheticSorry expectedType
+  mkSorry expectedType (synthetic := true)
 
 /--
   Log the given exception, and create a synthetic sorry for representing the failed

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
 
@@ -512,10 +513,59 @@ def mkSome (type value : Expr) : MetaM Expr := do
   let u ← getDecLevel type
   return mkApp2 (mkConst ``Option.some [u]) type value
 
+/--
+Return `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 UniqueSorryView where
+  module? : Option Name := none
+  range? : Option Lsp.Range := none
+
+def UniqueSorryView.encode (view : UniqueSorryView) : CoreM Name :=
+  let name := view.module?.getD .anonymous
+  let name :=
+    if let some range := view.range? then
+      name |>.num range.start.line |>.num range.start.character |>.num range.end.line |>.num range.end.character
+    else
+      name
+  mkFreshUserName (name.str "_unique_sorry")
+
+def UniqueSorryView.decode? (name : Name) : Option UniqueSorryView := 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? := name, range? := some ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩ }
+  else if name.isAnonymous then
+    return { module? := none, range? := none }
+  else
+    failure
+
+/--
+Make a `sorryAx` that is unique, in the sense that it is not defeq to any other `sorry` created by `mkUniqueSorry`.
+
+Encodes the source position of the current ref into the term.
+-/
+def mkUniqueSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
+  let tag ←
+    if let (some pos, some endPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
+      let range := (← getFileMap).utf8RangeToLspRange ⟨pos, endPos⟩
+      UniqueSorryView.encode { module? := (← getMainModule), range? := range }
+    else
+      UniqueSorryView.encode {}
+  let e ← mkSorry (mkForall `tag .default (mkConst ``Lean.Name) type) synthetic
+  return .app e (toExpr tag)
+
+/--
+Return a `UniqueSorryView` if `e` is an application of an expression returned by `mkUniqueSorry`.
+-/
+def isUniqueSorry? (e : Expr) : Option UniqueSorryView := do
+  guard <| e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 3
+  let some tag := (e.getArg! 2).name? | failure
+  UniqueSorryView.decode? tag
+
 /-- Return `Decidable.decide p` -/
 def mkDecide (p : Expr) : MetaM Expr :=
   mkAppOptM ``Decidable.decide #[p, none]
@@ -544,10 +594,6 @@ def mkDefault (α : Expr) : MetaM Expr :=
 def mkOfNonempty (α : Expr) : MetaM Expr := do
   mkAppOptM ``Classical.ofNonempty #[α, none]
 
-/-- Return `sorryAx type` -/
-def mkSyntheticSorry (type : Expr) : MetaM Expr :=
-  return mkApp2 (mkConst ``sorryAx [← getLevel type]) type (mkConst ``Bool.true)
-
 /-- Return `funext h` -/
 def mkFunExt (h : Expr) : MetaM Expr :=
   mkAppM ``funext #[h]

src/Lean/Parser/Term.lean

@@ -215,7 +215,21 @@ 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.
+
+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`.
+
+Each `sorry` is guaranteed to be unique, so for example the following fails:
+```lean
+example : (sorry : Nat) = sorry := rfl -- fails
+```
+
+See also the `sorry` tactic, which is short for `exact sorry`.
+-/
 @[builtin_term_parser] def «sorry» := leading_parser
   "sorry"
 /--

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1226,6 +1226,16 @@ 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 do
+  guard <| (← getExpr).getAppNumArgs ≥ 2
+  let mut arity := 2
+  -- If this is constructed by `Lean.Meta.mkUniqueSorry`, then don't print the unique tag.
+  if isUniqueSorry? (← getExpr) |>.isSome then
+    arity := 3
+  withOverApp arity do
+    `(sorry)
+
 open Parser Command Term in
 @[run_builtin_parser_attribute_hooks]
 -- use `termParser` instead of `declId` so we can reuse `delabConst`

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -197,6 +197,14 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
             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.isUniqueSorry? expr then
+          if let (some module, some range) := (view.module?, view.range?) 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
   | .ofFieldInfo fi =>
     if kind == type then

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

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)

tests/lean/run/sorry.lean

@@ -24,3 +24,37 @@ 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