Skip to content
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

Three changes to typing rules #14392

Closed
wants to merge 24 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
98bc26d
Merge pull request #12971 from dotty-staging/add-rechecker
odersky Aug 17, 2021
4b88b5a
Cleanups
odersky Aug 17, 2021
5e4e4f0
First version of capture checker.
odersky Sep 29, 2021
2941b6a
Include capture sets of methods in enclosing class
odersky Oct 2, 2021
20cf766
Update iterators example
odersky Nov 19, 2021
f18d951
Add capture checks for mutable variables
odersky Oct 5, 2021
a5d9d06
Implement deep check for variables
odersky Oct 5, 2021
0b130e3
Introduce @capability annotations
odersky Dec 12, 2021
1513393
Fix typo and update semanticdb.expect
odersky Dec 12, 2021
81512d5
Disable MiMa checks
odersky Dec 12, 2021
12f17a4
Special rule for {this} in capture sets of class members
odersky Dec 23, 2021
f134adb
Pure function types -> and ?->
odersky Dec 25, 2021
9bc09ee
Updates for latest master
odersky Jan 21, 2022
e349acc
Shorthand for curried functions
odersky Dec 23, 2021
670e510
Syntax change: allow capture sets in infix types
odersky Jan 26, 2022
7ba7c89
Test for contravariantly used class fields
odersky Jan 26, 2022
42c9eed
Handle captures in by-name parameters
odersky Jan 23, 2022
91299b2
Treat exceptions as capabilities
odersky Jan 25, 2022
9033e0c
Mark classes compiled under -Ycc with a CaptureChecked annotation
odersky Jan 26, 2022
6d672b1
Map regular function types to impure function types when unpickling
odersky Jan 26, 2022
18dd570
New scheme to reject root captures
odersky Jan 28, 2022
4cc8ff0
Three changes to typing rules
odersky Jan 30, 2022
fedd8f2
Change result type of by-name closures
odersky Feb 1, 2022
0ddbbe8
Capture-check exception capabilties
odersky Feb 1, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Special rule for {this} in capture sets of class members
Consider the lazylists.scala test in pos-custom-args/captures:
```scala
class CC
type Cap = {*} CC

trait LazyList[+A]:
  this: ({*} LazyList[A]) =>

  def isEmpty: Boolean
  def head: A
  def tail: {this} LazyList[A]

object LazyNil extends LazyList[Nothing]:
  def isEmpty: Boolean = true
  def head = ???
  def tail = ???

extension [A](xs: {*} LazyList[A])
  def map[B](f: {*} A => B): {xs, f} LazyList[B] =
    class Mapped extends LazyList[B]:
      this: ({xs, f} Mapped) =>

      def isEmpty = false
      def head: B = f(xs.head)
      def tail: {this} LazyList[B] = xs.tail.map(f)  // OK
    new Mapped
```
Without this commit, the second to last line is an error since the right hand side
has capture set `{xs, f}` but the required capture set is `this`.

To fix this, we widen the expected type of the rhs `xs.tail.map(f)` from `{this}` to
`{this, f, xs}`. That is, we add the declared captures of the self type to the expected
type. The soundness argument for doing this is as follows:

Since `tail` does not have parameters, the only thing it could capture are references that the
receiver `this` captures as well. So `xs` and `f` must come via `this`. For instance, if
the receiver `xs` of `xs.tail` happens to be pure, then `xs.tail` is pure as well.

On the other hand, in the neg test `lazylists1.scala` we add the following line to `Mapped`:
```scala
      def concat(other: {f} LazyList[A]): {this} LazyList[A] = ??? : ({xs, f} LazyList[A]) // error
```
Here, we cannot widen the expected type from `{this}` to `{this, xs, f}` since the result of concat
refers to `f` independently of `this`, namely through its parameter `other`. Hence, if `ys: {f} LazyList[String]`
then
```
   LazyNil.concat(ys)
```
still refers to `f` even though `LazyNil` is pure. But if we would accept the definition of `concat`
above, the type of `LazyNil.concat(ys)` would be `LazyList[String]`, which is unsound.

The current implementation widens the expected type of class members if the class member does not
have tracked parameters. We could potentially refine this to say we widen with all references in
the expected type that are not subsumed by one of the parameter types.

## Changes:

### Refine rule for this widening

We now widen the expected type of the right hand side of a class member as follows:

Add all references of the declared type of this that are not subsumed by a capture set
of a parameter type.

### Do expected type widening only in final classes

Alex found a counter-example why this is required. See map5 in
neg-customargs/captures/lazylists2.scala
odersky committed Jan 28, 2022
commit 12f17a4f2dce9f7a80c52174e6214b349c635771
9 changes: 8 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
@@ -49,7 +49,14 @@ sealed abstract class CaptureSet extends Showable:
/** Is this capture set definitely non-empty? */
final def isNotEmpty: Boolean = !elems.isEmpty

/** Cast to variable. @pre: @isConst */
/** Cast to Const. @pre: isConst */
def asConst: Const = this match
case c: Const => c
case v: Var =>
assert(v.isConst)
Const(v.elems)

