Add support for accessing/projecting record type fields

dhall/dhall.cabal

@@ -381,6 +381,7 @@ Library
         Dhall.Syntax.Instances.Functor
         Dhall.Syntax.Instances.Lift
         Dhall.Syntax.Instances.Monad
+        Dhall.Syntax.Instances.Monoid
         Dhall.Syntax.Instances.NFData
         Dhall.Syntax.Instances.Ord
         Dhall.Syntax.Instances.Pretty

dhall/src/Dhall/Eval.hs

@@ -367,6 +367,9 @@ vField t0 k = go t0
             Just (Just _) -> VPrim $ \ ~u -> VInject m k (Just u)
             Just Nothing  -> VInject m k Nothing
             _             -> error errorMsg
+        VRecord m
+            | Just v <- Map.lookup k m -> v
+            | otherwise -> error errorMsg
         VRecordLit m
             | Just v <- Map.lookup k m -> v
             | otherwise -> error errorMsg
@@ -414,6 +417,9 @@ vProjectByFields env t ks =
             VRecordLit kvs ->
                 let kvs' = Map.restrictKeys kvs (Dhall.Set.toSet ks)
                 in  VRecordLit kvs'
+            VRecord kTs ->
+                let kTs' = Map.restrictKeys kTs (Dhall.Set.toSet ks)
+                in  VRecord kTs'
             VProject t' _ ->
                 vProjectByFields env t' ks
             VPrefer l (VRecordLit kvs) ->

dhall/src/Dhall/Normalize.hs

@@ -664,6 +664,11 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
                       case Dhall.Map.lookup x kvs of
                           Just v  -> pure $ recordFieldValue v
                           Nothing -> Field <$> (RecordLit <$> traverse (Syntax.recordFieldExprs loop) kvs) <*> pure k
+                  Record kTs ->
+                      case Dhall.Map.lookup x kTs of
+                          Just _T -> pure $ recordFieldValue _T
+                          Nothing -> Field <$> (Record <$> traverse (Syntax.recordFieldExprs loop) kTs) <*> pure k
+
                   Project r_ _ -> loop (Field r_ k)
                   Prefer cs _ (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
                       Just v -> pure (Field (Prefer cs PreferFromSource (singletonRecordLit v) r_) k)
@@ -684,6 +689,8 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
               case x' of
                   RecordLit kvs ->
                       pure (RecordLit (Dhall.Map.restrictKeys kvs fieldsSet))
+                  Record kTs ->
+                      pure (Record (Dhall.Map.restrictKeys kTs fieldsSet))
                   Project y _ ->
                       loop (Project y (Left fields))
                   Prefer cs _ l (RecordLit rKvs) -> do
@@ -980,6 +987,7 @@ isNormalized e0 = loop (Syntax.denote e0)
           _ -> True
       Field r (FieldSelection Nothing k Nothing) -> case r of
           RecordLit _ -> False
+          Record    _ -> False
           Project _ _ -> False
           Prefer _ _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
           Prefer _ _ _ (RecordLit _) -> False
@@ -991,6 +999,7 @@ isNormalized e0 = loop (Syntax.denote e0)
           case p of
               Left s -> case r of
                   RecordLit _ -> False
+                  Record    _ -> False
                   Project _ _ -> False
                   Prefer _ _ _ (RecordLit _) -> False
                   _ -> not (null s) && Data.Set.toList (Data.Set.fromList s) == s

dhall/src/Dhall/Syntax.hs

@@ -19,6 +19,7 @@ import                Dhall.Syntax.Instances.Foldable    as Export ()
 import                Dhall.Syntax.Instances.Functor     as Export ()
 import                Dhall.Syntax.Instances.Lift        as Export ()
 import                Dhall.Syntax.Instances.Monad       as Export ()
+import                Dhall.Syntax.Instances.Monoid      as Export ()
 import                Dhall.Syntax.Instances.NFData      as Export ()
 import                Dhall.Syntax.Instances.Ord         as Export ()
 import                Dhall.Syntax.Instances.Pretty      as Export

dhall/src/Dhall/Syntax/Instances/Monoid.hs

@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Dhall.Syntax.Instances.Monoid () where
+
+import Dhall.Syntax.Const (Const(..))
+import Dhall.Syntax.Instances.Ord ()
+
+instance Semigroup Const where
+    (<>) = max
+
+instance Monoid Const where
+    mempty = Type

dhall/src/Dhall/TypeCheck.hs

@@ -1158,22 +1158,26 @@ infer typer = loop
                     case Dhall.Map.lookup x xTs' of
                         Just _T' -> return _T'
                         Nothing  -> die (MissingField x _E'')
-                _ -> do
-                    let e' = eval values e
-
-                    let e'' = quote names e'
-
-                    case e' of
-                        VUnion xTs' ->
-                            case Dhall.Map.lookup x xTs' of
-                                Just (Just _T') -> return (VHPi x _T' (\_ -> e'))
-                                Just  Nothing   -> return e'
-                                Nothing         -> die (MissingConstructor x e)
-
-                        _ -> do
-                            let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x)
-
-                            die (CantAccess text e'' _E'')
+                _   | VRecord xTs' <- eval values e ->
+                        case Dhall.Map.lookup x xTs' of
+                            Just _T' -> loop ctx (quote names _T')
+                            Nothing  -> die (MissingField x _E'')
+                    | otherwise -> do
+                        let e' = eval values e
+
+                        let e'' = quote names e'
+
+                        case e' of
+                            VUnion xTs' ->
+                                case Dhall.Map.lookup x xTs' of
+                                    Just (Just _T') -> return (VHPi x _T' (\_ -> e'))
+                                    Just  Nothing   -> return e'
+                                    Nothing         -> die (MissingConstructor x e)
+
+                            _ -> do
+                                let text = Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabel x)
+
+                                die (CantAccess text e'' _E'')
         Project e (Left xs) -> do
             case duplicateElement xs of
                 Just x -> do
@@ -1185,6 +1189,9 @@ infer typer = loop
 
             let _E'' = quote names _E'
 
+            let text =
+                    Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs)
+
             case _E' of
                 VRecord xTs' -> do
                     let process x =
@@ -1196,11 +1203,25 @@ infer typer = loop
 
                     fmap adapt (traverse process xs)
 
-                _ -> do
-                    let text =
-                            Dhall.Pretty.Internal.docToStrictText (Dhall.Pretty.Internal.prettyLabels xs)
+                _   | VRecord xTs' <- eval values e -> do
+                        let process x =
+                                case Dhall.Map.lookup x xTs' of
+                                    Just _T' -> do
+                                        _T'' <- loop ctx (quote names _T')
+
+                                        case _T'' of
+                                            VConst c -> pure c
+                                            _        -> die (CantProject text e _E'')
+
+                                    Nothing -> do
+                                        die (MissingField x _E'')
+
+                        cs <- traverse process xs
+
+                        return (VConst (mconcat cs))
 
-                    die (CantProject text e _E'')
+                    | otherwise -> do
+                        die (CantProject text e _E'')
 
         Project e (Right s) -> do
             _E' <- loop ctx e