feat: labeled and unique sorries

src/Init/NotationExtra.lean

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

src/Init/Prelude.lean

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

src/Init/Tactics.lean

@@ -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
+  mkLabeledSorry type (synthetic := false) (unique := true)
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkPairs (elems : Array Term) : MacroM Term :=

src/Lean/Elab/Extra.lean

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

src/Lean/Elab/MutualDef.lean

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

src/Lean/Elab/PreDefinition/Basic.lean

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

src/Lean/Elab/PreDefinition/Main.lean

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

src/Lean/Elab/Tactic/Basic.lean

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

src/Lean/Elab/Tactic/LibrarySearch.lean

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

src/Lean/Elab/Term.lean

@@ -1109,7 +1109,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
@@ -1215,7 +1215,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!
@@ -1771,7 +1771,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPo
     withRef stx <| ensureHasType expectedType? e errorMsgHeader?
   catch ex =>
     if (← read).errToSorry && ex matches .error .. then
-      exceptionToSorry ex expectedType?
+      withRef stx <| exceptionToSorry ex expectedType?
     else
       throw ex
 

src/Lean/Meta/AppBuilder.lean

@@ -9,6 +9,7 @@ import Lean.Util.Recognizers
 import Lean.Meta.SynthInstance
 import Lean.Meta.Check
 import Lean.Meta.DecLevel
+import Lean.Data.Lsp.Utf16
 
 namespace Lean.Meta
 
@@ -512,10 +513,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]
@@ -544,10 +600,6 @@ def mkDefault (α : Expr) : MetaM Expr :=
 def mkOfNonempty (α : Expr) : MetaM Expr := do
   mkAppOptM ``Classical.ofNonempty #[α, none]
 
-/-- Return `sorryAx type` -/
-def mkSyntheticSorry (type : Expr) : MetaM Expr :=
-  return mkApp2 (mkConst ``sorryAx [← getLevel type]) type (mkConst ``Bool.true)
-
 /-- Return `funext h` -/
 def mkFunExt (h : Expr) : MetaM Expr :=
   mkAppM ``funext #[h]

src/Lean/Meta/Check.lean

@@ -78,40 +78,49 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
-      if !a.isApp || !b.isApp then
-        return (a, b)
-      else if a.getAppNumArgs != b.getAppNumArgs then
+      if !a.isApp || !b.isApp || a.getAppNumArgs != b.getAppNumArgs then
         return (a, b)
       else if !(← isDefEq a.getAppFn b.getAppFn) then
-        return (a, b)
+        let (fa, fb) ← visit a.getAppFn b.getAppFn
+        return (mkAppN fa a.getAppArgs, mkAppN fb b.getAppArgs)
       else
-        let fType ← inferType a.getAppFn
-        forallBoundedTelescope fType a.getAppNumArgs fun xs _ => do
-          let mut as := a.getAppArgs
-          let mut bs := b.getAppArgs
-          if let some (as', bs') ← hasExplicitDiff? xs as bs then
-            return (mkAppN a.getAppFn as', mkAppN b.getAppFn bs')
-          else
-            for i in [:as.size] do
-              unless (← isDefEq as[i]! bs[i]!) do
-                let (ai, bi) ← visit as[i]! bs[i]!
-                as := as.set! i ai
-                bs := bs.set! i bi
-            let a := mkAppN a.getAppFn as
-            let b := mkAppN b.getAppFn bs
-            return (a.setAppPPExplicit, b.setAppPPExplicit)
+        -- Note: this isn't using forallBoundedTelescope because the function might be "overapplied".
+        -- That is to say, the arity might depend on the values of the arguments.
+        let mut as := a.getAppArgs
+        let mut bs := b.getAppArgs
+        let mut aFnType ← inferType a.getAppFn
+        let mut bFnType ← inferType b.getAppFn
+        let mut firstDiff? := none
+        for i in [0:as.size] do
+          unless aFnType.isForall do aFnType ← withTransparency .all <| whnf aFnType
+          unless bFnType.isForall do bFnType ← withTransparency .all <| whnf bFnType
+          -- These pattern matches are expected to succeed:
+          let .forallE _ _ abody abi := aFnType | return (a, b)
+          let .forallE _ _ bbody bbi := aFnType | return (a, b)
+          aFnType := abody.instantiate1 as[i]!
+          bFnType := bbody.instantiate1 bs[i]!
+          let explicit := abi.isExplicit && bbi.isExplicit
+          unless (← isDefEq as[i]! bs[i]!) do
+            if explicit then
+              let (ai, bi) ← visit as[i]! bs[i]!
+              let a := mkAppN a.getAppFn (as.set! i ai)
+              let b := mkAppN b.getAppFn (bs.set! i bi)
+              if a.isAppOf ``sorryAx then
+                -- Special case: if this is a `sorry` with source position, make sure the delaborator shows the position.
+                return (a.setOption `pp.sorrySource true, b.setOption `pp.sorrySource true)
+              return (a, b)
+            else
+              firstDiff? := firstDiff? <|> some i
+        if let some i := firstDiff? then
+          let (ai, bi) ← visit as[i]! bs[i]!
+          as := as.set! i ai
+          bs := bs.set! i bi
+        let a := mkAppN a.getAppFn as
+        let b := mkAppN b.getAppFn bs
+        return (a.setPPExplicit true, b.setPPExplicit true)
     catch _ =>
       return (a, b)
 
-  hasExplicitDiff? (xs as bs : Array Expr) : MetaM (Option (Array Expr × Array Expr)) := do
-    for i in [:xs.size] do
-      let localDecl ← xs[i]!.fvarId!.getDecl
-      if localDecl.binderInfo.isExplicit then
-         unless (← isDefEq as[i]! bs[i]!) do
-           let (ai, bi) ← visit as[i]! bs[i]!
-           return some (as.set! i ai, bs.set! i bi)
-    return none
-
 /--
   Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 -/

src/Lean/Meta/Tactic/Util.lean

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

src/Lean/Parser/Term.lean

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