/** Cast to variable. @pre: !isConst */
def asVar: Var =
assert(!isConst)
asInstanceOf[Var]
7 changes: 5 additions & 2 deletions compiler/src/dotty/tools/dotc/transform/Recheck.scala
Original file line number Diff line number Diff line change
@@ -203,12 +203,15 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
bindType

def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Unit =
if !tree.rhs.isEmpty then recheck(tree.rhs, sym.info)
if !tree.rhs.isEmpty then recheckRHS(tree.rhs, sym.info, sym)

def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Unit =
val rhsCtx = linkConstructorParams(sym).withOwner(sym)
if !tree.rhs.isEmpty && !sym.isInlineMethod && !sym.isEffectivelyErased then
inContext(rhsCtx) { recheck(tree.rhs, recheck(tree.tpt)) }
inContext(rhsCtx) { recheckRHS(tree.rhs, recheck(tree.tpt), sym) }

def recheckRHS(tree: Tree, pt: Type, sym: Symbol)(using Context): Type =
recheck(tree, pt)

def recheckTypeDef(tree: TypeDef, sym: Symbol)(using Context): Type =
recheck(tree.rhs)
16 changes: 16 additions & 0 deletions compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
Original file line number Diff line number Diff line change
@@ -322,6 +322,22 @@ class CheckCaptures extends Recheck:
interpolateVarsIn(tree.tpt)
curEnv = saved

override def recheckRHS(tree: Tree, pt: Type, sym: Symbol)(using Context): Type =
val pt1 = pt match
case CapturingType(core, refs, _)
if sym.owner.isClass && !sym.owner.isExtensibleClass
&& refs.elems.contains(sym.owner.thisType) =>
val paramCaptures =
sym.paramSymss.flatten.foldLeft(CaptureSet.empty) { (cs, p) =>
val pcs = p.info.captureSet
(cs ++ (if pcs.isConst then pcs else CaptureSet.universal)).asConst
}
val declaredCaptures = sym.owner.asClass.givenSelfType.captureSet
pt.derivedCapturingType(core, refs ++ (declaredCaptures -- paramCaptures))
case _ =>
pt
recheck(tree, pt1)

override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type =
for param <- cls.paramGetters do
if param.is(Private) && !param.info.captureSet.isAlwaysEmpty then
7 changes: 7 additions & 0 deletions tests/neg-custom-args/captures/lazylists1.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists1.scala:25:63 -----------------------------------
25 | def concat(other: {f} LazyList[A]): {this} LazyList[A] = ??? : ({xs, f} LazyList[A]) // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: {xs, f} LazyList[A]
| Required: {Mapped.this, xs} LazyList[A]

longer explanation available when compiling with `-explain`
27 changes: 27 additions & 0 deletions tests/neg-custom-args/captures/lazylists1.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
class CC
type Cap = {*} CC

trait LazyList[+A]:
this: ({*} LazyList[A]) =>

def isEmpty: Boolean
def head: A
def tail: {this} LazyList[A]

object LazyNil extends LazyList[Nothing]:
def isEmpty: Boolean = true
def head = ???
def tail = ???

extension [A](xs: {*} LazyList[A])
def map[B](f: {*} A => B): {xs, f} LazyList[B] =
final class Mapped extends LazyList[B]:
this: ({xs, f} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f) // OK
def drop(n: Int): {this} LazyList[B] = ??? : ({xs, f} LazyList[B]) // OK
def concat(other: {f} LazyList[A]): {this} LazyList[A] = ??? : ({xs, f} LazyList[A]) // error
new Mapped

45 changes: 45 additions & 0 deletions tests/neg-custom-args/captures/lazylists2.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
-- [E163] Declaration Error: tests/neg-custom-args/captures/lazylists2.scala:50:10 -------------------------------------
50 | def tail: {xs, f} LazyList[B] = xs.tail.map(f) // error
| ^
| error overriding method tail in trait LazyList of type => {Mapped.this} LazyList[B];
| method tail of type => {xs, f} LazyList[B] has incompatible type

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:18:4 ------------------------------------
18 | final class Mapped extends LazyList[B]: // error
| ^
| Found: {f, xs} LazyList[B]
| Required: {f} LazyList[B]
19 | this: ({xs, f} Mapped) =>
20 | def isEmpty = false
21 | def head: B = f(xs.head)
22 | def tail: {this} LazyList[B] = xs.tail.map(f)
23 | new Mapped

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:27:4 ------------------------------------
27 | final class Mapped extends LazyList[B]: // error
| ^
| Found: {f, xs} LazyList[B]
| Required: {xs} LazyList[B]
28 | this: ({xs, f} Mapped) =>
29 | def isEmpty = false
30 | def head: B = f(xs.head)
31 | def tail: {this} LazyList[B] = xs.tail.map(f)
32 | new Mapped

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:41:48 -----------------------------------
41 | def tail: {this} LazyList[B] = xs.tail.map(f) // error
| ^^^^^^^^^^^^^^
| Found: {f} LazyList[B]
| Required: {xs} LazyList[B]

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:59:48 -----------------------------------
59 | def tail: {this} LazyList[B] = xs.tail.map(f) // error
| ^^^^^^^^^^^^^^
| Found: {f} LazyList[B]
| Required: {Mapped.this} LazyList[B]

