go/types, types2: explore "interleaved" type inference by combining function argument type inference with constraint type inference

[griesemer]

This is extracted from an old comment by @rsc on the behavior of type inference as described in the spec (and as currently implemented). Given the following code:

// user-defined implementation of append
func Append[S ~[]T, T any](s S, x ...T) S { /* implementation of append */ return s }

func _() {
        type MyPtr *int
        var x []MyPtr
        _ = append(x, new(int))  // built-in append: ok
        _ = Append(x, new(int))  // user-defined append, not ok: []MyPtr does not implement ~[]*int
}

Type inference passes in separate phases of function argument type inference and constraint type inference: In the first phase (function arguments) the following matches are established: S -> []MyPtr and T -> *int. At this point we have all type arguments and we're done. After instantiation of Append we have the non-generic function:

func Append(s []*int, x ...*int) []MyPtr

and now []MyPtr doesn't implement ~[]*int (MyPtr is not identical to *int).

Per the comment by @rsc, this could work if function argument type inference and constraint type inference were interleaved (and inference using typed function arguments would stop as soon as all type arguments are known).

In such an interleaved world, as soon as we have established the mapping S -> []MyPtr constraint type inference would match []MyPtr against []T and establish the mapping T -> MyPtr. At this point all type arguments are inferred and upon instantiation of Append we would get:

func Append(s []MyPtr, x ...MyPtr) []MyPtr

Calling this version of Append would work because the unnamed type *int can be assigned to the named type MyPtr.

It might even be possible to apply constraint type inference to constraints that don't have a single specific type: As soon as we have a type argument inferred from a function argument it could be matched against every specific type in the constraint.

The interleaved type inference behavior is more powerful in this specific case (and thus we could change this in a backward-compatible way).

@rsc, @ianlancetaylor, @findleyr for comments.

[ianlancetaylor]

I don't think we should do anything here for Go 1.18 (except maybe try to get a better error message, that error message is pretty bad).

In 1.18 this works fine:

    _ = Append(x, MyPtr(new(int)))

and I don't have any problem telling people to write that.

[beoran]

It looks even better if you define a generic Array type a bit like this: https://gotipplay.golang.org/p/tIsplqcunlC
But i agree that for the next version of go it could be fixed.

[rsc]

Completely agree about not doing anything for Go 1.18.
What we have is good enough for the first version.
I don't believe that a future interleaving as described would have to invalidate existing programs.

[findleyr]

Agree about doing nothing for Go 1.18.

We already interleave function argument type inference and constraint type inference when there are untyped arguments, with similar effect. Perhaps this is just an extension of the same principle: in the first pass of function argument type inference we should only bind defined types, for which there can be no ambiguity.
EDIT: as described this does not work in the above example: we would not bind []MyPtr (because it is not defined), and therefore the first pass of function argument type inference would do nothing.

[griesemer]

My primary concern here is that we might be accepting code with the current algorithm that might not be accepted anymore if we change to an interleaving version, which would make a backward-compatible change difficult if not impossible.

But I think that may not be the case after all. Here's a rough outline of an argument that perhaps can be proven more rigorously:

The reason the append example fails is because assignability is a more relaxed relation than identity: if identity of types were required upon assignment, both algorithms would lead to errors. The assignability relation is weaker than identity chiefly because for assignability; at the top level of a (composite) type we don't require identity, we require that the underlying types are identical (ignoring the case where both types are named). Only at the (lower) component level of types, we require identity for assignability. Argument passing relies on assignability; type inference relies on identity.

Given any two arguments, suitably parameterized, we have the general situation

func f[P Cp[P, Q], Q Cq[P, Q], ...](x Tx[P, Q], y Ty[P, Q], ...) ...

Note that Cp and Cq cannot be a simple type parameter (as in interface{Q}), i.e., any use of P or or Q in the constraints Cp and Cq must be at the "lower" level of a composite type. (We only care about such simple composite type constraints, because only those can partake in constraint type inference.)

With the current algorithm, if Tx and Ty are just P and/or Q, the types of P and Q might be inferred to be the named types of the arguments to x and y. This way, a named type might make its way into the constraints Cp and Cq. If all type parameters are inferred through function argument type inference, constraint type inference won't kick in, and upon instantiation, the type arguments for P and Q might not implement Cp or Cq because the matching components of the type arguments don't match the named types brought in by P and Q into the constraints. This is the situation we have above.

If P and Q are at lower levels of Tx and Ty, if its possible to instantiate and call the function in the first place, what is inferred by function argument type inference must match what is inferred by constraint type inference because we require identity at those levels even for assignability.

With the interleaved algorithm, a named type for P or Q might be inferred by constraint type inference from Cp and Cq. Again, at best, P and Q are the types of x and y. The actual function arguments might be of the same named types, or they may be a matching underlying type (this is the situation we have above). Also, because constraint type inference kicked in (due to the interleaving), the actual type argument will satisfy the constraints, if at all possible. So in this case, the inferred type arguments lead to a more "relaxed" function signature.

Thus, it seems at least plausible that the interleaved approach is strictly more powerful than the current approach. This would mean that we should be able to adopt if, should we choose so, without causing existing programs to fail.