Add a subsumption rule between record types and dictionary types

core/src/typecheck/mod.rs

@@ -2401,16 +2401,17 @@ fn check<V: TypecheckVisitor>(
 
 /// Change from inference mode to checking mode, and apply a potential subsumption rule.
 ///
-/// Currently, there is no subtyping (until RFC004 is implemented), hence this function performs
+/// Currently, there is record/dictionary subtyping, if we are not in this case we fallback to perform
 /// polymorphic type instantiation with unification variable on the left (on the inferred type),
-/// and then simply performs unification (put differently, the subtyping relation is the equality
+/// and then simply performs unification (put differently, the subtyping relation when it is not
+/// a record/dictionary subtyping is the equality
 /// relation).
 ///
 /// The type instantiation corresponds to the zero-ary case of application in the current
 /// specification (which is based on [A Quick Look at Impredicativity][quick-look], although we
 /// currently don't support impredicative polymorphism).
 ///
-/// In the future, this function might implement a non-trivial subsumption rule.
+/// In the future, this function might implement a other non-trivial subsumption rule.
 ///
 /// [quick-look]: https://www.microsoft.com/en-us/research/uploads/prod/2020/01/quick-look-icfp20-fixed.pdf
 pub fn subsumption(
@@ -2420,7 +2421,46 @@ pub fn subsumption(
     checked: UnifType,
 ) -> Result<(), UnifError> {
     let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar);
-    checked.unify(inferred_inst, state, &ctxt)
+    match (&inferred_inst, &checked) {
+        (
+            UnifType::Concrete {
+                typ: TypeF::Record(rrows),
+                ..
+            },
+            UnifType::Concrete {
+                typ: TypeF::Dict { type_fields, .. },
+                ..
+            },
+        ) => {
+            for row in rrows.iter() {
+                match row {
+                    GenericUnifRecordRowsIteratorItem::Row(a) => {
+                        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
+                    }
+                    GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
+                    // We don't need to perform any variable level checks when unifying a free
+                    // unification variable with a ground type
+                    // We close the tail because there is no garanty that
+                    // { a : Number, b : Number, _ : a?} <= { _ : Number}
+                    {
+                        state
+                            .table
+                            .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
+                    }
+                    GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
+                        Err(UnifError::WithConst {
+                            var_kind: VarKindDiscriminant::RecordRows,
+                            expected_const_id: id,
+                            inferred: checked.clone(),
+                        })?
+                    }
+                    _ => (),
+                }
+            }
+            Ok(())
+        }
+        (_, _) => checked.unify(inferred_inst, state, &ctxt),
+    }
 }
 
 fn check_field<V: TypecheckVisitor>(

core/tests/integration/inputs/typecheck/mismatch_record_dictionary_subtyping.ncl

@@ -0,0 +1,10 @@
+# test.type = 'error'
+# eval = 'typecheck'
+#
+# [test.metadata]
+# error = 'TypecheckError::TypeMismatch'
+# [test.metadata.expectation]
+# expected = 'Number'
+# inferred = 'String'
+let test : {foo : Number, bar : String} = {foo = 5, bar = "test"} in
+(std.record.insert "baz" 5 test) : {_ : Number}

core/tests/integration/inputs/typecheck/record_dictionary_subtyping.ncl

@@ -0,0 +1,6 @@
+# test.type = 'pass'
+let test1 : {foo : Number} = {foo = 5} in
+let _ = (std.record.insert "bar" 5 test1) : {_ : Number} in
+let test2 : {foo : Number, bar : Number} = {foo = 5, bar = 5} in
+let _ = (std.record.insert "baz" 5 test2) : {_ : Number} in
+true