Merge pull request #92 from FintanH/fintan/typecheck-combine-types

Add typechecking for RecursiveRecordTypeMerge

3 files changed, 115 insertions, 7 deletions

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index bc5322a..aed6ccd 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -83,6 +83,8 @@ pub(crate) enum TypeMessage {
     Sort,
     RecordMismatch(Typed, Typed),
     RecordTypeDuplicateField,
+    RecordTypeMergeRequiresRecordType(Type),
+    RecordTypeMismatch(Type, Type, Type, Type),
     UnionTypeDuplicateField,
     Unimplemented,
 }
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 7d86833..a493b66 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -372,6 +372,38 @@ enum Ret<'a> {
     Expr(ExprF<Thunk, X>),
 }
 
+/// Performs an intersection of two HashMaps.
+///
+/// # Arguments
+///
+/// * `f` - Will compute the final value from the intersecting
+///         key and the values from both maps.
+///
+/// # Description
+///
+/// If the key is present in both maps then the final value for
+/// that key is computed via the `f` function.
+///
+/// The final map will contain the shared keys from the
+/// two input maps with the final computed value from `f`.
+pub(crate) fn intersection_with_key<K, T, U, V>(
+    mut f: impl FnMut(&K, &T, &U) -> V,
+    map1: &HashMap<K, T>,
+    map2: &HashMap<K, U>,
+) -> HashMap<K, V>
+where
+    K: std::hash::Hash + Eq + Clone,
+{
+    let mut kvs = HashMap::new();
+
+    for (k, t) in map1 {
+        // Only insert in the final map if the key exists in both
+        if let Some(u) = map2.get(k) { kvs.insert(k.clone(), f(k, t, u)); }
+    }
+
+    kvs
+}
+
 /// Performs an outer join of two HashMaps.
 ///
 /// # Arguments
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 9bb0e32..11d6c7a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -704,6 +704,79 @@ fn type_last_layer(
 
             combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r))
         }
+        BinOp(RecursiveRecordTypeMerge, l, r) => {
+            // A recursive function to dig down into
+            // records of records when merging.
+            fn combine_record_types(
+                ctx: &TypecheckContext,
+                kts_l: HashMap<Label, TypeThunk>,
+                kts_r: HashMap<Label, TypeThunk>,
+            ) -> Result<Typed, TypeError> {
+                use crate::phase::normalize::intersection_with_key;
+
+                // If the Label exists for both records and Type for the values
+                // are records themselves, then we hit the recursive case.
+                // Otherwise we have a field collision.
+                let combine = |k: &Label, kts_l_inner: &TypeThunk, kts_r_inner: &TypeThunk|
+                    -> Result<Typed, TypeError> {
+                    match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
+                        (Value::RecordType(kvs_l_inner), Value::RecordType(kvs_r_inner)) =>
+                            combine_record_types(ctx, kvs_l_inner, kvs_r_inner),
+                        (_, _) => Err(TypeError::new(ctx, FieldCollision(k.clone()))),
+                    }
+                };
+
+                let kts = intersection_with_key(
+                    |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r),
+                    &kts_l,
+                    &kts_r,
+                );
+
+                Ok(tck_record_type(
+                    ctx,
+                    kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r)))
+                )?
+                .into_type())
+            };
+
+            // Extract the Const of the LHS
+            let k_l = match l.get_type()?.to_value() {
+                Value::Const(k) => k,
+                _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(l.clone()))),
+            };
+
+            // Extract the Const of the RHS
+            let k_r = match r.get_type()?.to_value() {
+                Value::Const(k) => k,
+                _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(r.clone()))),
+            };
+
+            // Const values must match for the Records
+            let k = if k_l == k_r { k_l } else {
+                return Err(mkerr(RecordTypeMismatch(
+                    Typed::from_const(k_l),
+                    Typed::from_const(k_r),
+                    l.clone(),
+                    r.clone(),
+                )))
+            };
+
+            // Extract the LHS record type
+            let kts_x = match l.to_value() {
+                Value::RecordType(kts) => kts,
+                _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(l.clone()))),
+            };
+
+            // Extract the RHS record type
+            let kts_y = match r.to_value() {
+                Value::RecordType(kts) => kts,
+                _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(r.clone()))),
+            };
+
+            // Ensure that the records combine without a type error
+            // and if not output the final Const value.
+            combine_record_types(ctx, kts_x, kts_y).and(Ok(RetTypeOnly(Typed::from_const(k))))
+        }
         BinOp(o @ ListAppend, l, r) => {
             match l.get_type()?.to_value() {
                 Value::AppliedBuiltin(List, _) => {}
@@ -730,6 +803,7 @@ fn type_last_layer(
                 ListAppend => unreachable!(),
                 RightBiasedRecordMerge => unreachable!(),
                 RecursiveRecordMerge => unreachable!(),
+                RecursiveRecordTypeMerge => unreachable!(),
                 _ => return Err(mkerr(Unimplemented)),
             })?;
 
@@ -1236,13 +1310,13 @@ mod spec_tests {
     ti_success!(ti_success_unit_RecursiveRecordMergeTwo, "unit/RecursiveRecordMergeTwo");
     ti_success!(ti_success_unit_RecursiveRecordMergeTwoKinds, "unit/RecursiveRecordMergeTwoKinds");
     ti_success!(ti_success_unit_RecursiveRecordMergeTwoTypes, "unit/RecursiveRecordMergeTwoTypes");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursively, "unit/RecursiveRecordTypeMergeRecursively");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyKinds, "unit/RecursiveRecordTypeMergeRecursivelyKinds");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyTypes, "unit/RecursiveRecordTypeMergeRecursivelyTypes");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRhsEmpty, "unit/RecursiveRecordTypeMergeRhsEmpty");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwo, "unit/RecursiveRecordTypeMergeTwo");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoKinds, "unit/RecursiveRecordTypeMergeTwoKinds");
-    // ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoTypes, "unit/RecursiveRecordTypeMergeTwoTypes");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursively, "unit/RecursiveRecordTypeMergeRecursively");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyKinds, "unit/RecursiveRecordTypeMergeRecursivelyKinds");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyTypes, "unit/RecursiveRecordTypeMergeRecursivelyTypes");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeRhsEmpty, "unit/RecursiveRecordTypeMergeRhsEmpty");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwo, "unit/RecursiveRecordTypeMergeTwo");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoKinds, "unit/RecursiveRecordTypeMergeTwoKinds");
+    ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoTypes, "unit/RecursiveRecordTypeMergeTwoTypes");
     ti_success!(ti_success_unit_RightBiasedRecordMergeRhsEmpty, "unit/RightBiasedRecordMergeRhsEmpty");
     ti_success!(ti_success_unit_RightBiasedRecordMergeTwo, "unit/RightBiasedRecordMergeTwo");
     ti_success!(ti_success_unit_RightBiasedRecordMergeTwoDifferent, "unit/RightBiasedRecordMergeTwoDifferent");