Fix toMap type inference (and some merge tweaks)

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 }