Need better exhaustiveness for record-typed type matching.

[lrhn]

Currently record patterns can exhaust a union/sealed type field by exhausting the subtypes.

String s1(({int? value}) v) => switch (v) { // Is exhaustive.
  (value: int _) => "a", // Is a record with structure `(value:)` and field type \<: `int`.
  (value: Null _) => "b",
};

However, if you use an object or type pattern with the actual type of the record, that does not exhaust:

String s2(({int? value}) v) => switch (v) { // NOT exhaustive.
  ({int value}) _ => "a",
  ({Null value}) _ => "b",
};

or

typedef IntValue = ({int value});
typedef NullValue = ({Null value});
String s3(({int? value}) v) => switch (v) { // NOT exhaustive.
  IntValue() => "a",
  NullValue() => "b",
};

The error given is that it doesn't exhaust the type ({int? Value}).

That error makes sense if the type had been a generic class.

class C<T> {}
String s4(C<int?> v) => switch (v) {
  C<int>() => "a",
  C<Null>() => "b",
};

Here a value could have runtime type C<int?>. That is not the case for record types. The runtime type of a record type cannot have a field type that is an empty type.

We let s(int? v) => switch (v) { int _ => "a", Null _ => "b" }; exhaust int? because we know that int? itself is an empty type, which is the same sealed types are abstract. That works for single values, but not for generic type arguments, which can have the empty type. It works for values, not types.
We allow record patterns to do the same thing for record values with a matched value type containing exhaustible types, you can exhaust a field by exhausting the non-empty subtypes of its static type.

But we do not do the same thing for record types, and we should.

(Also has the "funny" consequence that this is not exhaustive:

String s5(({int? value}) v) => switch (v) {
  (value: int _) && ({int value}) _ => "a",
  (value: Null _) && ({Null value}) _ => "b",
};

and yet the analyzer complains that the && ... clauses are unnecessary.)

Possible fix

Not sure exactly where to poke the algorithm.

Maybe in the "Expanding a space" section where the space for a sealed type is expanded into
the set of its subtypes, union types are split into the spaces of their parts, and enums and bool
are split into value spaces.
If we add an item saying;

• If T is a record type with a shape with fields F1..Fn.

  • If T is the empty record type, the space is the space type for the empty record type.
  • Otherwise, let Si be the expanded spaces of the type of Fi for each i in 1..n.
  • The expanded spaces for T contains one space for each different combination of
    one element from each of the Si.
  • For each such combination, (P1,...Pn) in S1×...×Sn,
    the space has the record type with the same shape as T and the type of each P1..Pn
    as the type for the corresponding field F1...Fn.
  • Further if Pi contains any extra restrictions, the space adds those as restrictions
    of the Fi field.

  Example: The type (int?, bool) expands to four spaces. The int? expands to spaces for int and Null.
  The bool expands to two spaces for bool with the constant restrictions true and false respectively.
  The type (int?, bool) expands to four spaces:

  • (int, bool) with constant constraint $2 = true,
  • (int, bool) with constant constraint $2 = false,
  • (Null, bool) with constant constraint $2 = true,
  • (Null, bool) with constant constraint $2 = false,

(I probably missed some details, but "all the cross products of all the field spaces" is the general idea.)

Then record types will be treated as as-expandable as the types they're composed of, and in particular (T,) is just as exhaustible as T.

@munificent @stereotype441

[stereotype441]

Adding @johnniwinther, who is the latest person to touch the exhaustiveness implementation and probably remembers it better than anyone else at this point 😃