-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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 capture checking of dependent functions #16264
Conversation
After the fix of the soundness issue, sometimes we infer universal capabilities where it is not necessary. This results in completeness issues.
5992fdf
to
7e695fd
Compare
For an idempotent map f and a set C, we do not need to propagate x ∈ f(C) back to C when x comes from f(y) for some y ∈ C.
So that TypeComparer can propagate the capture sets correctly.
Given an applied function `f[cs A](g)`, where the type of `f` is `[T] -> (x: {*} C) -> T` and the type of `g` is dependent, e.g. `(x: {*} Cap) -> {x} A`, the reference `x` may be propagate to cs. But this makes `cs A` ill-formed since it is not allowed to mention `{x}`. This sometimes cause soundness problems. We heal this by pushing the capture set of `{x}` into cs.
- remove limitation errors - update check files
2b28cd6
to
1afbf74
Compare
5e3bc15
to
d2dee4c
Compare
d2dee4c
to
80830e3
Compare
MethodType.companion(isContextual = isContextual, isErased = isErased)(args, resultType) | ||
.toFunctionType(isJava = false, alwaysDependent = true) | ||
|
||
private def makeFunctionDependent(expected: Type, actual: Type)(using Context): Type = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe rename: alignDependentFunction?
healCaptureSet(refs) | ||
// mapOver(tp) | ||
traverseChildren(parent) | ||
case tp @ RefinedType(parent, rname, rinfo: MethodType) => |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Need to also consider parent for RefinedTypes that are not function types.
val localParams: List[TermParamRef] = tp.paramRefs | ||
val saved = allowed | ||
try | ||
localParams foreach { x => allowed = allowed + x } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe: tp.paramRefs.foreach(allowed += _)
case ref: TermParamRef => allowed.contains(ref) | ||
case _ => true | ||
|
||
private def widenParamRefs(refs: List[TermParamRef]): List[CaptureSet] = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consider adding a doc comment what it does
todos match | ||
case Nil => acc | ||
case ref :: rem => | ||
val cs = ref.binder.paramInfos(ref.paramNum).captureSet |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think ref.paramInfo
would work here as well.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
or maybe ref.captureSetOfInfo
.
// Both kinds will be detected in other places and tend to | ||
// give better error messages. | ||
// | ||
// The two kinds of errors are: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This second condition I am not sure about.
// - Failing to include a capture reference in a capture set. | ||
// This is mostly due to the restriction placed by explicit type annotations, | ||
// and should already be reported as a type mismatch during `checkConforms`. | ||
cs1.subCaptures(cs, frozen = false) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
checkSubSet(cs1, cs, tree.srcPos) or something like that.
bb871df
to
c4240fb
Compare
Fixes #15921.
Capture checking can be unsound for dependent functions. Minimized example:
In the above example, we issue an error for
g
, but not forf
, which is unsound.The root cause of this issue is that in the
Typer
phase, we only createInferredTypeTree
for the result type of function values when the expected type of the function literal is non-dependent; and later duringSetup
of the capture checking phase, we only create capture set variables and update the information of function symbols when its result type tree is anInferredTypeTree
.To be more specific, the function literal
io => () => io.use()
in bothf
andg
would be expaneded into the following tree inTyper
:For
g
, where the expected type of the function literal is non-dependent, we would create capture set variables inSetup
for the return type{} () -> Unit
and update the symbol info of the outer$anonfun
. Forf
, we would not do these things because{} () -> Unit
is not anInferredTypeTree
.This PR fixes this issue by typing the
DependentTypeTree
as anInferredTypeTree
in the typer.Currently, although this PR fixes the soundness problem, it brings completeness issues, where sometimes we propagate the universal capability to some capture sets incorrectly, which prevents some positive test cases from being accepted. I am still investigating this issue and thus mark this PR as a draft for now.The completeness problem is fixed by two additional refinements: