From 03bec7dc6ff6bbcdf077753230cee11211aa78ba Mon Sep 17 00:00:00 2001 From: Robert Griesemer Date: Tue, 25 Jul 2023 17:18:20 -0700 Subject: [PATCH] spec: add Appendix with detailed type unification rules Change-Id: I0d4ccbc396c48d565c0cbe93c9558ab330a44d02 Reviewed-on: https://go-review.googlesource.com/c/go/+/513275 Auto-Submit: Robert Griesemer Reviewed-by: Robert Griesemer Reviewed-by: Ian Lance Taylor TryBot-Bypass: Robert Griesemer --- doc/go_spec.html | 162 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 155 insertions(+), 7 deletions(-) diff --git a/doc/go_spec.html b/doc/go_spec.html index ae747d3a63..d1b8bf2a91 100644 --- a/doc/go_spec.html +++ b/doc/go_spec.html @@ -1,6 +1,6 @@ @@ -4620,13 +4620,13 @@ Otherwise, type inference succeeds.

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.

+ +

Appendix

+ +

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. +
      • +
    • + In all other cases unification of P and T fails. +
      • +
    +
    • +
+ +

+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 per the element matching mode, + 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. +
    • +
-- 2.48.1