feat: show expected type on/after := of let

Kha · Jun 3, 2022 · 30278e8 · 30278e8
1 parent 8649483
commit 30278e8
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
@@ -581,7 +581,7 @@ open Lean.Elab.Term.Quotation in
 
    The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
    If `elabBodyFirst == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. -/
-def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)
+def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (valStx valRef : Syntax) (body : Syntax)
     (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
   let (type, val, binders) ← elabBindersEx binders fun xs => do
     let (binders, fvars) := xs.unzip
@@ -592,7 +592,8 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       let val  ← mkFreshExprMVar type
       pure (type, val, binders)
     else
-      let val  ← elabTermEnsuringType valStx type
+      let val ← withInfoContext' valRef (mkInfo := mkTermInfo Name.anonymous (expectedType? := type) valRef) <|
+        elabTermEnsuringType valStx type
       let type ← mkForallFVars fvars type
       /- By default `mkLambdaFVars` and `mkLetFVars` create binders only for let-declarations that are actually used
          in the body. This generates counterintuitive behavior in the elaborator since users will not be notified
@@ -658,7 +659,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
   let body    := stx[3]
   if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
     let { id := id, binders := binders, type := type, value := val } := mkLetIdDeclView letDecl
-    elabLetDeclAux id binders type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
+    elabLetDeclAux id binders type val letDecl[3] body expectedType? useLetExpr elabBodyFirst usedLetOnly
   else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then
     -- node `Lean.Parser.Term.letPatDecl  $ try (termParser >> pushNone >> optType >> " := ") >> termParser
     if elabBodyFirst then
@@ -670,7 +671,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
       -- `let _ := ...` should not be treated at a `letIdDecl`
       let id   := mkIdentFrom pat `_
       let type := expandOptType id optType
-      elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
+      elabLetDeclAux id #[] type val letDecl[3] body expectedType? useLetExpr elabBodyFirst usedLetOnly
     else
       -- We are currently treating `let_fun` and `let` the same way when patterns are used.
       let stxNew ←

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
@@ -318,9 +318,11 @@ partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option
     else
       headFns
   t.smallestInfo? fun i => Id.run do
-    if i.contains hoverPos then
-      if let Info.ofTermInfo ti := i then
-        return !ti.stx.isIdent || !headFns.contains i.pos?.get!
+    if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
+      let trailSize := i.stx.getTrailingSize
+      if pos ≤ hoverPos ∧ hoverPos.byteIdx < tailPos.byteIdx + trailSize then
+        if let Info.ofTermInfo ti := i then
+          return !ti.stx.isIdent || !headFns.contains i.pos?.get!
     false
   where
     /- Returns the position of the head function symbol, if it is an identifier. -/