ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Correctly handle dependent types in dhall-lsp-server (#1216)

Browse Source 
* Correctly handle dependent types in dhall-lsp-server

Removes the "fast path" when typechecking `let`s whose bound expression
has a small type. This optimisation is no longer legal in the presence
of dependent types (as introduced in #1164).

* Fix bad merge

* Remove redundant import
This commit is contained in:
Frederik Ramcke 2019-08-12 13:27:41 +00:00 committed by mergify[bot]
parent 0348d18ac7
commit 8c3db821db
2 changed files with 8 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -18,7 +18,7 @@ import Dhall.Src (Src(..))
import Dhall.Parser
import Dhall.Parser.Token
import Dhall.Parser.Expression
import Text.Megaparsec ((<|>), try, skipManyTill, lookAhead, anySingle,
import Text.Megaparsec (try, skipManyTill, lookAhead, anySingle,
notFollowedBy, eof, takeRest)
import Control.Applicative (optional, (<|>))

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

@ -1,7 +1,7 @@
module Dhall.LSP.Backend.Typing (annotateLet, exprAt, srcAt, typeAt) where
import Dhall.Context (Context, insert, empty)
import Dhall.Core (Expr(..), Binding(..), Const(..), subExpressions, normalize, shift, subst, Var(..), pretty)
import Dhall.Core (Expr(..), Binding(..), subExpressions, normalize, shift, subst, Var(..), pretty)
import Dhall.TypeCheck (typeWithA, X, TypeError(..))
import Dhall.Parser (Src(..))
@ -48,16 +48,9 @@ typeAt' pos _ctx (Note src (Pi _ _A _)) | pos `inside` getForallIdentifier src =
-- 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
t <- fmap normalize (typeWithA absurd ctx _A)
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)
(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))
_ <- typeWithA absurd ctx a
let a' = shift 1 (V x 0) (normalize a)
typeAt' pos ctx (shift (-1) (V x 0) (subst (V x 0) a' e))
typeAt' pos ctx (Lam x _A b@(Note src _)) | pos `inside` src = do
let _A' = Dhall.Core.normalize _A
@ -126,15 +119,9 @@ annotateLet' pos ctx (Note src e@(Let (Binding _ _ a :| []) _))
-- binders, see typeAt'
annotateLet' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src = do
_A <- first show $ typeWithA absurd ctx a
t <- first show $ fmap normalize (typeWithA absurd ctx _A)
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)
annotateLet' pos ctx' e
_ -> do -- but we do have types depending on types
let a' = shift 1 (V x 0) (normalize a)
annotateLet' pos ctx (shift (-1) (V x 0) (subst (V x 0) a' e))
_ <- first show $ typeWithA absurd ctx a
let a' = shift 1 (V x 0) (normalize a)
annotateLet' pos ctx (shift (-1) (V x 0) (subst (V x 0) a' e))
annotateLet' pos ctx (Lam x _A b@(Note src _)) | pos `inside` src = do
let _A' = Dhall.Core.normalize _A