spec: update section on type unification for Go 1.21

This leaves the specific unification details out in favor
of a (forthcoming) section in an appendix.

Change-Id: If984c48bdf71c278e1a2759f9a18c51ef58df999
Reviewed-on: https://go-review.googlesource.com/c/go/+/507417
Reviewed-by: Robert Griesemer <[email protected]>
Auto-Submit: Robert Griesemer <[email protected]>
Reviewed-by: Ian Lance Taylor <[email protected]>
TryBot-Bypass: Robert Griesemer <[email protected]>

doc/go_spec.html

@@ -1,6 +1,6 @@
 <!--{
  "Title": "The Go Programming Language Specification",
- "Subtitle": "Version of July 20, 2023",
+ "Subtitle": "Version of July 25, 2023",
  "Path": "/ref/spec"
 }-->
 
@@ -4457,7 +4457,7 @@ <h3 id="Type_inference">Type inference</h3>
 (or <code>S ≡<sub>A</sub> Slice</code> for that matter),
 where the <code><sub>A</sub></code> in <code>≡<sub>A</sub></code>
 indicates that the LHS and RHS types must match per assignability rules
-(see the section on <a href="#Type_unification">type unifcation</a> for
+(see the section on <a href="#Type_unification">type unification</a> for
 details).
 Similarly, the type parameter <code>S</code> must satisfy its constraint
 <code>~[]E</code>. This can be expressed as <code>S ≡<sub>C</sub> ~[]E</code>
@@ -4618,84 +4618,108 @@ <h3 id="Type_inference">Type inference</h3>
 <h4 id="Type_unification">Type unification</h4>
 
 <p>
-<em>
-Note: This section is not up-to-date for Go 1.21.
-</em>
+Type inference solves type equations through <i>type unification</i>.
+Type unification recursively compares the LHS and RHS types of an
+equation, where either or both types may be or contain 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.
+During type unification, if a new type argument <code>A</code> is inferred,
+the respective mapping <code>P ➞ A</code> from type parameter to argument
+is added to the map.
+Conversely, when comparing types, a known type argument
+(a type argument for which a map entry already exists)
+takes the place of its corresponding type parameter.
+As type inference progresses, the map is populated more and more
+until all equations have been considered, or until unification fails.
+Type inference succeeds if no unification step fails and the map has
+an entry for each type parameter.
 </p>
 
-<p>
-Type inference is based on <i>type unification</i>. A single unification step
-applies to a <a href="#Type_inference">substitution map</a> and two types, either
-or both of which may be or contain type parameters. The substitution map tracks
-the known (explicitly provided or already inferred) type arguments: the map
-contains an entry <code>P</code> &RightArrow; <code>A</code> for each type
-parameter <code>P</code> and corresponding known type argument <code>A</code>.
-During unification, known type arguments take the place of their corresponding type
-parameters when comparing types. Unification is the process of finding substitution
-map entries that make the two types equivalent.
+</pre>
+For example, given the type equation with the bound type parameter
+<code>P</code>
 </p>
 
-<p>
-For unification, two types that don't contain any type parameters from the current type
-parameter list are <i>equivalent</i>
-if they are identical, or if they are channel types that are identical ignoring channel
-direction, or if their underlying types are equivalent.
-</p>
+<pre>
+ [10]struct{ elem P, list []P } ≡<sub>A</sub> [10]struct{ elem string; list []string }
+</pre>
 
 <p>
-Unification works by comparing the structure of pairs of types: their structure
-disregarding type parameters must be identical, and types other than type parameters
-must be equivalent.
-A type parameter in one type may match any complete subtype in the other type;
-each successful match causes an entry to be added to the substitution map.
-If the structure differs, or types other than type parameters are not equivalent,
-unification fails.
+type inference starts with an empty map.
+Unification first compares the top-level structure of the LHS and RHS
+types.
+Both are arrays of the same length; they unify if the element types unify.
+Both element types are structs; they unify if they have
+the same number of fields with the same names and if the
+field types unify.
+The type argument for <code>P</code> is not known yet (there is no map entry),
+so unifying <code>P</code> with <code>string</code> adds
+the mapping <code>P ➞ string</code> to the map.
+Unifying the types of the <code>list</code> field requires
+unifying <code>[]P</code> and <code>[]string</code> and
+thus <code>P</code> and <code>string</code>.
+Since the type argument for <code>P</code> is known at this point
+(there is a map entry for <code>P</code>), its type argument
+<code>string</code> takes the place of <code>P</code>.
+And since <code>string</code> is identical to <code>string</code>,
+this unification step succeeds as well.
+Unification of the LHS and RHS of the equation is now finished.
+Type inference succeeds because there is only one type equation,
+no unification step failed, and the map is fully populated.
 </p>
 
-<!--
-TODO(gri) Somewhere we need to describe the process of adding an entry to the
- substitution map: if the entry is already present, the type argument
- values are themselves unified.
--->
-
 <p>
-For example, if <code>T1</code> and <code>T2</code> are type parameters,
-<code>[]map[int]bool</code> can be unified with any of the following:
+Unification uses a combination of <i>exact</i> and <i>loose</i>
+Unification (see Appendix) depending on whether two types have
+to be <a href="#Type_identity">identical</a> or simply
+<a href="#Assignability">assignment-compatible</a>:
 </p>
 
-<pre>
-[]map[int]bool // types are identical
-T1 // adds T1 &RightArrow; []map[int]bool to substitution map
-[]T1 // adds T1 &RightArrow; map[int]bool to substitution map
-[]map[T1]T2 // adds T1 &RightArrow; int and T2 &RightArrow; bool to substitution map
-</pre>
-
 <p>
-On the other hand, <code>[]map[int]bool</code> cannot be unified with any of
+For an equation of the form <code>X ≡<sub>A</sub> Y</code>,
+where <code>X</code> and <code>Y</code> are types involved
+in an assignment (including parameter passing and return statements),
+the top-level type structures may unify loosely but element types
+must unify exactly, matching the rules for assignments.
 </p>
 
-<pre>
-int // int is not a slice
-struct{} // a struct is not a slice
-[]struct{} // a struct is not a map
-[]map[T1]string // map element types don't match
-</pre>
-
 <p>
-As an exception to this general rule, because a <a href="#Type_definitions">defined type</a>
-<code>D</code> and a type literal <code>L</code> are never equivalent,
-unification compares the underlying type of <code>D</code> with <code>L</code> instead.
-For example, given the defined type
+For an equation of the form <code>P ≡<sub>C</sub> C</code>,
+where <code>P</code> is a type parameter and <code>C</code>
+its corresponding constraint, the unification rules are bit
+more complicated:
 </p>
 
-<pre>
-type Vector []float64
-</pre>
+<ul>
+<li>
+ If <code>C</code> has a <a href="#Core_types">core type</a>
+ <code>core(C)</code>
+ and <code>P</code> has a known type argument <code>A</code>,
+ <code>core(C)</code> and <code>A</code> must unify loosely.
+ If <code>P</code> does not have a known type argument
+ and <code>C</code> contains exactly one type term <code>T</code>
+ that is not an underlying (tilde) type, unification adds the
+ mapping <code>P ➞ T</code> to the map.
+</li>
+<li>
+ If <code>C</code> does not have a core type
+ and <code>P</code> has a known type argument <code>A</code>,
+ <code>A</code> must have all methods of <code>C</code>, if any,
+ and corresponding method types must unify exactly.
+</li>
+</ul>
 
 <p>
-and the type literal <code>[]E</code>, unification compares <code>[]float64</code> with
-<code>[]E</code> and adds an entry <code>E</code> &RightArrow; <code>float64</code> to
-the substitution map.
+When solving type equations from type constraints,
+solving one equation may infer additional type arguments,
+which in turn may enable solving other equations that depend
+on those type arguments.
+Type inference repeats type unification as long as new type
+arguments are inferred.
 </p>
 
 <h3 id="Operators">Operators</h3>