Fix type-on-hover over non-dependent function types (#1233)

Previously, hovering over any part of a non-dependent function type like
`Bool -> Bool` would result in the type of the domain being displayed
(`Bool` in this example). The correct type is `Type`.

This bug resulted from the fact that we
expected all functions types to be syntactically of the form
`forall (b : Bool) -> Bool`, disregarding the simpler syntax for the
non-dependent function space (which desugars to
`forall (_ : Bool) -> Bool`).
This commit is contained in:
Frederik Ramcke 2019-08-20 02:00:18 +00:00 committed by mergify[bot]
parent 6ce01a0eda
commit b997d43efd
2 changed files with 12 additions and 14 deletions

View File

@ -81,11 +81,9 @@ getLetIdentifier src@(Src left _ text) =
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
getLamIdentifier :: Src -> Maybe Src
getLamIdentifier (Src left _ text) =
Megaparsec.parseMaybe (unParser parseLetIdentifier) text
where parseLetIdentifier = do
setSourcePos left
_lambda
@ -97,11 +95,9 @@ getLamIdentifier src@(Src left _ text) =
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
getForallIdentifier :: Src -> Maybe Src
getForallIdentifier (Src left _ text) =
Megaparsec.parseMaybe (unParser parseLetIdentifier) text
where parseLetIdentifier = do
setSourcePos left
_forall

View File

@ -39,12 +39,14 @@ typeAt' pos ctx (Note src (Let (Binding _ _ a :| []) _)) | pos `inside` getLetId
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)
typeAt' pos _ctx (Note src (Lam _ _A _)) | Just src' <- getLamIdentifier src
, pos `inside` src' =
return (Just src', _A)
-- "..." in a forall expression
typeAt' pos _ctx (Note src (Pi _ _A _)) | pos `inside` getForallIdentifier src =
return (Just $ getForallIdentifier src, _A)
typeAt' pos _ctx (Note src (Pi _ _A _)) | Just src' <- getForallIdentifier src
, pos `inside` src' =
return (Just src', _A)
-- the input only contains singleton lets
typeAt' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src = do