Merge pull request #2013 from xushiwei/q

mini spec: Type unification rules

doc/spec-mini.md

@@ -2006,4 +2006,39 @@ A struct or array type has size zero if it contains no fields (or elements, resp
 
 ## Appendix
 
+### Language versions
+
 TODO
+
+### Type unification rules
+
+The type unification rules describe if and how two types unify. The precise details are relevant for Go+ implementations, affect the specifics of error messages (such as whether a compiler reports a type inference or other error), and may explain why type inference fails in unusual code situations. But by and large these rules can be ignored when writing Go code: type inference is designed to mostly "work as expected", and the unification rules are fine-tuned accordingly.
+
+Type unification is controlled by a matching mode, which may be `exact` or `loose`. As unification recursively descends a composite type structure, the matching mode used for elements of the type, the element matching mode, remains the same as the matching mode except when two types are unified for [assignability]() (≡A): in this case, the matching mode is loose at the top level but then changes to exact for element types, reflecting the fact that types don't have to be identical to be assignable.
+
+Two types that are not bound type parameters unify exactly if any of following conditions is true:
+
+* Both types are [identical]().
+* Both types have identical structure and their element types unify exactly.
+* Exactly one type is an [unbound]() type parameter with a [core type](), and that core type unifies with the other type per the unification rules for ≡A (loose unification at the top level and exact unification for element types).
+
+If both types are bound type parameters, they unify per the given matching modes if:
+
+* Both type parameters are identical.
+* At most one of the type parameters has a known type argument. In this case, the type parameters are `joined`: they both stand for the same type argument. If neither type parameter has a known type argument yet, a future type argument inferred for one the type parameters is simultaneously inferred for both of them.
+* Both type parameters have a known type argument and the type arguments unify per the given matching modes.
+
+A single bound type parameter P and another type T unify per the given matching modes if:
+
+* P doesn't have a known type argument. In this case, T is inferred as the type argument for P.
+* P does have a known type argument A, A and T unify per the given matching modes, and one of the following conditions is true:
+  * Both A and T are interface types: In this case, if both A and T are also [defined]() types, they must be [identical](). Otherwise, if neither of them is a defined type, they must have the same number of methods (unification of A and T already established that the methods match).
+  * Neither A nor T are interface types: In this case, if T is a defined type, T replaces A as the inferred type argument for P.
+
+Finally, two types that are not bound type parameters unify loosely (and per the element matching mode) if:
+
+* Both types unify exactly.
+* One type is a [defined type](), the other type is a type literal, but not an interface, and their underlying types unify per the element matching mode.
+* Both types are interfaces (but not type parameters) with identical [type terms](), both or neither embed the predeclared type [comparable](), corresponding method types unify exactly, and the method set of one of the interfaces is a subset of the method set of the other interface.
+* Only one type is an interface (but not a type parameter), corresponding methods of the two types unify per the element matching mode, and the method set of the interface is a subset of the method set of the other type.
+* Both types have the same structure and their element types unify per the element matching mode.