unique -> labeled sorries. Turns out using unique sorries for elaboration errors can compound the issues. In any case, they can still be labeled.

improves addPPExplicitToExposeDiff when functions are overapplied

fixes mdata bugs in location RPC handler

fixes #4972

Author: kmill

src/Lean/Elab/BuiltinNotation.lean

@@ -214,7 +214,7 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
 
 @[builtin_term_elab «sorry»] def elabSorry : TermElab := fun _ expectedType? => do
   let type ← expectedType?.getDM mkFreshTypeMVar
-  mkUniqueSorry type (synthetic := false)
+  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.
-        mkUniqueSorry 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 => withRef header.declId <| mkUniqueSorry header.type (synthetic := true)
+            headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := false)
         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 (← withRef preDef.ref <| mkUniqueSorry 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 := (← withRef preDef.ref <| mkUniqueSorry 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 (← mkUniqueSorry 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."
-        mkUniqueSorry 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
-  mkUniqueSorry expectedType (synthetic := true)
+  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
-    withRef tacticCode <| mkUniqueSorry type false
+    withRef tacticCode <| mkLabeledSorry type false (unique := true)
   else
     let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
     let mvarId := mvar.mvarId!

src/Lean/Meta/AppBuilder.lean

@@ -520,51 +520,57 @@ 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
+structure SorryLabelView where
+  module? : Option (Name × Lsp.Range) := none
 
-def UniqueSorryView.encode (view : UniqueSorryView) : CoreM Name :=
-  let name := view.module?.getD .anonymous
+def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
   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
+    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
-      name
+      .anonymous
   mkFreshUserName (name.str "_unique_sorry")
 
-def UniqueSorryView.decode? (name : Name) : Option UniqueSorryView := do
+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? := name, range? := some ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩ }
-  else if name.isAnonymous then
-    return { module? := none, range? := none }
+    return { module? := some (name, ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩) }
   else
     failure
 
 /--
-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.
+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 mkUniqueSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
+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⟩
-      UniqueSorryView.encode { module? := (← getMainModule), range? := range }
+      SorryLabelView.encode { module? := (← getMainModule, range) }
     else
-      UniqueSorryView.encode {}
-  let e ← mkSorry (mkForall `tag .default (mkConst ``Lean.Name) type) synthetic
-  return .app e (toExpr tag)
+      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 `UniqueSorryView` if `e` is an application of an expression returned by `mkUniqueSorry`.
+Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
 -/
-def isUniqueSorry? (e : Expr) : Option UniqueSorryView := do
+def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
   guard <| e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 3
-  let some tag := (e.getArg! 2).name? | failure
-  UniqueSorryView.decode? tag
+  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 :=

src/Lean/Meta/Check.lean

@@ -78,40 +78,51 @@ 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
+      if ← isDefEq a b then
         return (a, b)
-      else if a.getAppNumArgs != b.getAppNumArgs then
+      else 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 ← mkUniqueSorry mvarType synthetic
+    let val ← mkLabeledSorry mvarType synthetic (unique := true)
     mvarId.assign val
 
 /-- Beta reduce the metavariable type head -/

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -222,14 +222,13 @@ def annotateTermInfo (stx : Term) : Delab := do
 
 /--
 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.
+to associate the term to the current expression, unless the syntax has a synthetic position
+and associated `Info` already.
 -/
 def annotateTermInfoUnlessAnnotated (stx : Term) : Delab := do
   if let .synthetic ⟨pos⟩ ⟨pos'⟩ := stx.raw.getHeadInfo then
-    if pos == pos' && pos == (← getPos) then
-      if (← get).infos.contains pos then
-        return stx
+    if pos == pos' && (← get).infos.contains pos then
+      return stx
   annotateTermInfo stx
 
 /--

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1014,15 +1014,15 @@ Delaborates an `OfNat.ofNat` literal.
 `@OfNat.ofNat _ n _` ~> `n`.
 -/
 @[builtin_delab app.OfNat.ofNat]
-def delabOfNat : Delab := whenPPOption getPPCoercions <| withOverApp 3 do
+def delabOfNat : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 3 do
   delabOfNatCore (showType := (← getPPOption getPPNumericTypes))
 
 /--
 Delaborates the negative of an `OfNat.ofNat` literal.
 `[email protected] _ n _` ~> `-n`
 -/
 @[builtin_delab app.Neg.neg]
-def delabNeg : Delab := whenPPOption getPPCoercions do
+def delabNeg : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions do
   delabNegIntCore (showType := (← getPPOption getPPNumericTypes))
 
 /--
@@ -1031,12 +1031,12 @@ Delaborates a rational number literal.
 and `[email protected] _ n _ / @OfNat.ofNat _ m` ~> `-n / m`
 -/
 @[builtin_delab app.HDiv.hDiv]
-def delabHDiv : Delab := whenPPOption getPPCoercions do
+def delabHDiv : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions do
   delabDivRatCore (showType := (← getPPOption getPPNumericTypes))
 
 -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
 @[builtin_delab app.OfScientific.ofScientific]
-def delabOfScientific : Delab := whenPPOption getPPCoercions <| withOverApp 5 do
+def delabOfScientific : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 5 do
   let expr ← getExpr
   guard <| expr.getAppNumArgs == 5
   let .lit (.natVal m) ← pure (expr.getArg! 2) | failure
@@ -1229,12 +1229,13 @@ def delabNameMkNum : Delab := delabNameMkStr
 @[builtin_delab app.sorryAx]
 def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExplicit do
   guard <| (← getExpr).getAppNumArgs ≥ 2
-  -- If this is constructed by `Lean.Meta.mkUniqueSorry`, then don't print the unique tag.
+  let sorrySource ← getPPOption getPPSorrySource
+  -- If this is constructed by `Lean.Meta.mkLabeledSorry`, then don't print the unique tag.
   -- But, if `pp.explicit` is false and `pp.sorrySource` is true, then print a simplified version of the tag.
-  if let some view := isUniqueSorry? (← getExpr) then
+  if let some view := isLabeledSorry? (← getExpr) then
     withOverApp 3 do
-      if let (some module, some range) := (view.module?, view.range?) then
-        if ← getPPOption getPPSorrySource then
+      if let some (module, range) := view.module? then
+        if ← pure sorrySource <||> getPPOption getPPSorrySource then
           -- LSP line numbers start at 0, so add one to it.
           -- Technically using the character as the column is incorrect since this is UTF-16 position, but we have no filemap to work with.
           let posAsName := Name.mkSimple s!"{module}:{range.start.line + 1}:{range.start.character}"

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -165,7 +165,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
     let mut expr := ti.expr
     if kind == type then
       expr ← ci.runMetaM i.lctx do
-        return Expr.getAppFn (← instantiateMVars (← Meta.inferType expr))
+        return Expr.getAppFn (← instantiateMVars (← Meta.inferType expr)) |>.consumeMData
     match expr with
     | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
     | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
@@ -184,7 +184,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
@@ -201,13 +201,14 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
             | .const declName _ => do
               if ← ci.runMetaM i.lctx do Lean.Meta.isInstance declName then pure #[declName] else pure #[]
             | .app fn arg => do pure $ (← extractInstances fn).append (← extractInstances arg)
+            | .mdata _ e => extractInstances e
             | _ => pure #[]
           if let some instArg := appArgs.get? instIdx then
             for inst in (← extractInstances instArg) do
               results := results.append (← ci.runMetaM i.lctx <| locationLinksFromDecl i inst)
             results := results.append elaborators -- put elaborators at the end of the results
-        if let some view := Meta.isUniqueSorry? expr then
-          if let (some module, some range) := (view.module?, view.range?) then
+        if let some view := Meta.isLabeledSorry? expr then
+          if let some (module, range) := view.module? then
             let targetUri := (← documentUriFromModule rc.srcSearchPath module).getD doc.meta.uri
             let result := {
               targetUri, targetRange := range, targetSelectionRange := range,

src/Lean/Util/Sorry.lean

@@ -10,15 +10,21 @@ import Lean.Declaration
 namespace Lean
 
 def Expr.isSorry : Expr → Bool
-  | app (app (.const ``sorryAx ..) ..) .. => true
+  | mkApp2 (.const ``sorryAx ..) _ _ => true
+  -- A unique sorry:
+  | mkApp3 (.const ``sorryAx ..) _ _ _ => true
   | _ => false
 
 def Expr.isSyntheticSorry : Expr → Bool
-  | app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) => true
+  | mkApp2 (const ``sorryAx ..) _ (const ``Bool.true ..) => true
+  -- A unique sorry:
+  | mkApp3 (const ``sorryAx ..) _ (const ``Bool.true ..) _ => true
   | _ => false
 
 def Expr.isNonSyntheticSorry : Expr → Bool
-  | app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) => true
+  | mkApp2 (const ``sorryAx ..) _ (const ``Bool.false ..) => true
+  -- A unique sorry:
+  | mkApp3 (const ``sorryAx ..) _ (const ``Bool.false ..) _ => true
   | _ => false
 
 def Expr.hasSorry (e : Expr) : Bool :=