Skip to content

Fixes to make dotc compile with capture checking #16254

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 37 commits into from
Nov 10, 2022
Merged

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Oct 27, 2022

This PR contains all fixes and enhancements that were needed to make the compiler itself pass capture checking.

A separate PR #16292 adds a capture-checkable version of the compiler as a test case.

@odersky
Copy link
Contributor Author

odersky commented Nov 6, 2022

Bootstrap achieved: the compiler can now compile itself under capture checking.

So far do not track any capability other than impure functions A => B. The next step will be to track contexts.

@odersky odersky force-pushed the fix-cc branch 2 times, most recently from ba40fd1 to d0995ce Compare November 7, 2022 09:28
@odersky odersky requested a review from Linyxus November 7, 2022 09:31
@odersky
Copy link
Contributor Author

odersky commented Nov 7, 2022

This is probably best reviewed commit by commit.

@odersky
Copy link
Contributor Author

odersky commented Nov 7, 2022

Classification of commits:

  • Bugfix: Fixing something that is clearly a bug
  • Enhancement: Improvements to capture checking rules (can be both relaxations and additional checks)
  • Tweak: Something in between: they influence capture checking in minor or more specialized ways without a clear connection to the theory.

The crash can happen if we compile some modules without capture checking when
other modules are compiled in the same run with capture checking.
Often, the box point is more interesting than the unbox point. It's when unsafe boxing
a variable's RHS that we have to make usre manually that no capability escapes.
They take a `{*} Object` instead of an `Object` parameter.
…le definition

We now allow an inferred type of the form `{C.this} T` if `C` is a pure class.
This is OK since such a type is equivalent to `T`.
An inferred self type in a non-sealed class is now OK if it is the same
as an explicit self type in a base class.
Add a case for cases like

    x.type <:< {r} (A | x.type)

where `x` captures `r`.

# Conflicts:
#	tests/pos-with-compiler-cc/dotc/core/Types.scala
Impure exceptions can't be thrown anyway since `throw` takes a
pure `Throwable` as operand.

The change avoids having to declare explicit pure self types for
exception classes.
When reducing match types, we did not permit to widen an abstract type scrutinee together with
a non-unique type parameter instantiation. But this criterion need not apply if the
widening is in a constraint satisfiabilty check. For instance

    T <: Tuple
    X <: A *: T

    X match
      case x *: (xs <: Tuple) => ...

Here the match does not succeed since X needs to be widened to A *: T and the x parameter
cannot be uniquely instantiated. On the other hand

    A *: T match
      case x *: (xs <: Tuple) => ...

should pass since there is no widening of the scrutinee. But there is a test T <: Tuple to check
whether T can match xs. That second check should not fall under the canWidenAbstract criterion.

Note: I was not able to make a test (without the fix) fail without capture checking, maybe
because the syntax (xs <: Tuple) is actually not allowed. But it is generated after Typer.
We previously required that a class inheriting an @experimental class is itself
@experimental. This is too strict. It should be OK to have the inheriting class
be contained in an experimental scope. I.e.
```
@experimental class A
@experimental object o:
  class B extends A
```
is now OK.
This can replace the more obscure idiom of declaring a
non-capturing self type.
Since root addition handlers are stored in capture sets they should
not close over a context, since otherwise every capture set would
close over a context.

# Conflicts:
#	tests/pos-with-compiler-cc/dotc/cc/CaptureSet.scala
 - Avoid accidental addition of capture set variables through traverseChildren
   of exact ValDefs and DefDefs.
 - Don't require that overriding symbols need explicit types if their capture set
   is non-empty. This is not needed since an overriding symbol with inferred type
   will get the type of the overridden symbol.
We need some special treatment for types such as `(=> A) => B`
Make sure to restore info of anonymous functions and their parameters after cc
…irements

Default getters always have an inferred result type. If that type captures capabilities,
we used to get an error that an inferred non pure type needs to be explicitly defined.
But usually, a default getter type does not matter. So we make an exception and allow
it. Note that this could be a hole, for instance in a situation like this:
```scala
  def f[X](x: X = foo): X = ...
```
If `foo`'s inferred type is `{*} T`, and there is a call to `f()` in the same compilation
unit `X` will be instantiated to `{*} T` and this will also be the result for `f`. But if
the call is in a different compilation unit, it will only see `foo: T`, and the result of
`f` is typed `T`.

A better solution would be to demand that default getter's types are pure, but only if the
getter type can leak into the type of the function to which it belongs. The problem is that
currently that's very hard to do because when we see a default getter it's difficult to
discover to which parameter from which function it belongs.

Therefore, for the moment we leave the hole open, hoping for a better solution to default getters
in the future.
It was already implied before, but so far an explicit rule that

    cs T <: Any

was missing. Adding that rule is important for bounds checking.
It turns out that bounds checking was missing so far.
Two major changes:

 1. During setup, don't generate a capture set variable for a type T if
   one of the base types of `T` is a pure class.

 2. During subtype checking, admit `cs T <: T` if one of the base types
   of `T` is a pure class. The idea is that in this case we know that the
   capture set will always be empty at runtime.

But don't do (2.) if we are checking self types. In this case the capture set cannot be
stripped. Example:

    class A:
      this: A =>
    class B extends A
      this: {c} B =>

In this case we should not assume `{c} B <: B` since we need to flag an error that the self
type of B does not conform to the self type of A.

   are checking self types. In that cas
We need an unsafe transform from

    {*} A => B

to

    box {*} A => B

I don't think this is expressible with `unsafeBox/unsafeUnbox` alone.
…e cc

This is needed to make -Ycheck work after capture checking
Copy link
Contributor

@Linyxus Linyxus left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Other than these minors, LGTM!

&& (recur(tp1.widen.stripCapturing, parent2)
|| tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
// this alternative is needed in case the right hand side is a
// capturing type that contains the lhs as an |-alternative.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is |- here a typo?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, I meant an alternative of a union type (|). I'll make it clearer.

case _ =>
}

if !ctx.reporter.errorsReported then
// We dont report errors hre if previous errors were reported, because other
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Typo.

@@ -911,8 +912,27 @@ class CheckCaptures extends Recheck, SymTransformer:
|The type needs to be declared explicitly.""", t.srcPos)
case _ =>
inferred.foreachPart(checkPure, StopAt.Static)
case t @ TypeApply(fun, args) =>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This case is missing in the documentation. Shall we add the explanation of it?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Where would you add it? It's basically the normal checking that type arguments must fit into type parameter bounds, taking capture setting into account.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was thinking that it would be good to be explained in the docstring of postCheck, since it only talks about the other two cases but not this newly-added one for bounds checking.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that makes sense.

@Linyxus Linyxus assigned odersky and Linyxus and unassigned Linyxus and odersky Nov 9, 2022
@odersky odersky merged commit a21791b into scala:main Nov 10, 2022
@odersky odersky deleted the fix-cc branch November 10, 2022 14:53
odersky added a commit that referenced this pull request Nov 10, 2022
 - Copy compiler code base into a separate test
 - Adapt code base so that it can be capture checked

Based on #16254

Only the last two commits are new:

-
[57527c4](57527c4)
copies the compiler codebase as a separate test.
-
[6dfeaa7](6dfeaa7)
makes the changes so that it passes capture checking.
@Kordyjan Kordyjan added this to the 3.3.0 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants