Do level checking on instantiation

[odersky]

Level checking was first implemented #14026. The idea was to avoid level-incorrect constraints from the outset, by cloning type variables and adjusting bounds as needed. This fixed a number of issues, but also caused a number of regressions since the number of added type variables had subtle interactions with other aspects of type checking.

This PR is more conservative in its change set: It still allows level-incorrect constraints to be formed, but fixes levels when type variables are instantiated. To do this soundy, it uses an "untrusted bounds" mode in the type comparer, under which we do not accidentally forget types when forming lubs or glbs with other references that have bad bounds.

One can choose between level checking when forming constraints (i.e. #14026) vs level checking on instantiation (i.e. #15746) by setting the value Config.checkLevelsOnConstraints

Fixes #8900
Fixes #15595

[odersky]

@smarter I have put everything under two config flags, so one can switch between

• no level checking at all (unsound)
• level checking on instantiation
• level checking on constraint formation

That way, we can fix the immediate issues while we take more time to decide what kind of checking is best.

[odersky]

@WojciechMazur This commit is fairly high risk for regressions. Can you run the large CB with this branch to see what would break?

[WojciechMazur]

Sure, I've started the build and its progress can be found here https://scala3.westeurope.cloudapp.azure.com/blue/organizations/jenkins/runBuild/detail/runBuild/6/pipeline
I should be able to aggregate the results on Monday. So far I can see some type related problems with the compilation of Akka https://scala3.westeurope.cloudapp.azure.com/job/buildCommunityProject/268/

[odersky]

So I conclude we have some breakage. @WojciechMazur from your experience, can you give an estimate how bad it is?

On the other hand, the current situation with unsound and buggy type variable instantiation is untenable. So we will need to make the effort to minimize the regressions and try to fix them individually. I am not sure whether this is better done with a merged PR or before. In any case we should merge this PR at the start of a release cycle.

[odersky]

I think we should merge this now, as long as we are in the beginning of a release cycle, and have a chance to catch regressions. Who can give it a review?

[smarter]

Shouldn't we check whether this breaks more or less things in the open community build than the previous level-checking logic before settling on this approach?
I won't be able to do a thorough review of this PR this month but one thing that really needs to be addressed is the use of a var in TypeVar in https://github.com/lampepfl/dotty/pull/15746/files#diff-c59c50b7dcb6f1a4eb6d807a1c6c54a684c01e368d3a293ae8fd055531ac97faR4508. This will lead to very weird bugs whenever the constraint is rolled back, as explained in the commit message of 3ab18a9 :

Each fresh variable will be upper-
or lower-bounded by the existing variable it is substituted for
depending on variance (an idea that I got from [1]), in the invariant
case the existing variable will be instantiated to the fresh one (unlike
[2], we can't simply mutate the nestingLevel of the existing variable
after running avoidance on its bounds because the constraint containing
these bounds might later be retracted).

[odersky]

Shouldn't we check whether this breaks more or less things in the open community build than the previous level-checking logic before settling on this approach?

I don't think so, since we can selectively turn either logic on. Level checking on constraint formation clearly does not work as is, and requires major changes to several parts of the type checker to make it work. There's no-one scheduled or volunteering to do these changes, so we cannot count on them to be done. Level checking on instantiation has a chance to work, we have to go through the effort of minimization and see what the reasons for the breakages are.

Not doing level checking at all (which is the current state) also clearly does not work, and, if not addressed will just encourage more unsound code.

I won't be able to do a thorough review of this PR this month but one thing that really needs to be addressed is the use of a var in TypeVar in https://github.com/lampepfl/dotty/pull/15746/files#diff-c59c50b7dcb6f1a4eb6d807a1c6c54a684c01e368d3a293ae8fd055531ac97faR4508. This will lead to very weird bugs whenever the constraint is rolled back, as explained in the commit message of 3ab18a9 :

I am actually not so sure about this. The worst that could happen is that a type variable gets a lower level than expected, which is still sound. I find the alternative of instantiating type variables very complicated, and will not have time to do it. So i propose we merge with the option of improving this aspect later.

[smarter]

There's no-one scheduled or volunteering to do these changes

It's something I'd like to do, although I can't promise when exactly right now.

The worst that could happen is that a type variable gets a lower level than expected, which is still sound.

It's probably sound, but it leads to weird "action at a distance" effects. Type inference bugs are already very hard to debug because there's so many interactions to consider, but with this change I fear the situation would get 10x harder to deal with: now some logic in a retracted TyperState might influence whether your code compiles or not, this will lead to regressions that take enormous effort to understand and that probably cannot be fixed.

[odersky]

I think in summary, with the long list of failures associated with the current disabled behavior, it's still better to go ahead and merge this. I am not happy about it, but I don't see a practicable alternative.

[odersky]

I opened issue #15884 to keep track of the nestingLevel update problem.

[odersky]

It's something I'd like to do, although I can't promise when exactly right now.

I think that would be good. But we cannot keep the code in the current problematic state until this is resolved. I think this needs to go into 3.2.1. So I propose we get back to it later, without the pressure of time constraints.

[smarter]

Ok, but it would still be good if someone else could review this then.

[odersky]

@dwijnand Do you think you could give this a go? It's plain constraints as opposed to GADT constraints but since the two are duals it should be close.

[odersky]

I found a solution for the problem of hidden state in nestingLevel: Make the state explicit in TyperState where updates to nesting levels are stored.

[smarter]

Nice! I was considering whether the nestingLevel should be stored in the Constraint, because there's multiple places where we rollback constraints without rolling back the full TyperState, e.g:

• https://github.com/lampepfl/dotty/blob/ead0fbc7804026e2c764f88f7576029c2fb7a51f/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala#L103
• https://github.com/lampepfl/dotty/blob/ead0fbc7804026e2c764f88f7576029c2fb7a51f/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1766
• https://github.com/lampepfl/dotty/blob/ead0fbc7804026e2c764f88f7576029c2fb7a51f/compiler/src/dotty/tools/dotc/typer/Applications.scala#L2226

But perhaps these places should use TyperState#{snapshot, resetTo} instead.

[odersky]

But perhaps these places should use TyperState#{snapshot, resetTo} instead.

Yes, that seems right.

[odersky]

Actually, I think we need the TyperState shapshot only for harmonize. The operations in ProtoTypes and TypeComparer only affect constraints but do not instantiate type variables.

[odersky]

In fact, I am not sure what to do about harmonize. It seems that resetting the constraint is fishy and resetting the typerstate is clearly wrong. We need to come back to this.

[WojciechMazur]

Regressions found in the open community build:
Tested 639 projects, 6 regressions found based on the commit f01abfb after exclusion of failures due to missing dependencies and regressions present in 3.2.1-nightly

Project	Version	Build URL
akka/akka	2.6.19	Open CB #2604
fd4s/vulcan	1.8.3	Open CB #2607	Fails in main, so probably not related
mvv/sager	0.2-M1	Open CB #2611	Fails in main, so probably not related
scala-ts/scala-ts	0.5.13	Open CB #2612	Fails in main, so probably not related
sirthias/borer	1.10.1	Open CB #2622	Fails in main, so probably not related
zio/zio-query	0.3.1	Open CB #2614

[dwijnand]

Akka failure:

[info] compiling 21 Scala sources and 2 Java sources to /home/jenkins/agent/workspace/buildCommunityProject/repo/akka-cluster-typed/target/scala-3.2.1-RC1-bin-f01abfba6840d8e91e1a8936cd7c112007667a23-COMMUNITY-BUILD/classes ...
[error] -- [E007] Type Mismatch Error: /home/jenkins/agent/workspace/buildCommunityProject/repo/akka-cluster-typed/src/main/scala/akka/cluster/ddata/typed/internal/ReplicatorBehavior.scala:92:46 
[error] 92 |                reply.foreach { cmd.replyTo ! _ }
[error]    |                                              ^
[error]    |Found:    akka.cluster.ddata.typed.javadsl.Replicator.GetResponse[?1.CAP]
[error]    |Required: akka.cluster.ddata.typed.javadsl.Replicator.GetResponse[d]
[error]    |
[error]    |where:    ?1 is an unknown value of type scala.runtime.TypeBox[d, akka.cluster.ddata.ReplicatedData]
[error]    |          d  is a type in an anonymous function in method withState with bounds <: akka.cluster.ddata.ReplicatedData
[error]    |
[error]    | longer explanation available when compiling with `-explain`
[error] one error found

[odersky]

Is there a way to minimize the Akka failure? So far it does not tell us much. ?.CAP is an unknown instance of some type parameter. It's quite plausible that we first instantiated a type variable to something unsound and then this was the fallback. But it could also be something else.

[dwijnand]

I can't reproduce it, but the code looks like something that you could easily fix with an explicit type argument or type annotation. The fix looks good to me. I might continue to try to recreate a minimised version of Akka's failure tomorrow.