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

Fix #8861: Avoid parameters when instantiating closure results #8867

Merged
merged 11 commits into from
May 9, 2020

Conversation

odersky
Copy link
Contributor

@odersky odersky commented May 3, 2020

This was much harder than I anticipated, probably the hardest thing to fix for the last year or so.

The fundamental problem is that when typing closures, we pass a partially instantiated expected type down as the result type of the closure. Type variables in this type might get constraints polluted with local parameter references. If we instantiate these type variables to these local types
referring such local parameters, unsoundness results.

Now, the easy fix would to simply not pass uninstantiated variables into scopes where their constraints can be polluted. Approximate them with wildcards instead. Unfortunately this causes some projects to fail. Notably zio, and test run-macros/quote-matcher-symantics-3 since type inference propagates not enough. So, while it's the safe route it's not really an option at this point.

I also tried to apply avoidance to the whole constraint at the end of type checking the body of a closure, but that's tricky, in particular for curried closures.

I finally tried various backtracking schemes to alternatively type check with wildcards or type variables, but none of them passed all the test and they all got messy quickly.

So, this PR tackles the problem at the root: When trying to instantiate a type variable, avoid all term references to parameters or local variables that are nested more deeply than the type variable itself. This means we have to keep track of nesting levels for symbols and type variables. If such avoidance gives an instance type that does not fit the constraint bounds, throw a type error.

There might be other possible ways to deal with it. But in any case, the current PR is a useful defensive programming measure. No matter what we do, we should not instantiate a type variable
to references that are more deeply nested. So, arguably it's useful in any case.

@@ -1556,6 +1556,17 @@ class Namer { typer: Typer =>
val termParamss = ctx.normalizeIfConstructor(vparamss.nestedMap(symbolOfTree), isConstructor)
sym.setParamss(typeParams, termParamss)
def wrapMethType(restpe: Type): Type = {
restpe match
case tv: TypeVar
Copy link
Member

@smarter smarter May 3, 2020

Choose a reason for hiding this comment

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

Checking for type variables at the top-level is not enough, for example I can reproduce the ClassCastException by wrapping the result type in an identity type lambda:

object Test {
  type Id[T] = T

  sealed trait Container { s =>
    type A
    def visit[R](int: IntV & s.type => Id[R], str: StrV & s.type => Id[R]): R
  }
  final class IntV extends Container { s =>
    type A = Int
    val i: Int = 42
    def visit[R](int: IntV & s.type => Id[R], str: StrV & s.type => Id[R]): R = int(this)
  }
  final class StrV extends Container { s =>
    type A = String
    val t: String = "hello"
    def visit[R](int: IntV & s.type => Id[R], str: StrV & s.type => Id[R]): R = str(this)
  }

  def minimalOk[R](c: Container { type A = R }): R = c.visit[R](
    int = vi => vi.i : Id[vi.A],
    str = vs => vs.t : Id[vs.A]
  )
  def minimalFail[M](c: Container { type A = M }): M = c.visit(
    int = vi => vi.i : Id[vi.A],
    str = vs => vs.t : Id[vs.A]  // error
  )

  def main(args: Array[String]): Unit = {
    val e: Container { type A = String } = new StrV
    println(minimalOk(e)) // this one prints "hello"
    println(minimalFail(e)) // this one fails with ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer
  }
}

(more complex types are also probably problematic but slightly harder to get a ClassCastException out of)

@odersky odersky force-pushed the fix-#8861 branch 2 times, most recently from 5965190 to 39b9011 Compare May 5, 2020 18:59
@odersky odersky marked this pull request as draft May 5, 2020 20:18
Encapsulate nesting level computation and make it more efficient.
@odersky odersky marked this pull request as ready for review May 7, 2020 09:35
@odersky odersky mentioned this pull request May 7, 2020
@odersky
Copy link
Contributor Author

odersky commented May 7, 2020

I think that's as far as I can go on it. One should dig deeper, to get a more complete understanding about this tricky subject matter. I opened #8900 so we don't forget this.

The immediate problem is important to fix and merge since it is a soundness hole introduced by type inference. The fix has the potential to invalidate some programs that passed before. In our code base, the final version that I implemented does pass all the test, but previous fixes did not. So we should get this in before we encounter code that exploits the loophole and is rejected by the fix.

odersky added a commit to dotty-staging/dotty that referenced this pull request May 7, 2020
Also, move `avoid` from TypeAssigner to TypeOps, since we
need to refer to it in Types.

Based on scala#8867
odersky added a commit to dotty-staging/dotty that referenced this pull request May 7, 2020
Also, move `avoid` from TypeAssigner to TypeOps, since we
need to refer to it in Types.

Based on scala#8867
def nestingLevel(using Context): Int =
@tailrec def recur(d: SymDenotation, n: Int): Int = d match
case d: ClassDenotation => d.nestingLevel + n // profit from the cache in ClassDenotation
case _ => recur(d.owner, n + 1)
Copy link
Member

Choose a reason for hiding this comment

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

The documentation of this method is inaccurate currently: NoSymbol.nestingLevel crashes because it has no owner:

Suggested change
case _ => recur(d.owner, n + 1)
case _ => if maybeOwner.exists then recur(maybeOwner, n + 1) else 0

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I thought it was preferable to change the comment instead. So, nestingLevel of root is 0, and it's undefined for NoSymbol. We don't need it for NoSymbol, and the code is simpler that way.

Copy link
Member

Choose a reason for hiding this comment

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

We don't need it for NoSymbol

In TypeVar#avoidCaptures we call ref.symbol.maybeOwner.nestingLevel, I think this will crash if ref happens to be a reference to a member of a structural type.

Copy link
Member

Choose a reason for hiding this comment

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

Also, ClassDenotation#nestingLevel does check if the owner exists, is that difference intentional?

Copy link
Member

Choose a reason for hiding this comment

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

Thinking about it more, the case of structural type member is interesting: it seems that their level should be the level of their underlying type, but then that means nestingLevel should be defined on Type

Copy link
Member

@smarter smarter May 9, 2020

Choose a reason for hiding this comment

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

Currently, TypeVar#avoidCaptures only looks for TermRefs, and I think these TermRefs can never be structural members because a reference to such a member is never a stable path. So I think the current implementation is OK, but it's something to watch out for if Typevar#avoidCaptures is extended to do more checks

Copy link
Contributor Author

@odersky odersky May 9, 2020

Choose a reason for hiding this comment

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

I fixed nestingLevel to work for NoDenotation as well. Structural type members would not have the form TermRef(NoPrefix, _), so we do not check their nestingLevel. It's true that we might also have to extend this to type members. That's part of #8900.

compiler/src/dotty/tools/dotc/core/Types.scala Outdated Show resolved Hide resolved
@odersky odersky merged commit b4338a8 into scala:master May 9, 2020
@odersky odersky deleted the fix-#8861 branch May 9, 2020 18:09
odersky added a commit to dotty-staging/dotty that referenced this pull request May 9, 2020
Also, move `avoid` from TypeAssigner to TypeOps, since we
need to refer to it in Types.

Based on scala#8867
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.

2 participants