Skip to content

Commit

Permalink
constructors === id (#693)
Browse files Browse the repository at this point in the history
  • Loading branch information
FintanH authored and Gabriella439 committed Nov 27, 2018
1 parent 04e2dbf commit 5a0d671
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 21 deletions.
10 changes: 2 additions & 8 deletions dhall/src/Dhall/Core.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1897,14 +1897,8 @@ normalizeWithM ctx e0 = loop (denote e0)
Constructors t -> do
t' <- loop t
case t' of
Union kts -> pure (RecordLit kvs)
where
kvs = Dhall.Map.mapWithKey adapt kts

adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest)
where
rest = Dhall.Map.delete k kts
_ -> pure (Constructors t')
u@(Union _) -> pure u
_ -> pure $ Constructors t'
Field r x -> do
r' <- loop r
case r' of
Expand Down
9 changes: 3 additions & 6 deletions dhall/src/Dhall/TypeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -771,13 +771,10 @@ typeWithA tpa = loop
loop ctx e@(Constructors t ) = do
_ <- loop ctx t

kts <- case Dhall.Core.normalize t of
Union kts -> return kts
t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t'))

let adapt k t_ = Pi k t_ (Union kts)
case Dhall.Core.normalize t of
u@(Union _) -> loop ctx u
t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t'))

return (Record (Dhall.Map.mapWithKey adapt kts))
loop ctx e@(Field r x ) = do
t <- fmap Dhall.Core.normalize (loop ctx r)

Expand Down
2 changes: 1 addition & 1 deletion dhall/tests/import/success/issue553B.dhall
Original file line number Diff line number Diff line change
@@ -1 +1 @@
./issue553A.dhall sha256:6fb582c043889dd5a4c97176f8a58d2633252b5374cb71e288b93bc3757f9643
./issue553A.dhall sha256:e2d014696fb7d773727ae5aa42dc20bbd2447ea82bcb5971ccbb7763906edace
7 changes: 1 addition & 6 deletions dhall/tests/tutorial/unions4B.dhall
Original file line number Diff line number Diff line change
@@ -1,6 +1 @@
{ Empty =
λ(Empty : {}) < Empty = Empty | Person : { age : Natural, name : Text } >
, Person =
λ(Person : { age : Natural, name : Text })
< Person = Person | Empty : {} >
}
< Empty : {} | Person : { name : Text, age : Natural } >

0 comments on commit 5a0d671

Please sign in to comment.