Extract GADT constraints from wildcard type arguments

[dwijnand]

No description provided.

[dwijnand]

This regressed with #12506 (which shipped with 3.0.2).

[dwijnand]

@abgruszecki could you review this please, or delegate the review to someone else?

[abgruszecki]

@dwijnand I was going to prepare a different fix for the problem, but it looks like it's not going to happen any time soon. Let me just suggest a comment that I think should be there and we can merge this PR.

[smarter]

@abgruszecki so it's not clear to me if this change is actually sound? The previous comment mentioned that this was unsound but didn't provide a test case, and the new comment just says this fix isn't "proper" but it's not clear to me what that implies.

[abgruszecki]

@smarter we don't pass TypeBounds themselves to isSubType here, we just "give up" on what I did in the deskolemization PR (referenced in the new comment) and instead we call isSubType on the entire types. It's not proper in the sense that using SkolemType in this way results in problems in some edge cases, but at least it fixes the regression.

[smarter]

Do you have an example of these edge cases?

[abgruszecki]

These issues were fixed by the deskolemization PR:

• Overconstrained GADT bounds in presence of type bounds with non-variant type constructors  #11103
• Infinite type comparison when narrowing GADT bounds #12476

[abgruszecki]

So after a discussion with Guillaume, there's one more thing that should be said: this PR may have introduced unsoundness into the compiler. I paid too much attention to us regressing after the deskolemization PR, but that PR was actually necessary to fix some soundness issues, like #11103. With that in mind, we should either have a very good & convincing case why this fix is certainly sound, or we should go ahead and rewrite the isSubType check added in this PR to compare the "elements" of TypeBounds instead of comparing the entire types.

[dwijnand]

If you can come up with an unsound example, I'm happy to redo this PR. But without more information I wouldn't know which parts of isSubType are the unsound bits and which are the sound ones that should be inlined.

Are you free next Tuesday to pair on this in the Scala Spree?