Keep type information after RecursiveRecordTypeMerge

3 files changed, 26 insertions, 90 deletions

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 0c4e185..28dc0f6 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -452,53 +452,20 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-/// 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
-}
-
-pub(crate) fn merge_maps<K, V>(
+pub(crate) fn merge_maps<K, V, F, Err>(
     map1: &HashMap<K, V>,
     map2: &HashMap<K, V>,
-    mut f: impl FnMut(&V, &V) -> V,
-) -> HashMap<K, V>
+    mut f: F,
+) -> Result<HashMap<K, V>, Err>
 where
+    F: FnMut(&V, &V) -> Result<V, Err>,
     K: std::hash::Hash + Eq + Clone,
     V: Clone,
 {
     let mut kvs = HashMap::new();
     for (x, v2) in map2 {
         let newv = if let Some(v1) = map1.get(x) {
-            f(v1, v2)
+            f(v1, v2)?
         } else {
             v2.clone()
         };
@@ -508,7 +475,7 @@ where
         // Insert only if key not already present
         kvs.entry(x.clone()).or_insert_with(|| v1.clone());
     }
-    kvs
+    Ok(kvs)
 }
 
 fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
@@ -518,8 +485,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         RightBiasedRecordMerge, TextAppend,
     };
     use ValueF::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
-        TextLit,
+        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, TextLit,
     };
     let x_borrow = x.as_whnf();
     let y_borrow = y.as_whnf();
@@ -604,31 +570,16 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
-                    RecursiveRecordMerge,
-                    v1.clone(),
-                    v2.clone(),
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |v1, v2| {
+                Ok(Value::from_valuef_untyped(ValueF::PartialExpr(
+                    ExprF::BinOp(RecursiveRecordMerge, v1.clone(), v2.clone()),
                 )))
-            });
+            })?;
             Ret::ValueF(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
-        }
-        (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
-                    RecursiveRecordTypeMerge,
-                    v1.clone(),
-                    v2.clone(),
-                )))
-            });
-            Ret::ValueF(RecordType(kvs))
+        (RecursiveRecordTypeMerge, _, _) => {
+            unreachable!("This case should have been handled in typecheck")
         }
 
         (Equivalence, _, _) => {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index abe05a3..363d733 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -567,7 +567,9 @@ fn type_last_layer(
 
             // Union the two records, prefering
             // the values found in the RHS.
-            let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone());
+            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, r_t| {
+                Ok(r_t.clone())
+            })?;
 
             // Construct the final record type from the union
             RetTypeOnly(tck_record_type(
@@ -584,25 +586,7 @@ fn type_last_layer(
             ),
         )?),
         BinOp(RecursiveRecordTypeMerge, l, r) => {
-            use crate::phase::normalize::intersection_with_key;
-
-            // Extract the Const of the LHS
-            let k_l = match l.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
-                }
-            };
-
-            // Extract the Const of the RHS
-            let k_r = match r.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
-                }
-            };
-
-            let k = max(k_l, k_r);
+            use crate::phase::normalize::merge_maps;
 
             // Extract the LHS record type
             let borrow_l = l.as_whnf();
@@ -623,9 +607,11 @@ fn type_last_layer(
             };
 
             // Ensure that the records combine without a type error
-            let kts = intersection_with_key(
+            let kts = merge_maps(
+                kts_x,
+                kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
-                |_: &Label, l: &Value, r: &Value| {
+                |l: &Value, r: &Value| {
                     type_last_layer(
                         ctx,
                         ExprF::BinOp(
@@ -635,12 +621,9 @@ fn type_last_layer(
                         ),
                     )
                 },
-                kts_x,
-                kts_y,
-            );
-            tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+            )?;
 
-            RetTypeOnly(Value::from_const(k))
+            RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
diff --git a/tests_buffer b/tests_buffer
index 15dc9c5..511ea49 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -32,7 +32,9 @@ variables across import boundaries
 typecheck:
 something that involves destructuring a recordtype after merge
 add some of the more complicated Prelude tests back, like List/enumerate
-failure on old-style optional literal
+success/
+    regression/
+        RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } }
 failure/
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >