diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs index 114faa0600..1d70ac5fff 100644 --- 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 new file mode 100644 index 0000000000..13b89bcd60 --- /dev/null +++ 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 +