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.

[sjrd]

That seems to be a problem with ParamRef#superTypeNormalized rather than with disjointnessBoundary.

[dwijnand]

What should superTypeNormalized do?

[sjrd]

It should return the declared type of the corresponding param, which is supposed to be its underlying. I don't see a scenario in which superTypeNormalized should ever return NoType, except possibly for AnyKind itself.

[EugeneFlesselle]

Apparently, it can happen that it is not initialised:
https://github.com/lampepfl/dotty/blob/e994cf06eeee23e8a55a086907957e43140f2112/compiler/src/dotty/tools/dotc/core/Types.scala#L4690-L4695

[sjrd]

That sort of explains it, although it's still concerning that we're attempting to read it from provablyDisjoint when it hasn't been initialized yet. Looks like a time bomb waiting to explode later due to weird compilation order issues.

[EugeneFlesselle]

Yes, and this is not the only case, I ran into a similar issue where normalisation relies on the underlying type, which is not always set as expected. For a TypeRef, it goes through the denotation info, of which the completion seemed a bit unpredictable to me (heavily influenced by small changes in where things happen to be reduced).

Also (maybe) unrelated the normalization depends on the gadt ctx which doesn't seem to be reliably populated when using NamedTypes.

[dwijnand]

I guess I should've opted for AnyKind rather than Any, as the more conservative approach.

[sjrd]

I would still be less uncomfortable if we specifically handled ParamRef to deal with its superTypeNormalized returning NoType; instead of having this "catch-all" NoType. That would limit the blast radius of this workaround. We should also clearly comment that it is a workaround.

[dwijnand]

Sure thing.