longer explanation available when compiling with `-explain`
64 changes: 64 additions & 0 deletions tests/neg-custom-args/captures/lazylists2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
class CC
type Cap = {*} CC

trait LazyList[+A]:
this: ({*} LazyList[A]) =>

def isEmpty: Boolean
def head: A
def tail: {this} LazyList[A]

object LazyNil extends LazyList[Nothing]:
def isEmpty: Boolean = true
def head = ???
def tail = ???

extension [A](xs: {*} LazyList[A])
def map[B](f: {*} A => B): {f} LazyList[B] =
final class Mapped extends LazyList[B]: // error
this: ({xs, f} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f)
new Mapped

def map2[B](f: {*} A => B): {xs} LazyList[B] =
final class Mapped extends LazyList[B]: // error
this: ({xs, f} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f)
new Mapped

def map3[B](f: {*} A => B): {xs} LazyList[B] =
final class Mapped extends LazyList[B]:
this: ({xs} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f) // error
new Mapped

def map4[B](f: {*} A => B): {xs} LazyList[B] =
final class Mapped extends LazyList[B]:
this: ({xs, f} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {xs, f} LazyList[B] = xs.tail.map(f) // error
new Mapped

def map5[B](f: {*} A => B): LazyList[B] =
class Mapped extends LazyList[B]:
this: ({xs, f} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f) // error
class Mapped2 extends Mapped:
this: Mapped =>
new Mapped2


27 changes: 27 additions & 0 deletions tests/pos-custom-args/captures/lazylists-mono.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
class CC
type Cap = {*} CC

//-------------------------------------------------

def test(E: Cap) =

trait LazyList[+A]:
protected def contents: {E} () => (A, {E} LazyList[A])
def isEmpty: Boolean
def head: A = contents()._1
def tail: {E} LazyList[A] = contents()._2

class LazyCons[+A](override val contents: {E} () => (A, {E} LazyList[A]))
extends LazyList[A]:
def isEmpty: Boolean = false

object LazyNil extends LazyList[Nothing]:
def contents: {E} () => (Nothing, LazyList[Nothing]) = ???
def isEmpty: Boolean = true

extension [A](xs: {E} LazyList[A])
def map[B](f: {E} A => B): {E} LazyList[B] =
if xs.isEmpty then LazyNil
else
val cons = () => (f(xs.head), xs.tail.map(f))
LazyCons(cons)
42 changes: 42 additions & 0 deletions tests/pos-custom-args/captures/lazylists.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
class CC
type Cap = {*} CC

trait LazyList[+A]:
this: ({*} LazyList[A]) =>

def isEmpty: Boolean
def head: A
def tail: {this} LazyList[A]

object LazyNil extends LazyList[Nothing]:
def isEmpty: Boolean = true
def head = ???
def tail = ???

extension [A](xs: {*} LazyList[A])
def map[B](f: {*} A => B): {xs, f} LazyList[B] =
final class Mapped extends LazyList[B]:
this: ({xs, f} Mapped) =>

def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f) // OK
def concat(other: {f} LazyList[A]): {this, f} LazyList[A] = ??? : ({xs, f} LazyList[A]) // OK
if xs.isEmpty then LazyNil
else new Mapped

def test(cap1: Cap, cap2: Cap) =
def f(x: String): String = if cap1 == cap1 then "" else "a"
def g(x: String): String = if cap2 == cap2 then "" else "a"

val xs =
class Initial extends LazyList[String]:
this: ({cap1} Initial) =>

def isEmpty = false
def head = f("")
def tail = LazyNil
new Initial
val xsc: {cap1} LazyList[String] = xs
val ys = xs.map(g)
val ysc: {cap1, cap2} LazyList[String] = ys
35 changes: 35 additions & 0 deletions tests/pos-custom-args/captures/lazylists1.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
class CC
type Cap = {*} CC

trait LazyList[+A]:
this: ({*} LazyList[A]) =>

def isEmpty: Boolean
def head: A
def tail: {this} LazyList[A]

object LazyNil extends LazyList[Nothing]:
def isEmpty: Boolean = true
def head = ???
def tail = ???

final class LazyCons[+T](val x: T, val xs: {*} () => {*} LazyList[T]) extends LazyList[T]:
this: ({*} LazyList[T]) =>

def isEmpty = false
def head = x
def tail: {this} LazyList[T] = xs()

extension [A](xs: {*} LazyList[A])
def map[B](f: {*} A => B): {xs, f} LazyList[B] =
if xs.isEmpty then LazyNil
else LazyCons(f(xs.head), () => xs.tail.map(f))

def test(cap1: Cap, cap2: Cap) =
def f(x: String): String = if cap1 == cap1 then "" else "a"
def g(x: String): String = if cap2 == cap2 then "" else "a"

val xs = LazyCons("", () => if f("") == f("") then LazyNil else LazyNil)
val xsc: {cap1} LazyList[String] = xs
val ys = xs.map(g)
val ysc: {cap1, cap2} LazyList[String] = ys