cmd/compile/internal/types2: make type inference independent of function argument order

[mdempsky]

In the test case at https://go2goplay.golang.org/p/gEl3-egETB2, F(i, j) is accepted, but F(j, i) is not. Both of F's value parameters have identical type, so the behavior here should be consistent (either both accepted, or both rejected).

Based on my understanding from Robert (that type inference requires arguments to have identical type to the parameter, not mere assignability to it), I suspect the correct, consistent behavior is for both to be rejected.

Some more tests at https://go2goplay.golang.org/p/aVaXxBbK1j5. I plan to write a program to exhaustively generate test cases.

(My motivation for looking into this was adding type parameter support to rf, for type-polymorphic rewriting rules: rsc/rf#6)

/cc @griesemer @ianlancetaylor

[ianlancetaylor]

I don't see why the type parameters have identical type. One is type I. The other is type interface{ Equal(I) bool }. A named type is not identical to an unnamed type. What am I missing?

[mdempsky]

The calls' value arguments i and j have different types; but F's value parameters are a and b, which are both declared as type T. (There's only one type parameter in the simplified test case: T.)

[griesemer]

I agree that either both of these calls of F should succeed or fail as the only difference is the order of the arguments.

Unfortunately, we currently have an asymmetry in the unification algorithm: If one of the involved types is a defined type (here I) and the other one is not (here interface{ Equal(I) bool }), w/o any further steps, unification would fail right away (the two types are different). In cases like these we take the underlying type of the named type I, so interface{ Equal(I) bool } and try to unify that with the type of j which is also interface{ Equal(I) bool } and everything is fine.

Since we started with I (first argument), the inferred type is I. As a result we get the invocation F[I](i, j); I which satisfies the constraint, and both i and j can be assigned to a I parameter.

In the 2nd case we start with interface{ Equal(I) bool } (type of j). We use the same rule as above, unification succeeds, but the inferred type is now interface{ Equal(I) bool }. As a result we get the invocation F[interface{ Equal(I) bool}](j, i). This type does not satisfy the constraint because the constraint's Equal method is (after substitution) Equal(interface{Equal(I) bool}) bool which is not equal to Equal(I) bool, and instantiation fails.

In summary, unification produces the following calls:

F[I](i, j)
F[interface{ Equal(I) bool}](j, i)

It seems reasonable to postulate that if we enter unification with an underlying type of a named type to make it succeed, the inferred type should be the underlying type (here interface{Equal(I) bool}). We probably should make that change to make the algorithm symmetric.

But then both calls in this example would fail (because instantiation fails).

Alternatively, maybe the interface I and interface{Equal(I) bool} should be considered identical recursively, which is essentially #8082. Or maybe #8082 but only for unification purposes.

This problem only occurs with interfaces because those are the only types for which we can provide methods in the type literal; for all other types, we need a defined type to attach methods.

There may be other work-arounds and changes to the inference algorithm that make this work "as expected". But is does seems accepting #8082 would solve this problem for interfaces.

[gopherbot]

Change https://golang.org/cl/276692 mentions this issue: [dev.typeparams] go/types: import unify.go and infer.go from dev.go2go

[griesemer]

Slightly simpler, analogous case:

package p

func f[T ~func(T)](a, b T) {}

type F func(F)

func _() {
	var i F
	var j func(F)

	f(i, j)
	f(j, i)
}

[gopherbot]

Change https://golang.org/cl/377894 mentions this issue: go/types, types2: make function type inference argument-order independent

[griesemer]

The above CL addresses this issue, but it also adds complexity to the description of type inference. Per discussion w/ @ianlancetaylor , this is not necessarily a "bug": the error can be explained given the existing spec rules (in progress). It is also an extremely esoteric case that seems unlikely to occur frequently in practice.

Decision is to postpone any action on this for the time being. We can keep the code in place as it is guarded by a flag. If we decide to act upon this, it will be trivial to enable this specific fix.