unify Combine and CombineTypes

dhall/src/Dhall/Eval.hs

@@ -318,6 +318,12 @@ vCombine mk t u =
             t'
         (VRecordLit m, VRecordLit m') ->
             VRecordLit (Map.unionWith (vCombine Nothing) m m')
+        (VRecord m, u') | null m ->
+            u'
+        (t', VRecord m) | null m ->
+            t'
+        (VRecord m, VRecord m') ->
+            VRecord (Map.unionWith (vCombine Nothing) m m')
         (t', u') ->
             VCombine mk t' u'
 

dhall/src/Dhall/Normalize.hs

@@ -548,15 +548,20 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
               kts' = traverse (traverse loop) kts
           Combine cs mk x y -> decide <$> loop x <*> loop y
             where
+              mergeFields (RecordField _ expr _ _) (RecordField _ expr' _ _) =
+                Syntax.makeRecordField $ decide expr expr'
               decide (RecordLit m) r | Data.Foldable.null m =
                   r
               decide l (RecordLit n) | Data.Foldable.null n =
                   l
               decide (RecordLit m) (RecordLit n) =
-                  RecordLit (Dhall.Map.unionWith f m n)
-                where
-                  f (RecordField _ expr _ _) (RecordField _ expr' _ _) =
-                    Syntax.makeRecordField $ decide expr expr'
+                  RecordLit (Dhall.Map.unionWith mergeFields m n)
+              decide (Record m) r | Data.Foldable.null m =
+                  r
+              decide l (Record n) | Data.Foldable.null n =
+                  l
+              decide (Record m) (Record n) =
+                  Record (Dhall.Map.unionWith mergeFields m n)
               decide l r =
                   Combine cs mk l r
           CombineTypes cs x y -> decide <$> loop x <*> loop y
@@ -949,6 +954,9 @@ isNormalized e0 = loop (Syntax.denote e0)
           decide (RecordLit m) _ | Data.Foldable.null m = False
           decide _ (RecordLit n) | Data.Foldable.null n = False
           decide (RecordLit _) (RecordLit _) = False
+          decide (Record m) _ | Data.Foldable.null m = False
+          decide _ (Record n) | Data.Foldable.null n = False
+          decide (Record _) (Record _) = False
           decide  _ _ = True
       CombineTypes _ x y -> loop x && loop y && decide x y
         where

dhall/src/Dhall/TypeCheck.hs

@@ -801,15 +801,24 @@
         Combine _ mk l r -> do
             _L' <- loop ctx l
 
-            let l'' = quote names (eval values l)
+            let l' = eval values l
+
+            let l'' = quote names l'
 
             _R' <- loop ctx r
 
-            let r'' = quote names (eval values r)
+            let r' = eval values r
 
-            xLs' <- case _L' of
-                VRecord xLs' ->
-                    return xLs'
+            let r'' = quote names r'
+
+            -- The `Combine` operator should now work on record terms and also on record types.
+            -- If both sides are record terms, we set leftTypeOrRecord and rightTypeOrRecord to (Left record_fields).
+            -- If both sides are record types, we set both of them to (Right (Type, record_fields)).
+            -- Then we match the pair (leftTypeOrRecord, rightTypeOrRecord) to make sure we catch errors.
+            leftTypeOrRecord <- case (_L', l') of
+                (VRecord xLs', _) -> return (Left xLs')
+
+                (VConst cL, VRecord xLs') -> return (Right (cL, xLs'))
 
                 _ -> do
                     let _L'' = quote names _L'
@@ -818,9 +827,12 @@
                         Nothing -> die (MustCombineARecord '∧' l'' _L'')
                         Just t  -> die (InvalidDuplicateField t l _L'')
 
-            xRs' <- case _R' of
-                VRecord xRs' ->
-                    return xRs'
+            -- Make sure both are on the Left (both record values) or on the Right (both record types).
+            rightTypeOrRecord  <- case (leftTypeOrRecord, _R', r') of
+                (Left _, VRecord xRs', _) ->
+                    return (Left xRs')
+
+                (Right _, VConst cR, VRecord xRs') -> return (Right (cR, xRs'))
 
                 _ -> do
                     let _R'' = quote names _R'
@@ -845,7 +857,26 @@
 
                     return (VRecord xTs)
 
-            combineTypes [] xLs' xRs'
+            let combineTypesCheck xs xLs₀' xRs₀' = do
+                    let combine x (VRecord xLs₁') (VRecord xRs₁') =
+                            combineTypesCheck (x : xs) xLs₁' xRs₁'
+
+                        combine x _ _ =
+                            die (FieldTypeCollision (NonEmpty.reverse (x :| xs)))
+
+                    let mL = Dhall.Map.toMap xLs₀'
+                    let mR = Dhall.Map.toMap xRs₀'
+
+                    Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR)
+
+            case (leftTypeOrRecord, rightTypeOrRecord) of
+                (Left xLs', Left xRs') -> do
+                                combineTypes [] xLs' xRs'
+                (Right (cL, xLs'), Right (cR, xRs')) -> do
+                                                         let c = max cL cR
+                                                         combineTypesCheck [] xLs' xRs'
+                                                         return (VConst c)
+
 
         CombineTypes _ l r -> do
             _L' <- loop ctx l