Type inference solves type equations through type unification.
Type unification recursively compares the LHS and RHS types of an
-equation, where either or both types may be or contain type parameters,
+equation, where either or both types may be or contain bound type parameters,
and looks for type arguments for those type parameters such that the LHS
and RHS match (become identical or assignment-compatible, depending on
context).
To that effect, type inference maintains a map of bound type parameters
-to inferred type arguments.
-Initially, the type parameters are known but the map is empty.
+to inferred type arguments; this map is consulted and updated during type unification.
+Initially, the bound type parameters are known but the map is empty.
During type unification, if a new type argument A is inferred,
the respective mapping P ➞ A from type parameter to argument
is added to the map.
@@ -4674,9 +4674,12 @@ no unification step failed, and the map is fully populated.
Unification uses a combination of exact and loose -Unification (see Appendix) depending on whether two types have -to be identical or simply -assignment-compatible: +unification depending on whether two types have to be +identical, +assignment-compatible, or +only structurally equal. +The respective type unification rules +are spelled out in detail in the Appendix.
@@ -8357,3 +8360,148 @@ The following minimal alignment properties are guaranteed:
A struct or array type has size zero if it contains no fields (or elements, respectively) that have a size greater than zero. Two distinct zero-size variables may have the same address in memory.
+ ++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: +
+ +≡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: +
+ +
+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:
+ 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).
+ 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.
+ P and T fails.
+ +Finally, two types that are not bound type parameters unify loosely +(and per the element matching mode) if: +
+ +