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

Canonicalize capture variable subtype comparisons #22289

Closed
wants to merge 1 commit into from

Conversation

bracevac
Copy link
Contributor

@bracevac bracevac commented Jan 1, 2025

Fixes #22103

Subtype problems where at least one side is a type variable representing a capture variable are canonicalized to capturing type comparisons on the special CapSet for the universe of capture sets. For example, C <: CapSet^{C^} becomes CapSet^{C^} <: CapSet^{C^}, and A <: B becomes CapSet^{A^} <: CapSet^{B^} if both A and B are capture variables.

Supersedes #22183. This solution is overall cleaner and does not require adding a new bit to the TypeComparer's ApproxState.

Fixes scala#22103

Subtype problems where at least one side is a type variable
representing a capture variable are canonicalized to
capturing type comparisons on the special `CapSet` for the
universe capture sets. For example, `C <: CapSet^{C^}`
becomes `CapSet^{C^} <: CapSet^{C^}`, and `A <: B` becomes
`CapSet^{A^} <: CapSet^{B^}` if both `A` and `B` are capture
variables.
val c3: C = d_e_f1 // error
val c4: C = f1 // error
val e4: E = f1 // error
val e5: E = d1 // error
Copy link
Contributor Author

Choose a reason for hiding this comment

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

This should fail but currently doesn't. We now canonicalize the subtype test D <: E (fails) to CapSet^{D^} <: CapSet^{E^} (succeeds). It appears the subcapturing implementation does not handle this correctly.

@odersky
Copy link
Contributor

odersky commented Jan 2, 2025

Can you push this to dotty-staging? Then we can collaborate to maybe fix the problem with the failing test.

@Linyxus
Copy link
Contributor

Linyxus commented Jan 2, 2025

I think the problem of the failing test is with CaptureSet.ofType: if tp is a type (param) ref an empty set is always returned, which now shall not be the case for capvars.

And if we handle this correctly, it should also be possible to write things like

def f[C^, D^, E <: C | D](...) = ...

which means that E is upper bounded by {C^, D^}.

or:

def f[C^, D^, E <: C & D](...) = ...

which means that E should be upper bounded by the glb of C and D ...

@bracevac
Copy link
Contributor Author

bracevac commented Jan 2, 2025

@Linyxus exactly! That will be the next step.

@bracevac
Copy link
Contributor Author

bracevac commented Jan 2, 2025

The continuation: #22299

@bracevac bracevac closed this Jan 2, 2025
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.

Improve Subtyping and Normalization of Capture Sets
3 participants