Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add a subsumption rule between record types and dictionary types #1977

Merged
merged 5 commits into from
Jul 1, 2024
Merged

Add a subsumption rule between record types and dictionary types #1977

Changes from 3 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
35ff633
Add subsumption rule between Record/Dictionary
Eckaos Jun 25, 2024
abbbe1f
Remove commented code
Eckaos Jun 25, 2024
00a9537
Remove clone in pattern match, replaced fold by a for loop, take into…
Eckaos Jun 26, 2024
c99634e
Update & add comments
Eckaos Jun 27, 2024
bb20fc9
Add integration tests
Eckaos Jun 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 33 additions & 1 deletion core/src/typecheck/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2420,7 +2420,39 @@ 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, .. },
..
},
) => {
Comment on lines +2424 to +2434
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nitpick: in Rust, when you have a match case of the form (that is with only one pattern and a default case)

match foo {
  Pattern => /* .. some code */,
  _ => /* .. default case */,
}

It's more idiomatic to use an if-let. It's exactly the same result but save one level of indentation:

if let Pattern = foo then {
  /* some code */
}
else {
 /* default case */
}

for row in rrows.iter() {
match row {
GenericUnifRecordRowsIteratorItem::Row(a) => {
subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
}
GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } => state
.table
.assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty)),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It could be good to also reproduce the comment that was at the other place where this code was taken from, saying that because we are unifying with a ground type, we don't need to care about level and stuff. Usually assign_rrows is a bit low-level and one shouldn't blindly use it directly. Here we can, but for future readers, it's good to say why.

GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
Err(UnifError::WithConst {
var_kind: VarKindDiscriminant::EnumRows,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
var_kind: VarKindDiscriminant::EnumRows,
var_kind: VarKindDiscriminant::RecordRows,

Copy-paste leftover I guess, but we are unifying record rows, not enum rows 🙂

expected_const_id: id,
inferred: checked.clone(),
})?
}
_ => (),
}
}
Ok(())
}
(_, _) => checked.unify(inferred_inst, state, &ctxt),
}
}

fn check_field<V: TypecheckVisitor>(
Expand Down