Fix records type inference rules to match implementations. (#3613)

If the context of a record literal is the same shape as the record
literal, but the actual type of one or more fields is not a subtype of
the corresponding field in the context type, and no coercion is
possible, then the implementations do not necessarily issue an
error. They only issue an error if the type mismatch leads to an
assignability error during subsequent analysis.

An example of a circumstance where the type mismatch doesn't lead to
an assignability error is if the context resulted from assignment to a
previously promoted local variable. For example:

    f(Object o) {
      if (o is (int,)) {
        o = ('',); // OK; demotes `o` back to `Object`.
      }
    }

This change adjusts the spec to agree with what was implemented.

accepted/3.0/records/feature-specification.md

@@ -524,7 +524,7 @@ dm : K{n+m}})` then:
       appropriate implicit coercion(s) on `ei`.  Let `Ti` be the type of the
       resulting coerced value (which must be a subtype of `Ri`, possibly
       proper).
-    - Otherwise, it is a static error.
+    - Otherwise, let `Ti` be `Si`.
   - The type of `E` is `(T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})`
 
 If `K` is any other type schema: