Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix unbound variable bug #134

Merged
merged 2 commits into from Sep 14, 2017
Merged

Fix unbound variable bug #134

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9a205d7
Fix unbound variable bug
Gabriella439 Sep 13, 2017
a3a34e5
Update Regression.hs
Gabriella439 Sep 13, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Dhall/TypeCheck.hs
View file
Open in desktop
Expand Up @@ -175,7 +175,7 @@ typeWith ctx e@(Let f mt r b ) = do

let ctx' = Dhall.Context.insert f tR ctx
tB <- typeWith ctx' b
ttB <- fmap Dhall.Core.normalize (typeWith ctx tB)
ttB <- fmap Dhall.Core.normalize (typeWith ctx' tB)
kB <- case ttB of
Const k -> return k
-- Don't bother to provide a `let`-specific version of this error
Expand Down
12 changes: 12 additions & 0 deletions tests/Regression.hs
View file
Open in desktop
Expand Up @@ -85,6 +85,18 @@ parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do
Left e -> Control.Exception.throwIO e
Right _ -> return () )

typeChecking0 :: TestTree
typeChecking0 = Test.Tasty.HUnit.testCase "Type-checking regression #0" (do
-- There used to be a bug in the type-checking logic where `T` would be
-- added to the context when inferring the type of `λ(x : T) → x`, but was
-- missing from the context when inferring the kind of the inferred type
-- (i.e. the kind of `∀(x : T) → T`). This led to an unbound variable
-- error when inferring the kind
--
-- This bug was originally reported in issue #10
_ <- Util.code "let Day : Type = Natural in λ(x : Day) → x"
return ()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a parenthesis missing here (from line 89). This is the cause for Travis build check.

+1 on the fix itself, of course.


trailingSpaceAfterStringLiterals :: TestTree
trailingSpaceAfterStringLiterals =
Test.Tasty.HUnit.testCase "Trailing space after string literals" (do
Expand Down