From 8a54e4329de41e4deaa7b6d265420ddb90adb535 Mon Sep 17 00:00:00 2001 From: Nathan Pollart Date: Mon, 8 Jul 2024 16:54:35 +0200 Subject: [PATCH 1/6] adding constructors to subsumption rule --- core/src/typecheck/mod.rs | 68 +++++++++++++++++++-------------------- 1 file changed, 33 insertions(+), 35 deletions(-) diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs index 4c05834295..266746dcc4 100644 --- a/core/src/typecheck/mod.rs +++ b/core/src/typecheck/mod.rs @@ -2409,45 +2409,43 @@ pub fn subsumption( checked: UnifType, ) -> Result<(), UnifError> { let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar); - 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(), - })? + 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(), + })? + } + _ => (), } - _ => (), } + Ok(()) } - Ok(()) + (TypeF::Array(a), TypeF::Array(b)) => subsumption(state, ctxt, *a.clone(), *b.clone()), + (_, _) => checked.unify(inferred_inst, state, &ctxt), } - (_, _) => checked.unify(inferred_inst, state, &ctxt), + } else { + checked.unify(inferred_inst, state, &ctxt) } } From 19d70523e5681d586a66555d28f6316b73b975b7 Mon Sep 17 00:00:00 2001 From: Nathan Pollart Date: Wed, 17 Jul 2024 09:51:30 +0200 Subject: [PATCH 2/6] Add test --- core/tests/integration/inputs/typecheck/array_subtyping.ncl | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 core/tests/integration/inputs/typecheck/array_subtyping.ncl diff --git a/core/tests/integration/inputs/typecheck/array_subtyping.ncl b/core/tests/integration/inputs/typecheck/array_subtyping.ncl new file mode 100644 index 0000000000..f1303d3f0b --- /dev/null +++ b/core/tests/integration/inputs/typecheck/array_subtyping.ncl @@ -0,0 +1,5 @@ +# test.type = 'pass' +let test : Array {foo : Number} = [{foo = 5}] in +let test_func : Array {_ : Number} -> Array {_ : Number} = fun a => a in +let result = test_func test in +true From 296c52e5281df3ef35cdcfbcd34477de8197e25f Mon Sep 17 00:00:00 2001 From: Nathan Pollart Date: Wed, 17 Jul 2024 13:34:26 +0200 Subject: [PATCH 3/6] Modify test --- core/tests/integration/inputs/typecheck/array_subtyping.ncl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/tests/integration/inputs/typecheck/array_subtyping.ncl b/core/tests/integration/inputs/typecheck/array_subtyping.ncl index f1303d3f0b..788bbd0f98 100644 --- a/core/tests/integration/inputs/typecheck/array_subtyping.ncl +++ b/core/tests/integration/inputs/typecheck/array_subtyping.ncl @@ -1,5 +1,5 @@ # test.type = 'pass' let test : Array {foo : Number} = [{foo = 5}] in let test_func : Array {_ : Number} -> Array {_ : Number} = fun a => a in -let result = test_func test in +let result : Array {_ : Number} = test_func test in true From 656b088761e87eac7404b868a22e26d7c602db24 Mon Sep 17 00:00:00 2001 From: Nathan Pollart Date: Wed, 17 Jul 2024 15:30:33 +0200 Subject: [PATCH 4/6] Add dictionary constructor subtyping and adding a test for it --- core/src/typecheck/mod.rs | 3 +++ .../integration/inputs/typecheck/dictionary_subtyping.ncl | 6 ++++++ 2 files changed, 9 insertions(+) create mode 100644 core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs index 114faa0600..ff9855da53 100644 --- a/core/src/typecheck/mod.rs +++ b/core/src/typecheck/mod.rs @@ -2416,6 +2416,9 @@ pub fn subsumption( Ok(()) } (TypeF::Array(a), TypeF::Array(b)) => subsumption(state, ctxt, *a.clone(), *b.clone()), + (TypeF::Dict { type_fields: a, .. }, TypeF::Dict { type_fields: b, .. }) => { + subsumption(state, ctxt.clone(), *a.clone(), *b.clone()) + } (_, _) => checked.unify(inferred_inst, state, &ctxt), } } else { diff --git a/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl b/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl new file mode 100644 index 0000000000..612e7ea82b --- /dev/null +++ b/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl @@ -0,0 +1,6 @@ +# test.type = 'pass' +let test : {_ : {foo : Number}} = {a = {foo = 5}} in +let test_func : {_ : {_ : Number}} -> {_ : {_ : Number}} = fun a => a in +let result : {_ : {_ : Number}} = test_func test in +true + From 9d530969d33eaafcf68976b6179fe64fd817b416 Mon Sep 17 00:00:00 2001 From: Eckaos <71016723+Eckaos@users.noreply.github.com> Date: Thu, 18 Jul 2024 15:00:31 +0200 Subject: [PATCH 5/6] Update core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl Co-authored-by: Yann Hamdaoui --- .../integration/inputs/typecheck/dictionary_subtyping.ncl | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl b/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl index 612e7ea82b..13b89bcd60 100644 --- a/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl +++ b/core/tests/integration/inputs/typecheck/dictionary_subtyping.ncl @@ -1,6 +1,7 @@ # test.type = 'pass' -let test : {_ : {foo : Number}} = {a = {foo = 5}} in -let test_func : {_ : {_ : Number}} -> {_ : {_ : Number}} = fun a => a in -let result : {_ : {_ : Number}} = test_func test in +let test : _ = + let test_func : {_ : {_ : Number}} -> {_ : {_ : Number}} = fun a => a in + test_func {a = {foo = 5}} +in true From c99209ed75d9360fa4aec36ee1e9ddcde728f125 Mon Sep 17 00:00:00 2001 From: Nathan Pollart Date: Fri, 19 Jul 2024 11:13:24 +0200 Subject: [PATCH 6/6] Modify subsumption function to clone less --- core/src/typecheck/mod.rs | 102 ++++++++++++++++++++++++-------------- 1 file changed, 66 insertions(+), 36 deletions(-) diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs index ff9855da53..1d70ac5fff 100644 --- a/core/src/typecheck/mod.rs +++ b/core/src/typecheck/mod.rs @@ -2383,46 +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()), - (TypeF::Dict { type_fields: a, .. }, TypeF::Dict { type_fields: b, .. }) => { - subsumption(state, ctxt.clone(), *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), } }