Nicer inferred and displayed record types

[pchiusano]

Similar to what we do for ability variables, this PR generalizes function signatures to include slack variables in record types, while eliding them from display when they are in strictly negative position. The goal here is to:

1. Make the nicest syntax the thing you typically want, and nudge people away from accidentally making functions needlessly strict in what fields are allowed.
2. Avoid polluting displayed type signatures with slack variables.
3. Avoid users needing to make pointless decisions about whether a function should allow extra fields or not (since by default, allowing extra fields for record types in negative position is almost always what you want)

For instance, given:

foo : { x : Nat } -> Nat
foo rec = rec@x + 100

The typechecker treats this as:

foo : { x : Nat | rest } -> Nat

... allowing it to be called with foo {x : 10, blah : "unused" }.

But since this | rest is in strictly negative position and appears only once in the type, it is hidden.

The ... syntax is gone, it isn't necessary anymore.

I futzed with various ways of doing this before settling on this combination. I am not 100% sold this is the right balance, but it's easy to tweak the approach later, so I plan on merging and we can see how it goes.

One thing I rejected, after talking it over with @ChrisPenner - general subtyping of records, where a record is a subtype of another if it has a superset of the fields. That has some bad properties, like that {x : 10} === {x : 10, y: 11} and if you put differently typed records in a list it just silently infers their least upper bound of common fields, which could even be the empty record type!

Tested by transcripts.