Decrement depth in subtype check withTypeVars

[joroKr21]

Fixes scala/bug#7612

The LUB becomes Kili[_ >: A with B <: Kili[_ >: A with B <: Object]].
That makes sense to me.

[adriaanm]

Let's see if we can keep the depth bookkeeping in GlbLubs. Suggestion added, but not tested in depth.

[adriaanm]

This works, but I'd prefer to keep the depth bookkeeping logic in GlbLubs. How about adding a .decr in this spot:

scala/src/reflect/scala/reflect/internal/tpe/GlbLubs.scala

Line 354 in a2cd257

isSubType(t, lubRefined, depth) || {

In my superficial local testing, this also seems to break the cycle for this test case. What do you think?

[joroKr21]

Ah yes, you are right, that works too! I wonder if this check is even needed though. The comment about higher-order type parameters shouldn't be true anymore.

[adriaanm]

Yes! Definitely worth looking into getting rid of this additional check.

[joroKr21]

Ok I tried to disable the check entirely. Let's see what CI says. If it's all is green we can try a community build with this change.

However the LUB looks weird now:
Kili[_ >: A with B <: Kili[_ >: A with B <: Object]]{def fili: Fili[_ >: A with M]}

[joroKr21]

That failed quickly. But the errors reveal some fishy code paths.

val concretes = concreteTypes(tvar)
(concretes contains AnyRefClass) || (concretes contains site.memberType(tvar))

Checking if a list of types contains a symbol, for example?

[adriaanm]

contains-Any strikes again!

[joroKr21]

I made only the suggested changes now, which means the LUB is:

 Kili[_ >: A with B <: Kili[_ >: A with B <: Object]]{def fili: Fili[_ >: A with M]}

I don't know why the type parameter M is leaking in the signature, but it doesn't seem to be a problem?

Apart from that I don't have any rational argument of why I prefer decrementing in withTypeVars. To me it just seems like a problematic code path altogether.

[adriaanm]

As far as I know, the depth argument is meant specifically for avoiding blowups in lub/glb, so I don't understand why it should be decremented in existential type subtyping (if so, why not also in polytype subtyping?)

[adriaanm]

The fact that M occurs in the result does sound like a(nother) bug

[joroKr21]

As far as I know, the depth argument is meant specifically for avoiding blowups in lub/glb, so I don't understand why it should be decremented in existential type subtyping (if so, why not also in polytype subtyping?)

et2.withTypeVars(isSubType(tp1, _, depth), depth) uses depth twice. I meant the second one which is used when solving for the quantified variables. Of course it makes no sense to decrement in the underlying subtype check. Since we only care that there is a solution for the quantified variables but not what that solutions is, I'm not sure how much the depth matters there.

But I agree the same can be said about LUB verification.

As long as we know that it's not possible to constrain a quantified variable recursively with the existential type itself, it should be fine.

The fact that M occurs in the result does sound like a(nother) bug

One bug at a time 😃

[adriaanm]

My rationale comes from having the structure of the computation of the maximal depth be reflected in how it's decremented. I don't see a link between existential subtyping and typeDepth, but there is one (albeit tenuous) in recursive calls to lub/glb.