Add a subsumption rule between record types and dictionary types

[Eckaos]

Modified the subsumption function to add the subsumption rule between a record type and a dictionary type.

[yannham]

It's on the right track! There's one oversight though around the tail of record types. See the comments.

We probably also want to add a bunch of tests.

[yannham]

Suggested change

	match (inferred_inst.clone(), checked.clone()) {
	match (inferred_inst, checked) {

Those early clones are probably not needed. You might need to put a ref in the pattern matching though, as in:

           UnifType::Concrete {
                typ: TypeF::Record(ref rrows),
                ..
            },

[yannham]

If you don't build anything valuable in a fold, then you can probably get rid of it and just use a good old for loop:

for row in rrows {
    if  let GenericUnifRecordRowsIteratorItem::Row(a) = row {
        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?;
    }
}

Ok(())

[yannham]

Now I'm thinking about something that I haven't thought about before. During type inference, we might have open record types, such as {foo : Number, bar : Number; tail} where the tail at the end means that this value can have more fields that we don't know yet.

If we try to subtype that with a dictionary, as in {foo : Number, bar : Number; ?a} <: {_ : Number}, we can't let the ?a be, because it might very much be instantiated with baz : String at some point. So we need to close the tail of the record.

Interestingly, we can put Dyn in the tail currently (instead of ?a) to say that we don't know anything about it, that those are some fields with Dyn type. I wonder if we could extend the type system to add other types, for example {foo : Number, bar : Number; Number} (or {foo : Number, bar : Number; _ : Number}) to say that the tail is unknown but fields must be numbers. That would probably be a better representation.

Anyhow, I'm just thinking out loud. Let's forget that, for now, I don't think we can do better than closing the tail of the record. In practice, this means that we need to also consider the cases:

• GenericUnifRecordRowsIteratorItem::UnifVar { id, init_level}. In that case we need to unify this var with an empty row. Here is how it's done (note: it's done for enum rows below, but it's exactly the same for record rows; just change any "enum" to "record"):

  nickel/core/src/typecheck/pattern.rs

  Lines 129 to 133 in 9969d9a

  	// We don't need to perform any variable level checks when unifying a free
  	// unification variable with a ground type
  	state
  	.table
  	.assign_erows(id, UnifEnumRows::concrete(EnumRowsF::Empty));

• GenericUnifRecordRowsIteratorItem::TailConstant(id). In this case we must fail. We can raise a WithConst error - in the future we could have a dedicated error for better messages, but for now, that will do.

[yannham]

@Eckaos feel free to re-request a review from me when you think it's ready for a new round!

[Eckaos]

If you think there no need to think about GenericUnifRecordRowsIteratorItem::TailDyn and GenericUnifRecordRowsIteratorItem::TailVar(&'a LocIdent), I think it's ready for a new round ! @yannham

[yannham]

The logic looks good to me.

What's still missing before we can merge:

• Update the documentation of subsumption, which isn't up to date. It says that we don't perform any form of subtyping, but we do, know. We can also include a bit on why we close the tail when it's a unification variable.
• Add tests. You can look at core/tests/integration, the README (EDIT: when I say look at the readme, I mean core/tests/integration/README.md, not the root one), and various inputs (in the inputs directory). It's sufficient to just add new test .ncl test files somewhere in core/tests/integration/inputs/* and they'll automatically be picked up in tests.

We should also update the user manual, but that can probably come in a second step (that is, another pull request).

[yannham]

Suggested change

	var_kind: VarKindDiscriminant::EnumRows,
	var_kind: VarKindDiscriminant::RecordRows,

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

[yannham]

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 */
}

[yannham]

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.

[Eckaos]

@yannham It must be good !

[yannham]

I think more tests would be welcome, in particular when applying a function such as std.record.insert or std.record.get to a record literal (put in a variable). However, I tested those locally and they work, so let's proceed with this PR and add more compelling tests in a second step.

[yannham]

Suggested change

/// In the future, this function might implement a other non-trivial subsumption rule.

[yannham]

Suggested change

	/// a record/dictionary subtyping is the equality
	/// relation).
	/// a record/dictionary subtyping is the equality relation).