Fix toMap type inference (and some merge tweaks)

[philandstuff]

Currently, there is only one type inference rule for toMap e : T, and
it requires that e is of type {}. This adds a second rule which
allows a toMap expression on a nonempty record type to be annotated
with a compatible type.

There is prior art for this in merge t u : T.

---

When I looked at said merge t u : T prior art, I noticed that the requirements
could be relaxed.

Currently, if you want to annotate a merge t u expression, you have to
annotate it with a type that exactly matches the type generated by the
type inference algorithm. This relaxes that requirement so that it only
has to be judgmentally equal to the inferred type.

I also removed the Γ ⊢ t :⇥ { ts… } precondition; the other
precondition, Γ ⊢ merge t u : T, implies that Γ ⊢ t :⇥ { ts… } so we
do not need to state this explicitly. I think it makes the rule
clearer: it's more obvious that "a merge expression can always be
annotated in a compatible way".

---

After opening this PR, I noticed that unannotated toMap e also cannot typecheck.

Currently, there is no base case for type inference of toMap e: the
only rule which can infer a type for an expression of the form toMap e
requires, as precondition, another expression of the form toMap e to
typecheck. This cyclic dependency effectively means that no expression
of the form toMap e (without annotation) can typecheck.

I added a commit which fixes that, by using toMap e : T as the base case instead
of toMap e. This pattern has prior art in the rules for merge t u
and merge t u : T expressions.