feat: add support for displaying conv goal in interactive mode

src/Lean/Meta/PPGoal.lean

@@ -144,7 +144,20 @@ end ToHide
 private def addLine (fmt : Format) : Format :=
   if fmt.isNil then fmt else fmt ++ Format.line
 
-def ppGoal (mvarId : MVarId) (convGoal := false) : MetaM Format := do
+/--
+  Return the target type for the given goal.
+  If `inConv == true` and target type is an equality, then return the left-hand-side only. -/
+def getGoalTarget (mvarDecl : MetavarDecl) (inConv : Bool) : MetaM Expr := do
+  let target ← instantiateMVars mvarDecl.type
+  if inConv then
+    if let some (_, lhs, _) ← matchEq? target then
+      instantiateMVars lhs
+    else
+      return target
+  else
+    return target
+
+def ppGoal (mvarId : MVarId) (inConv := false) : MetaM Format := do
   match (← getMCtx).findDecl? mvarId with
   | none          => pure "unknown goal"
   | some mvarDecl => do
@@ -201,14 +214,7 @@ def ppGoal (mvarId : MVarId) (convGoal := false) : MetaM Format := do
            ppVars varNames prevType? fmt localDecl
       let fmt ← pushPending varNames type? fmt
       let fmt := addLine fmt
-      let typeFmt ←
-        if convGoal then
-          if let some (_, lhs, _) ← matchEq? mvarDecl.type then
-            ppExpr lhs
-          else
-            ppExpr mvarDecl.type
-        else
-          ppExpr mvarDecl.type
+      let typeFmt ← ppExpr (← getGoalTarget mvarDecl inConv)
       let fmt := fmt ++ "⊢ " ++ Format.nest indent typeFmt
       match mvarDecl.userName with
       | Name.anonymous => pure fmt

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -148,7 +148,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
             let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
             let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
-            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g))
+            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g ti.inConv))
           return some { goals := goals.toArray }
 
       return none
@@ -182,7 +182,7 @@ partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
          -- for binders, hide the last hypothesis (the binder itself)
          let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
          let goal ← ci.runMetaM lctx' do
-           Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
+           Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! (inConv := false)
          let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
          return some { goal with range }
       return none

src/Lean/Widget/InteractiveGoal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Wojciech Nawrocki
 -/
+import Lean.Meta.PPGoal
 import Lean.Widget.InteractiveCode
 
 /-! RPC procedures for retrieving tactic and term goals with embedded `CodeWithInfos`. -/
@@ -65,7 +66,7 @@ structure InteractiveGoals where
 
 open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
-def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
+def goalToInteractive (mvarId : MVarId) (inConv : Bool) : MetaM InteractiveGoal := do
   let some mvarDecl ← (← getMCtx).findDecl? mvarId
     | throwError "unknown goal {mvarId}"
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
@@ -117,7 +118,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
         else
           ppVars varNames prevType? hyps localDecl
     let hyps ← pushPending varNames type? hyps
-    let goalTp ← instantiateMVars mvarDecl.type
+    let goalTp ← getGoalTarget mvarDecl inConv
     let goalFmt ← exprToInteractive goalTp
     let userName? := match mvarDecl.userName with
       | Name.anonymous => none