Refine criterion when to widen types

[odersky]

Refine criterion when to widen types in match type reduction.

We now do not widen if the compared-against type contains variant named type parameters. This is intended to fix the soundness problem in #17149. It also fixes the regression in #15926. @Decel was right in suggesting these two were related.

Fixes #17149
Fixes #15926

Todos:

• Check & fix neg test failures
• Add more tests
• Also consider approximating abstract types to lower bounds. This is completely missing so far. There are neither tests nor an implementation.
• Update the docs on match types to explain what goes on here.

[odersky]

@Decel, @dwijnand Can one or both of you take this over and address the remaining points? It's a tricky area, I believe quite a bit more work will be needed to arrive at a fully satisfactory solution.

[dwijnand]

@odersky Happy to. @Decel let me know if you want to sync in a call or on the LAMP slack.

Also, what do you think of my approach in #17173? I don't quite get the mechanics of Ranges in ApproximatingTypeMap's, so I wondered if it can be cleaned up further. But generally, it solves the problem within matchCases alone. (The other pickler and tupleElementTypes changes are both Ytest-pickler related.)

[odersky]

I left a comment on #17173.

[odersky]

One thing where #17180 falls short is error diagnostics. When we do not widen, we essentially get a "Stuck" error saying scrutinee is not a subtype and is not disjoint either. But before we got a "variable cannot be uniquely instantiated" error, which is much better. After all, scrutinee is a subtype of pattern in this case, for some instantiation of type variables.

We could recover the original error diagnostics by doing the widening in widenAbstractOKFor instead of preventing it, but "poisoning" any variant type variables in the other type. Then in redux we can flag such type variable instantiations (but maybe using Range is not the best way to do this). Then we can take these flagged variables and issue a MatchResult.NoInstance message.

So my proposal would be:

• change widenAbstractOKFor to always return canWidenAbstract but poison variant type variables in the other type.
• in paramInstance record poisoned and undetermined type variables instead of wrapping with Range.
• In redux produce a NoInstance error if bad type variables were recorded.

That could lead to much better error messages. And diagnostics is really important for match types, since the algorithms are so complex.

[odersky]

I think the new neg tests are effectivly less informative than the old ones. So before fixing the check files we should try to improve the diagnostics to a point where they are equivalent.

[dwijnand]

I agree. I marked it draft to convey that even if it's green, it's not to be merged.

[Decel]

Also fixes #16504

[odersky]

@Decel @dwijnand What's the status here?

[dwijnand]

Let's look at it this this coming week (24th).

[Decel]

So, we have managed to find a counterexample with @dwijnand:

trait Show[-A >: Nothing]

type MT1[I <: Show[Nothing], N] = I match
  case Show[a] => N match
    case 0     => a

val a = summon[MT1[Show[Any], 0] =:= Any]

[dwijnand]

LGTM, pending Martin's review

[dwijnand]

@odersky I can't request your review of your PR, but could you have a look and say if you're happy with this landing? Thank you.

[dwijnand]

LGTM, pending Martin's review