pervasive mkUniqueSorry

Author: kmill

src/Init/Prelude.lean

@@ -648,13 +648,11 @@ set_option linter.unusedVariables.funArgs false in
 Auxiliary axiom used to implement the `sorry` term and tactic.
 
 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
+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.
 
-"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
 in the expression. A synthetic `sorry` acts like a regular one, except that it

src/Init/Tactics.lean

@@ -403,7 +403,7 @@ syntax (name := acRfl) "ac_rfl" : tactic
 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.
+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`.

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
+        mkUniqueSorry expectedType false
 
 builtin_initialize
   registerTraceClass `Elab.binop

src/Lean/Elab/MutualDef.lean

@@ -977,7 +977,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 <| mkUniqueSorry header.type (synthetic := true)
         let headers ← headers.mapM instantiateMVarsAtHeader
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift

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 <| mkUniqueSorry type (synthetic := 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 <| mkUniqueSorry preDef.type (synthetic := 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 (← mkUniqueSorry mvarType (synthetic := 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)
+        mkUniqueSorry expectedType (synthetic := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta
         instantiateMVars goal

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
-  mkSorry expectedType (synthetic := true)
+  mkUniqueSorry expectedType (synthetic := true)
 
 /--
   Log the given exception, and create a synthetic sorry for representing the failed
@@ -1213,7 +1213,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 <| mkUniqueSorry type false
   else
     let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
     let mvarId := mvar.mvarId!
@@ -1769,7 +1769,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

@@ -514,7 +514,7 @@ def mkSome (type value : Expr) : MetaM Expr := do
   return mkApp2 (mkConst ``Option.some [u]) type value
 
 /--
-Return `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
+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
@@ -544,7 +544,7 @@ def UniqueSorryView.decode? (name : Name) : Option UniqueSorryView := do
     failure
 
 /--
-Make a `sorryAx` that is unique, in the sense that it is not defeq to any other `sorry` created by `mkUniqueSorry`.
+Makes 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.
 -/
@@ -559,7 +559,7 @@ def mkUniqueSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
   return .app e (toExpr tag)
 
 /--
-Return a `UniqueSorryView` if `e` is an application of an expression returned by `mkUniqueSorry`.
+Returns 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

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 ← mkUniqueSorry mvarType synthetic
     mvarId.assign val
 
 /-- Beta reduce the metavariable type head -/

src/Lean/Parser/Term.lean

@@ -218,11 +218,13 @@ def binderIdent : Parser  := ident <|> hole
 /--
 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
+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

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -212,7 +212,7 @@ where
   }
 
 /--
-Annotates the term with the current expression position and registers `TermInfo`
+Annotate the term with the current expression position and register `TermInfo`
 to associate the term to the current expression.
 -/
 def annotateTermInfo (stx : Term) : Delab := do
@@ -221,13 +221,31 @@ 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 (1) the syntax has a position and it is for the current position
+and (2) there is already `TermInfo` at this position.
+-/
+def annotateTermInfoUnlessAnnotated (stx : Term) : Delab := do
+  if let .synthetic ⟨pos⟩ ⟨pos'⟩ := stx.raw.getHeadInfo then
+    if pos == pos' && pos == (← getPos) then
+      if (← 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
+
 def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
   -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
   let suggestion := if suggestion.isAnonymous then `a else suggestion
@@ -271,11 +289,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
@@ -365,7 +385,7 @@ def omission (reason : OmissionReason) : Delab := do
 partial def delabFor : Name → Delab
   | Name.anonymous => failure
   | k              =>
-    (do annotateTermInfo (← (delabAttribute.getValues (← getEnv) k).firstM id))
+    (do annotateTermInfoUnlessAnnotated (← (delabAttribute.getValues (← getEnv) k).firstM id))
     -- have `app.Option.some` fall back to `app` etc.
     <|> if k.isAtomic then failure else delabFor k.getRoot
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -573,7 +573,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]
@@ -1227,14 +1227,30 @@ def delabNameMkStr : Delab := whenPPOption getPPNotation do
 def delabNameMkNum : Delab := delabNameMkStr
 
 @[builtin_delab app.sorryAx]
-def delabSorry : Delab := whenPPOption getPPNotation do
+def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExplicit 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)
+  -- But, if `pp.explicit` is false and `pp.sorrySource` is true, then print a simplified version of the tag.
+  if let some view := isUniqueSorry? (← getExpr) then
+    withOverApp 3 do
+      if let (some module, some range) := (view.module?, view.range?) then
+        if ← 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]

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -34,6 +34,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"
@@ -250,6 +255,7 @@ def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
 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)

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -151,8 +151,17 @@ 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
@@ -206,6 +215,11 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
             }
             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
@@ -220,13 +234,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)

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.