Adding dictionary constructor to subsumption rule (#1998)

* adding constructors to subsumption rule * Add test * Modify test * Add dictionary constructor subtyping and adding a test for it * Update core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com> * Modify subsumption function to clone less --------- Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>
tweag · Jul 19, 2024 · e9770b0 · e9770b0
1 parent b934978
commit e9770b0
Show file tree

Hide file tree

Showing 2 changed files with 73 additions and 33 deletions.
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
@@ -2383,43 +2383,76 @@ pub fn subsumption(
     checked: UnifType,
 ) -> Result<(), UnifError> {
     let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar);
-    if let (UnifType::Concrete { typ: typ1, .. }, UnifType::Concrete { typ: typ2, .. }) =
-        (&inferred_inst, &checked)
-    {
-        match (typ1, typ2) {
-            (TypeF::Record(rrows), 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(),
-                            })?
-                        }
-                        _ => (),
+    match (inferred_inst, checked) {
+        (
+            UnifType::Concrete {
+                typ: TypeF::Record(rrows),
+                ..
+            },
+            UnifType::Concrete {
+                typ:
+                    TypeF::Dict {
+                        type_fields,
+                        flavour,
+                    },
+                var_levels_data,
+            },
+        ) => {
+            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) => {
+                        let checked = UnifType::Concrete {
+                            typ: TypeF::Dict {
+                                type_fields: type_fields.clone(),
+                                flavour,
+                            },
+                            var_levels_data,
+                        };
+                        Err(UnifError::WithConst {
+                            var_kind: VarKindDiscriminant::RecordRows,
+                            expected_const_id: id,
+                            inferred: checked,
+                        })?
+                    }
+                    _ => (),
                 }
-                Ok(())
             }
-            (TypeF::Array(a), TypeF::Array(b)) => subsumption(state, ctxt, *a.clone(), *b.clone()),
-            (_, _) => checked.unify(inferred_inst, state, &ctxt),
+            Ok(())
         }
-    } else {
-        checked.unify(inferred_inst, state, &ctxt)
+        (
+            UnifType::Concrete {
+                typ: TypeF::Array(a),
+                ..
+            },
+            UnifType::Concrete {
+                typ: TypeF::Array(b),
+                ..
+            },
+        )
+        | (
+            UnifType::Concrete {
+                typ: TypeF::Dict { type_fields: a, .. },
+                ..
+            },
+            UnifType::Concrete {
+                typ: TypeF::Dict { type_fields: b, .. },
+                ..
+            },
+        ) => subsumption(state, ctxt.clone(), *a, *b),
+        (inferred_inst, checked) => checked.unify(inferred_inst, state, &ctxt),
     }
 }
 

diff --git a/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl b/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl
@@ -0,0 +1,7 @@
+# test.type = 'pass'
+let test : _ = 
+  let test_func : {_ : {_ : Number}} -> {_ : {_ : Number}} = fun a => a in 
+  test_func {a = {foo = 5}}
+in
+true
+