Skip to content

Commit 92a68ef

Browse files
authored
Add support for records of records of types (#700)
... as standardized in dhall-lang/dhall-lang#300 Fixes #692
1 parent 5a0d671 commit 92a68ef

File tree

6 files changed

+8
-11
lines changed

6 files changed

+8
-11
lines changed

dhall/src/Dhall/TypeCheck.hs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -512,10 +512,7 @@ typeWithA tpa = loop
512512
Left (TypeError ctx e (InvalidFieldType k t))
513513
Dhall.Map.traverseWithKey_ process rest
514514

515-
case c of
516-
Type -> return (Const Type)
517-
Kind -> return (Const Sort)
518-
Sort -> return (Const Sort)
515+
return (Const c)
519516
loop ctx e@(RecordLit kvs ) = do
520517
case Dhall.Map.toList kvs of
521518
[] -> return (Record mempty)

dhall/tests/TypeCheck.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,6 @@ typecheckTests =
4747
, should
4848
"allow records of types of mixed kinds"
4949
"success/recordOfTypes"
50-
, should
51-
"allow Boehm-Berarducci-encoded records of types of mixed kinds"
52-
"success/encodedRecordOfTypes"
5350
, should
5451
"allow accessing a type from a record"
5552
"success/accessType"
@@ -62,6 +59,9 @@ typecheckTests =
6259
, should
6360
"allow accessing a constructor from a type stored inside a record"
6461
"success/simple/mixedFieldAccess"
62+
, should
63+
"allow a record of a record of types"
64+
"success/recordOfRecordOfTypes"
6565
]
6666

6767
preludeExamples :: TestTree

dhall/tests/typecheck/success/encodedRecordOfTypesA.dhall

Lines changed: 0 additions & 3 deletions
This file was deleted.

dhall/tests/typecheck/success/encodedRecordOfTypesB.dhall

Lines changed: 0 additions & 1 deletion
This file was deleted.
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
let types = { Scopes = < Public : {} | Private : {} >}
2+
let prelude = { types = types }
3+
in prelude.types.Scopes.Public {=}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
< Public : {} | Private : {} >

0 commit comments

Comments
 (0)