Fix toMap type inference (and some merge tweaks) (#671)

* Allow `toMap e : T` where `e` is a nonempty record

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`.

* Relax `merge t u` annotation requirements

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".

* add test for new toMap inference rule

* Ensure `toMap e` can 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.

This commit 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.

standard/type-inference.md

@@ -763,18 +763,22 @@ The `toMap` operator can be applied only to a record value, and every field
 of the record must have the same type, which in turn must be a `Type`.
 
 
-    Γ ⊢ e :⇥ { x : T₀, xs… }
-    Γ ⊢ toMap { xs… } :⇥ List { mapKey : Text, mapValue : T₁ }
-    T₀ ≡ T₁
-    ──────────────────────────────────────────────────────────
-    Γ ⊢ toMap e : List { mapKey : Text, mapValue : T₀ }
+    Γ ⊢ e :⇥ { x : T, xs… }
+    Γ ⊢ ( toMap { xs… } : List { mapKey : Text, mapValue : T } ) :⇥ List { mapKey : Text, mapValue : T }
+    ────────────────────────────────────────────────────────────────────────────────────────────────────
+    Γ ⊢ toMap e : List { mapKey : Text, mapValue : T }
 
 
     Γ ⊢ e :⇥ {}   Γ ⊢ T₀ :⇥ Type   T₀ ⇥ List { mapKey : Text, mapValue : T₁ }
     ─────────────────────────────────────────────────────────────────────────
     Γ ⊢ ( toMap e : T₀ ) : List { mapKey : Text, mapValue : T₁ }
 
 
+    Γ ⊢ toMap e : T₀   T₀ ≡ T₁
+    ──────────────────────────
+    Γ ⊢ ( toMap e : T₁ ) : T₁
+
+
 ## Unions
 
 Union types are "anonymous", meaning that they are uniquely defined by the names
@@ -859,9 +863,9 @@ between the fields of the handler record and the alternatives of the union:
     Γ ⊢ (merge t u : T) : T
 
 
-    Γ ⊢ t :⇥ { ts… }   Γ ⊢ merge t u : T
-    ────────────────────────────────────  ; `ts` non-empty
-    Γ ⊢ (merge t u : T) : T
+    Γ ⊢ merge t u : T₀   T₀ ≡ T₁
+    ────────────────────────────
+    Γ ⊢ (merge t u : T₁) : T₁
 
 
     Γ ⊢ t :⇥ { y : ∀(x : A₀) → T₀, ts… }

tests/type-inference/success/unit/ToMapAnnotatedA.dhall

@@ -0,0 +1 @@
+toMap { foo = 1, bar = 4, baz = 9 } : List { mapKey : Text, mapValue : Natural }

tests/type-inference/success/unit/ToMapAnnotatedB.dhall

@@ -0,0 +1 @@
+List { mapKey : Text, mapValue : Natural }