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

Unsound reduction of match types #19746

Closed
EugeneFlesselle opened this issue Feb 20, 2024 · 2 comments · Fixed by #20015
Closed

Unsound reduction of match types #19746

EugeneFlesselle opened this issue Feb 20, 2024 · 2 comments · Fixed by #20015
Assignees
Labels
area:match-types itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException)
Milestone

Comments

@EugeneFlesselle
Copy link
Contributor

Compiler version

3.4.2-RC1

Minimized example

trait V:
  type X = this.type match
    case W[x] => x

trait W[+Y] extends V

extension (self: Any) def as[T]: T =
  def asX(w: W[Any]): w.X /* <- reduces to Any */ = self
  asX(new W[T] {}) /* <- reduces to T */

0.as[Boolean] // java.lang.ClassCastException

The issue is that w.X reduces to Any because the scrutinee w is widened to W[Any] before attempting the reduction of the match type.

@EugeneFlesselle EugeneFlesselle added stat:needs triage Every issue needs to have an "area" and "itype" label area:match-types itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException) and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Feb 20, 2024
@EugeneFlesselle
Copy link
Contributor Author

Interestingly, this kind of issue is already detected when using an intermediate type parameter for w.

extension (self: Any) def as[T]: T =
    def asX[W1 <: W[Any]](w: W1): w.X /* <- does not reduce to Any */ = self
    asX(new W[T] {}) /* <- reduces to T */

In this case, we rightfully find that the scrutinee is not specific enough to determine an instance for the capture in W[x].

Also note that the this.type is not fundamentally necessary for the issue to arise. It just so happens that doing something like X[w.type] instead of w.X avoids the problem due to some unrelated issue with caching.

@sjrd sjrd self-assigned this Feb 20, 2024
@sjrd
Copy link
Member

sjrd commented Feb 20, 2024

@Gedochao Probably a candidate P0, as unsoundness issues are pretty bad.

sjrd added a commit to sjrd/dotty that referenced this issue Mar 25, 2024
Term refs that reference term parameters can be substituted later
by more precise ones, which can lead to different instantiations
of type captures. They must therefore be considered as non concrete
when following `baseType`s to captures in variant positions, like
we do for type param refs and other substitutable references.

We actually rewrite `isConcrete` in the process to be more based
on an "allow list" of things we know to be concrete, rather than
an "exclusion list" of things we know to be non-concrete. That
should make it more straightforward to evaluate the validity of
the algorithm.
@sjrd sjrd linked a pull request Mar 25, 2024 that will close this issue
sjrd added a commit that referenced this issue Apr 4, 2024
Term refs that reference term parameters can be substituted later by
more precise ones, which can lead to different instantiations of type
captures. They must therefore be considered as non concrete when
following `baseType`s to captures in variant positions, like we do for
type param refs and other substitutable references.

We actually rewrite `isConcrete` in the process to be more based on an
"allow list" of things we know to be concrete, rather than an "exclusion
list" of things we know to be non-concrete. That should make it more
straightforward to evaluate the validity of the algorithm.
@Kordyjan Kordyjan added this to the 3.5.0 milestone May 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:match-types itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants