Approximate MatchTypes with lub of case bodies, if non-recursive

[dwijnand]

Fixes #19710

[dwijnand]

@mbovel @EugeneFlesselle @sjrd cc @nicolasstucki Do you remember why we don't approximate match types with the lub of their bodies? I thought I had done this experiment before, before Seb's reimplementation, proving how it's wrong. Doing the experiment now, it seems to work. So, is this wrong? I.e. unsound?

[nicolasstucki]

I do not remember.

[sjrd]

At the very least, it does not correspond to anything that was ever specified or documented. Doing that would require a dedicated rule in the type system.

Off the top of my head, I don't see why it would be unsound. But that's also assuming that type bounds are correctly checked in the bodies, which IIUC is not done yet?

[dwijnand]

But that's also assuming that type bounds are correctly checked in the bodies, which IIUC is not done yet?

I believe so:

https://github.com/lampepfl/dotty/blob/98efdab3c3edaac379c07b979f9ff103bf13cd07/compiler/src/dotty/tools/dotc/typer/Typer.scala#L2378-L2379

[EugeneFlesselle]

@dwijnand Some issues had been discussed in #8085, perhaps filtering for recursive match-types is enough to avoid then though.

[dwijnand]

I like the approach of caching the lub once during typing, much smarter. I'll try that change.

[EugeneFlesselle]

I like the approach of caching the lub once during typing, much smarter. I'll try that change.

I'm wondering however if doing the check during subtyping might make use of a narrowed context ? Or more generally, when it could be useful to recompute the bound. For example if a match type is inherited and the scrutinee has been refined.

In any case, I think this would be a great improvement.