Skip to content

Fix #25830: explicify inferred capture-polymorphic lambda types#25939

Open
bracevac wants to merge 5 commits intoscala:mainfrom
dotty-staging:ob/fix-25830-v3
Open

Fix #25830: explicify inferred capture-polymorphic lambda types#25939
bracevac wants to merge 5 commits intoscala:mainfrom
dotty-staging:ob/fix-25830-v3

Conversation

@bracevac
Copy link
Copy Markdown
Contributor

Fixes #25830

PostTyper's CleanupRetains ran on every inferred lambda type and stripped all @retains annotations, so a poly-fn literal like { [C^] => (xs: List[File^{C}]) => xs } lost its {C} and could no longer be applied capture-polymorphically.

Instead of trying to make CleanupRetains preserve the right retains, we now "explicify" the freshly inferred type before cleaning it: walk the lambda's poly-/method-/function-type chain and only apply CleanupRetains to the innermost result, preserving outer parameter types and binder bounds verbatim. Then flip the tpt to a non-inferred TypeTree so that Setup processes it via transformExplicitType (which respects user- written retains) rather than mapInferred (which drops them).

The same treatment has to recurse into the synthesized $anonfun DefDefs that appear in curried lambdas: their result tpts are still inferred and would otherwise have ys's {C} dropped. We collect those sub-anonfun symbols when we detect a capset poly-fn literal at a val/def RHS and apply the same explicify on their tpts as PostTyper traverses.

This also permits a much broader class of capture-polymorphic lambdas than the previous restriction-based approach: literals whose retains mention enclosing capabilities (e.g. {C, external}), bounded capset binders, curried params, defs, and lambdas nested inside other lambdas all compile, since the user-written param types are kept as-is.

How much have you relied on LLM-based tools in this contribution?

Extensively, for good health and prosperity.

How was the solution tested?

New automated tests (including the issue's reproducer, if applicable)

@bracevac
Copy link
Copy Markdown
Contributor Author

@odersky it's ready. The new approach is a lot simpler and permits more lambdas. The CI failure about scaladoc is unrelated to this PR.

@bracevac
Copy link
Copy Markdown
Contributor Author

I also briefly looked at dependent lambdas (c : Cap) => (f: File^{c.C}) => ... but these would need more work...

PostTyper's CleanupRetains ran on every inferred lambda type and stripped
all `@retains` annotations, so a poly-fn literal like
`{ [C^] => (xs: List[File^{C}]) => xs }` lost its `{C}` and could no longer
be applied capture-polymorphically.

Instead of trying to make CleanupRetains preserve the right retains, we
now "explicify" the freshly inferred type before cleaning it: walk the
lambda's poly-/method-/function-type chain and only apply CleanupRetains
to the innermost result, preserving outer parameter types and binder
bounds verbatim. Then flip the tpt to a non-inferred TypeTree so that
Setup processes it via `transformExplicitType` (which respects user-
written retains) rather than `mapInferred` (which drops them).

The same treatment has to recurse into the synthesized `$anonfun`
DefDefs that appear in curried lambdas: their result tpts are still
inferred and would otherwise have ys's `{C}` dropped. We collect those
sub-anonfun symbols when we detect a capset poly-fn literal at a val/def
RHS and apply the same explicify on their tpts as PostTyper traverses.

This also permits a much broader class of capture-polymorphic lambdas
than the previous restriction-based approach: literals whose retains
mention enclosing capabilities (e.g. `{C, external}`), bounded capset
binders, curried params, defs, and lambdas nested inside other lambdas
all compile, since the user-written param types are kept as-is.
Confirms that explicify and the lambda-detection predicate handle
PolyTypes whose capset binders are interleaved with non-capset type
parameters, e.g. `[C^, A]`, `[A, C^]`, and `[A, C^, B, D^]`.
`isCapsetPolyFunLiteralRhs` previously bailed out when the outermost
closure was a `PolyType` whose paramRefs contained no capset binders,
even though a curried inner closure further in the chain might still
introduce one — e.g. `[A] => zs => [C^] => xs => …`. As a result, the
val/def's tpt skipped explicify, the inner `{C}` was lost in Setup's
`mapInferred`, and the lambda could not be applied capture-polymorphically.

Now we recurse into `dd.rhs` whenever the current closure's PolyType
lacks capset binders, mirroring the behaviour for non-PolyType infos.

Add tests for multiple capset binder blocks separated by term-parameter
lists, covering both leading-capset and trailing-capset orderings as
well as inner blocks that reference earlier capset binders.
Replace the leaf CleanupRetains in Explicify.explicify with sanitizeLeaf,
which only scrubs typer placeholder retains (e.g. retain[TypeBounds(...)])
and keeps user-written capability references intact. Mixed retain args
are filtered sub-part-wise so the user-meaningful pieces survive.

Without this, an identity poly-fn `[C^] => (x: File^{C}) => x` had stored
result type `File^{}`, and `id[{a}](a)` could be assigned to a strict
pure bound — unsound.
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.

CC: Type inference for capture-polymorphic lambdas is broken

2 participants