Skip to content

Commit

Permalink
Fixed mixed field access (#694)
Browse files Browse the repository at this point in the history
Fixes #692

The standard permits a user to access a constructor from a type stored inside
a record, but the Haskell implementation had a mistake which prevented this.
Specifically, the Haskell implementation was not normalizing the union type
as the standard specified before attempting to access the constructor, leading
to an unexpected type error.
  • Loading branch information
Gabriella439 committed Nov 22, 2018
1 parent 8bc595b commit bacb824
Show file tree
Hide file tree
Showing 4 changed files with 15 additions and 4 deletions.
8 changes: 4 additions & 4 deletions dhall/src/Dhall/TypeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -791,12 +791,12 @@ typeWithA tpa = loop
Just t' -> return t'
Nothing -> Left (TypeError ctx e (MissingField x t))
Const Type -> do
case r of
(Note _ (Union kts)) ->
case Dhall.Core.normalize r of
Union kts ->
case Dhall.Map.lookup x kts of
Just t' -> return (Pi x t' (Union kts))
Nothing -> Left (TypeError ctx e (MissingField x t))
_ -> Left (TypeError ctx e (CantAccess text r t))
r' -> Left (TypeError ctx e (CantAccess text r' t))
_ -> do
Left (TypeError ctx e (CantAccess text r t))
loop ctx e@(Project r xs ) = do
Expand Down Expand Up @@ -3309,7 +3309,7 @@ prettyTypeMessage (CantAccess lazyText0 expr0 expr1) = ErrorMessages {..}
\ \n\
\" <> txt0 <> "\n\
\ \n\
\... on the following expression which is not a record nor a union: \n\
\... on the following expression which is not a record nor a union type: \n\
\ \n\
\" <> txt1 <> "\n\
\ \n\
Expand Down
3 changes: 3 additions & 0 deletions dhall/tests/TypeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,9 @@ typecheckTests =
, shouldNotTypeCheck
"Hurkens' paradox"
"failure/hurkensParadox"
, should
"allow accessing a constructor from a type stored inside a record"
"success/simple/mixedFieldAccess"
]

preludeExamples :: TestTree
Expand Down
7 changes: 7 additions & 0 deletions dhall/tests/typecheck/success/simple/mixedFieldAccessA.dhall
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
-- Verify that users can use `.` to both access a record field and a union
-- constructor within the same expression. This is a common idiom if a user
-- provides a types package.

let Scope = < Public : {} | Private : {} >
let types = { Scope = Scope }
in types.Scope.Public {=}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
< Private : {} | Public : {} >

0 comments on commit bacb824

Please sign in to comment.