Full pattern matching

[yannham]

Depends on #1819.

This PR finally brings the work done around patterns and ADTs together by making match expressions accept arbitrary patterns on the left hand side of the => sign. This results in both full pattern matching, and the ability to deconstruct ADTs in a type-safe way.

Beside some administrative changes (changing the parsing rule of match, switching to the pattern compilation instead of the current ad-hoc evaluation of match expressions for enum tags, etc.), the bulk of the new work of this PR is the typechecking of general patterns.

Typechecking

For simplicity, I reproduce here what I wrote as a comment inside the typechecker:

We can associate a type to each pattern of each case of the match expression. This the type of a valid argument for this particular pattern. From there, the type of a valid argument for the whole match expression is ideally the union of all the pattern types.

For record types, we don't have any good way to express union: for example, what could be the type of something that is either {x} or {y}? In the Nickel type system, no type can represent that. Thus the match expression should be morally of type Void -> _, which itself doesn't actually exist as a Nickel type, so we reject it. In the case of record types, we just take the intersection of the types, which amounts to unify all pattern types together. While it might fail most of the time (including for {x} and {y}) and throws a type error, it can typecheck interesting expressions when the goal is rather to match on a subfield, for example:

x |> match {
{foo, bar: 'Baz} => <branch1>
{foo, bar: 'Qux} => <branch2>
}

We can definitely find a type for x: {foo: a, bar: [| 'Baz, 'Qux |]}.

For enum types, we can express unions: for example, the union of [|'Foo, 'Bar|] and [|'Bar, 'Baz|] is [|'Foo, 'Bar, 'Baz|]. We can even turn this into a unification problem: "open" the initial row types as [| 'Foo, 'Bar; ?a |] and [|'Bar, 'Baz; ?b |], unify them together, and close the result (unify the tail with an empty row tail). The advantage of this open-unify-close approach is that unification takes care of descending into record types and sub-patterns to perform this operation, and we're back to the same procedure (almost) than for record patterns: unify all pattern types. Although we have additional bookkeeping to perform (closing the right row types at the end of the procedure).

This bookkeeping is performed at least partially by the typecheck::pattern::PatternTypes::pattern_types function.

In consequence, the current approach to typecheck a pattern is:

• in typecheck::pattern, the pattern_types function which elaborates the type of a pattern as well as its variables always elaborates open-ended enum rows when it encounters an enum pattern. It saves the open tail in a vector, together with a pattern path, which localizes the enum pattern inside the wider pattern
• in the typechecker, we unify all the pattern types together, with the open enum rows described above. Then, depending on the presence of a default case, we close either all tails, or we close all but the tails appearing at the top-level of the pattern. Indeed, match { 'Foo => .., 'Bar => .., _ => } : forall rows. [| 'Foo, 'Bar; rows |]. The other paths are currently not leveraged, but we can imagine in the near future having wildcard patterns, in which case we would also let open the tails corresponding to each path where there is a wildcard pattern: typically, we would have match { {foo = 'Foo} => ..., {foo = 'Bar} => ..., {foo = _} => ...} : forall rows . { foo : [| 'Foo, 'Bar; rows |] }

Content

Besides the typechecking implementation, the rest is mostly obvious consequences of generalizing match expressions, as well as bug fixing in pattern compilations and pattern type checking discovered by adding more comprehensive tests.

Follow-up (ADTs + patterns)

• Contracts specified within patterns are currently ignored by the compilation. This shouldn't be the case (and isn't very hard to restore)
• Finally set the right syntax for ADTs (using normal application)
• Decide if we want 'Foo to be matched by 'Foo x or not, adding %unit%: %Unit%.
• Fix the contract generated for enum variants in enum types
• Documentation

[yannham]

The interesting part of this change is here: it was missing a null check which could lead at runtime to %record_remove% complaining that its argument is null on valid (albeit unmatching) patterns. The rest of the diff in this file is just the implementation of this change.

[dpulls]

🎉 All dependencies have been resolved !