dhall-lsp-server: Improve type-on-hover behaviour over binders (#1062)

* Improve type-on-hover behaviour over binders

Dhall's parser does not generate `Src` annotations for the names in
binders, which means that it's not quite as straight-forward to check
whether the user meant to hover over it and see its type as one would
hope. As a result, the current "naive" implementation sometimes behaves
slightly unintuitively and returns the type of the entire expression,
rather than the type of the bound variable. E.g.
  let x = 2 in "text"
      ~
would result in the type `Text` being displayed, rather than `Natural`
as one would expect. Since the language server also marks the expression
whose type is being displayed, the behaviour isn't quite that bad in
practice (we aren't falsely led to believe that `x` has type `Text`).

This change recovers the `Src` information describing the bound variable
names and handles those cases in a way that should be more in line with
the expectations of the user.

* Fix exprAt not handling multi-lets correctly

* Fix merge left-overs

dhall-lsp-server/src/Dhall/LSP/Backend/Parsing.hs

@@ -1,4 +1,10 @@
-module Dhall.LSP.Backend.Parsing (getLetInner, getLetAnnot) where
+module Dhall.LSP.Backend.Parsing
+  ( getLetInner
+  , getLetAnnot
+  , getLetIdentifier
+  , getLamIdentifier
+  , getForallIdentifier)
+where
 
 import Dhall.Src (Src(..))
 import Dhall.Parser
@@ -47,6 +53,56 @@ getLetAnnot (Src left _ text) = Megaparsec.parseMaybe (unParser parseLetAnnot) t
           _ <- Megaparsec.takeRest
           return (Src begin end tokens)
 
+-- | Given an Src of a let expression return the Src containing the bound
+--   identifier, i.e. given `let x = ... in ...` return the Src descriptor
+--   containing `x`. Returns the original Src if something goes wrong.
+getLetIdentifier :: Src -> Src
+getLetIdentifier src@(Src left _ text) =
+  case Megaparsec.parseMaybe (unParser parseLetIdentifier) text of
+    Just src' -> src'
+    Nothing -> src
+  where parseLetIdentifier = do
+          setSourcePos left
+          _let
+          begin <- getSourcePos
+          (tokens, _) <- Megaparsec.match label
+          end <- getSourcePos
+          _ <- Megaparsec.takeRest
+          return (Src begin end tokens)
+
+-- | Cf. `getLetIdentifier`.
+getLamIdentifier :: Src -> Src
+getLamIdentifier src@(Src left _ text) =
+  case Megaparsec.parseMaybe (unParser parseLetIdentifier) text of
+    Just src' -> src'
+    Nothing -> src
+  where parseLetIdentifier = do
+          setSourcePos left
+          _lambda
+          _openParens
+          begin <- getSourcePos
+          (tokens, _) <- Megaparsec.match label
+          end <- getSourcePos
+          _ <- Megaparsec.takeRest
+          return (Src begin end tokens)
+
+-- | Cf. `getLetIdentifier`.
+getForallIdentifier :: Src -> Src
+getForallIdentifier src@(Src left _ text) =
+  case Megaparsec.parseMaybe (unParser parseLetIdentifier) text of
+    Just src' -> src'
+    Nothing -> src
+  where parseLetIdentifier = do
+          setSourcePos left
+          _forall
+          _openParens
+          begin <- getSourcePos
+          (tokens, _) <- Megaparsec.match label
+          end <- getSourcePos
+          _ <- Megaparsec.takeRest
+          return (Src begin end tokens)
+
+
 setSourcePos :: SourcePos -> Parser ()
 setSourcePos src = Megaparsec.updateParserState
                      (\(Megaparsec.State s o (Megaparsec.PosState i o' _ t l)) ->

dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs

@@ -9,9 +9,10 @@ import Data.List.NonEmpty (NonEmpty (..))
 import Control.Lens (toListOf)
 import Data.Text (Text)
 import Control.Applicative ((<|>))
-import Data.Bifunctor (first, bimap)
+import Data.Bifunctor (first)
 
-import Dhall.LSP.Backend.Parsing (getLetInner, getLetAnnot)
+import Dhall.LSP.Backend.Parsing (getLetInner, getLetAnnot, getLetIdentifier,
+  getLamIdentifier, getForallIdentifier)
 import Dhall.LSP.Backend.Diagnostics (Position, Range(..), rangeFromDhall)
 import Dhall.LSP.Backend.Dhall (WellTyped, fromWellTyped)
 
@@ -20,16 +21,33 @@ import qualified Data.Text.Prettyprint.Doc.Render.Text     as Pretty
 import Dhall.Pretty (CharacterSet(..), prettyCharacterSet)
 
 -- | Find the type of the subexpression at the given position. Assumes that the
---   input expression is well-typed.
-typeAt :: Position -> WellTyped -> Either String (Expr Src X)
+--   input expression is well-typed. Also returns the Src descriptor containing
+--   that subexpression if possible.
+typeAt :: Position -> WellTyped -> Either String (Maybe Src, Expr Src X)
 typeAt pos expr = do
   expr' <- case splitLets (fromWellTyped expr) of
              Just e -> return e
              Nothing -> Left "The impossible happened: failed to split let\
                               \ blocks when preprocessing for typeAt'."
-  bimap show normalize $ typeAt' pos empty expr'
+  (mSrc, typ) <- first show $ typeAt' pos empty expr'
+  case mSrc of
+    Just src -> return (Just src, normalize typ)
+    Nothing -> return (srcAt pos expr', normalize typ)
+
+typeAt' :: Position -> Context (Expr Src X) -> Expr Src X -> Either (TypeError Src X) (Maybe Src, Expr Src X)
+-- the user hovered over the bound name in a let expression
+typeAt' pos ctx (Note src (Let (Binding _ _ a :| []) _)) | pos `inside` getLetIdentifier src = do
+  typ <- typeWithA absurd ctx a
+  return (Just $ getLetIdentifier src, typ)
+
+-- "..." in a lambda expression
+typeAt' pos _ctx (Note src (Lam _ _A _)) | pos `inside` getLamIdentifier src =
+  return (Just $ getLamIdentifier src, _A)
+
+-- "..." in a forall expression
+typeAt' pos _ctx (Note src (Pi _ _A _)) | pos `inside` getForallIdentifier src =
+  return (Just $ getForallIdentifier src, _A)
 
-typeAt' :: Position -> Context (Expr Src X) -> Expr Src X -> Either (TypeError Src X) (Expr Src X)
 -- the input only contains singleton lets
 typeAt' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src = do
   _A <- typeWithA absurd ctx a
@@ -37,8 +55,8 @@ typeAt' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src =
   case t of
     Const Type -> do  -- we don't have types depending on values
       let ctx' = fmap (shift 1 (V x 0)) (insert x (normalize _A) ctx)
-      _B <- typeAt' pos ctx' e
-      return (shift (-1) (V x 0) _B)
+      (mSrc, _B) <- typeAt' pos ctx' e
+      return (mSrc, shift (-1) (V x 0) _B)
     _ -> do  -- but we do have types depending on types
       let a' = shift 1 (V x 0) (normalize a)
       typeAt' pos ctx (shift (-1) (V x 0) (subst (V x 0) a' e))
@@ -53,25 +71,30 @@ typeAt' pos ctx (Pi x _A  _B@(Note src _)) | pos `inside` src = do
       ctx' = fmap (shift 1 (V x 0)) (insert x _A' ctx)
   typeAt' pos ctx' _B
 
--- peel of a single Note constructor
+-- peel off a single Note constructor
 typeAt' pos ctx (Note _ expr) = typeAt' pos ctx expr
 
 -- catch-all
 typeAt' pos ctx expr = do
   let subExprs = toListOf subExpressions expr
   case [ (src, e) | (Note src e) <- subExprs, pos `inside` src ] of
-    [] -> typeWithA absurd ctx expr  -- return type of whole expression
-    ((src, e):_) -> typeAt' pos ctx (Note src e)  -- continue with subexpression
+    [] -> do typ <- typeWithA absurd ctx expr  -- return type of whole subexpression
+             return (Nothing, typ)
+    ((src, e):_) -> typeAt' pos ctx (Note src e)  -- continue with leaf-expression
 
 
 -- | Find the smallest Note-wrapped expression at the given position.
 exprAt :: Position -> Expr Src a -> Maybe (Expr Src a)
-exprAt pos e@(Note _ expr) = exprAt pos expr <|> Just e
-exprAt pos expr =
+exprAt pos e = do e' <- splitLets e
+                  exprAt' pos e'
+
+exprAt' :: Position -> Expr Src a -> Maybe (Expr Src a)
+exprAt' pos e@(Note _ expr) = exprAt pos expr <|> Just e
+exprAt' pos expr =
   let subExprs = toListOf subExpressions expr
   in case [ (src, e) | (Note src e) <- subExprs, pos `inside` src ] of
     [] -> Nothing
-    ((src,e) : _) -> exprAt pos e <|> Just (Note src e)
+    ((src,e) : _) -> exprAt' pos e <|> Just (Note src e)
 
 
 -- | Find the smallest Src annotation containing the given position.

dhall-lsp-server/src/Dhall/LSP/Handlers.hs

@@ -14,12 +14,12 @@ import Dhall.TypeCheck (X)
 
 import Dhall.LSP.Backend.Dhall (FileIdentifier, parse, load, typecheck,
   normalize, fileIdentifierFromFilePath, fileIdentifierFromURI, invalidate,
-  cacheExpr, parseWithHeader, fromWellTyped)
+  cacheExpr, parseWithHeader)
 import Dhall.LSP.Backend.Diagnostics (Range(..), Diagnosis(..), explain,
   rangeFromDhall, diagnose)
 import Dhall.LSP.Backend.Formatting (formatExprWithHeader)
 import Dhall.LSP.Backend.Linting (Suggestion(..), suggest, lint)
-import Dhall.LSP.Backend.Typing (typeAt, srcAt, annotateLet)
+import Dhall.LSP.Backend.Typing (typeAt, annotateLet)
 import Dhall.LSP.State
 
 import Control.Applicative ((<|>))
@@ -167,9 +167,8 @@ hoverType request = do
     Right wt -> return wt
   case typeAt (line,col) welltyped of
     Left err -> throwE (Error, Text.pack err)
-    Right typ ->
-      let _range = fmap (rangeToJSON . rangeFromDhall)
-                        (srcAt (line,col) (fromWellTyped welltyped))
+    Right (mSrc, typ) ->
+      let _range = fmap (rangeToJSON . rangeFromDhall) mSrc
           _contents = J.List [J.PlainString (pretty typ)]
           hover = J.Hover{..}
       in lspRespond LSP.RspHover request (Just hover)