Skip to content

Commit bacb824

Browse files
authored
Fixed mixed field access (#694)
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.
1 parent 8bc595b commit bacb824

File tree

4 files changed

+15
-4
lines changed

4 files changed

+15
-4
lines changed

dhall/src/Dhall/TypeCheck.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -791,12 +791,12 @@ typeWithA tpa = loop
791791
Just t' -> return t'
792792
Nothing -> Left (TypeError ctx e (MissingField x t))
793793
Const Type -> do
794-
case r of
795-
(Note _ (Union kts)) ->
794+
case Dhall.Core.normalize r of
795+
Union kts ->
796796
case Dhall.Map.lookup x kts of
797797
Just t' -> return (Pi x t' (Union kts))
798798
Nothing -> Left (TypeError ctx e (MissingField x t))
799-
_ -> Left (TypeError ctx e (CantAccess text r t))
799+
r' -> Left (TypeError ctx e (CantAccess text r' t))
800800
_ -> do
801801
Left (TypeError ctx e (CantAccess text r t))
802802
loop ctx e@(Project r xs ) = do
@@ -3309,7 +3309,7 @@ prettyTypeMessage (CantAccess lazyText0 expr0 expr1) = ErrorMessages {..}
33093309
\ \n\
33103310
\" <> txt0 <> "\n\
33113311
\ \n\
3312-
\... on the following expression which is not a record nor a union: \n\
3312+
\... on the following expression which is not a record nor a union type: \n\
33133313
\ \n\
33143314
\" <> txt1 <> "\n\
33153315
\ \n\

dhall/tests/TypeCheck.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,9 @@ typecheckTests =
5959
, shouldNotTypeCheck
6060
"Hurkens' paradox"
6161
"failure/hurkensParadox"
62+
, should
63+
"allow accessing a constructor from a type stored inside a record"
64+
"success/simple/mixedFieldAccess"
6265
]
6366

6467
preludeExamples :: TestTree
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
-- Verify that users can use `.` to both access a record field and a union
2+
-- constructor within the same expression. This is a common idiom if a user
3+
-- provides a types package.
4+
5+
let Scope = < Public : {} | Private : {} >
6+
let types = { Scope = Scope }
7+
in types.Scope.Public {=}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
< Private : {} | Public : {} >

0 commit comments

Comments
 (0)