go/types: cannot infer type arguments in self-recursive call (stack overflow in unification)

[griesemer]

This is a follow-up on #50755. The following code:

func f[M map[K]int, K comparable](m M) {
        f(m)
}

leads to an internal stack overflow during unification and then type checking fails with error:

M does not match map[K]int

Start of the inference process:

-- inferA [M₁, K₂] -> []
M₁ ≡ M₁
.  M₁ ➞ M₁
-- inferB [M₁, K₂] ➞ [M₁, <nil>]
M₁ ➞ M₁
M₁ ≡ map[K₂]int
.  M₁ ≡ map[K₂]int
.  .  M₁ ≡ map[K₂]int
.  .  .  M₁ ≡ map[K₂]int
.  .  .  .  M₁ ≡ map[K₂]int
etc.

Marking for 1.18 in case the fix is easy. Ok to move to 1.19.

cc: @findleyr

[griesemer]

Likely a duplicate of #48656.

[gopherbot]

Change https://go.dev/cl/385494 mentions this issue: go/types: prototype for eliminating recursive type parameters in

[findleyr]

Just took a look at this. It looks like a fundamental bug that the unification algorithm can't distinguish uninferred type parameters from type parameters occurring in explicit type arguments or function arguments, when they have the same pointer identity.

We can fix in a number of ways. One approach is to create a synthetic copy of the type parameter list and substitute in explicit targs and function arguments. This ensures that we properly differentiate these occurrences from uninferred type parameters, and then we can invert the substitution in the resulting inferred type arguments. https://go.dev/cl/385494 is my quick-and-dirty prototype of this, and seems to work as expected. It also resolved some other tests that had unnecessary errors.

[griesemer]

Yes, you prototyped this a while back when one of these bugs showed up for the first time. I believe this is the right approach: when we call a function from itself, the type parameters that are supplied are getting mixed up with the type parameters for which we want to infer types.

I tried to convince myself that this is correct and this is the argument I came up with: If we would call a different function with the same signature it would all work. For instance, the above example can be changed manually to:

func f_[M map[K]int, K comparable](m M) {
}

func f[M map[K]int, K comparable](m M) {
	f_(m)
}

by calling a synthetic function f_ with the same signature and then inference works because we have different type parameters. So we simply do the same thing automatically by creating the synthetic signature in the inference function and then reverting it. (And we can avoid it if we know that the type parameters are from different functions, but that's an optimization.)

And maybe we can even have an assertion that a type parameter should never infer itself as an argument. After all, this is (one of) the reasons we get endless recursion. In this part of u.nify:

	case i >= 0:
		// x is a type parameter, y is not
		if tx := u.x.at(i); tx != nil {
			return u.nifyEq(tx, y, p)
		}
		// otherwise, infer type from y
		u.x.set(i, y)
		return true

if tx == x the recursive call becomes endless. At the very least we could recognize this case end return false right away. Because that's what we're getting now with the recursion depth check. I'm not sure about the assertion yet, but I think the check for tx == x is a safe shortcut, independent of the suggested fix for this issue.

I will review your CL tomorrow.

[findleyr]

Yes, you prototyped this a while back when one of these bugs showed up for the first time

Right, in https://go.dev/cl/352510. I recalled that CL but thought that it was slightly different, because we figured out a different solution at the time. Looking at it now it is rather the same... down to my quick-and-dirty caveat 🤦. I suppose I am predictable.

We need to differentiate type parameters occurring in the declaration list from type parameters that are passed in at the instantiation site. There are likely other ways to do this, but I'm skeptical about doing it inside the unifier. As you point out, in this case "if tx == x the recursive call becomes endless", but I suspect it would be possible to produce arbitrarily complex recursive patterns. For example:

func f[M map[K]int, K comparable, M2 map[K2]int, K2 comparable](m M, m2 M2) {
        f(m2, m)
}

On first principles it seems necessary to introduce a way to differentiate occurrences of type parameters from inside and outside the type declaration.

I tried to convince myself that this is correct

The way I think about it, type parameters are really two things: they are constraints on a parameter space of types, and they are placeholders for the types that are substituted for those parameters. The problem is that unification is conflating these two things, when it needs to keep them separate. Imagine an analogous example with subsets of a plane:

S1 := { (x, y) | x > 0, y > 0 }
S2 := { (x+y, y) | (x, y) ∈ S1 }

We're effectively trying to check whether S2 ⊂ S1, but get stuck in an infinite recursion because we can't differentiate the x and y on the first line from the x and y on the second line.

We could alternatively do the substitution in the declaration type parameter list, which could be memoized, but I suspect it is more efficient to substitute in targs and args as in the common case they will not contain references to the type parameters being unified.

I will clean up my CL.

[findleyr]

We could alternatively do the substitution in the declaration type parameter list, which could be memoized, but I suspect it is more efficient to substitute in targs and args as in the common case they will not contain references to the type parameters being unified.

While going through and closing tabs, I noticed this and thought I'd close the loop:

The primary advantage of substituting in args rather than params was that most of the time it would be a no-op. However, @griesemer had a great suggestion for how to cheaply detect self-recursive calls, and so we were able to substitute in parameters only in the case of self-recursion. This significantly simplified the complexity of the substitution code.