Skip to content

"Ill-scoped" type variables can be bound in patterns #16952

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

Open
howtonotwin opened this issue Feb 17, 2023 · 2 comments
Open

"Ill-scoped" type variables can be bound in patterns #16952

howtonotwin opened this issue Feb 17, 2023 · 2 comments
Labels
area:typer itype:bug itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException)

Comments

@howtonotwin
Copy link

Compiler version

Dotty 3.2.2 on Scastie as well as Dotty 3.3.0-RC3 locally. Seems to exist from Scala 2.

Minimized code

class T[A]
val x: T[T[_]] = new T[T[_]]
def f(): Unit = x match {
  case y: T[T[a]] => ()
}

Output

Compiles.

Expectation

Type error at the pattern y: T[T[a]], which should not be allowed in a match on a value of type T[T[_]]. Conceptually, the pattern just doesn't make sense. (What is a supposed to be binding? It's clear for x: T[_], but not for x: T[T[_]].) In a less minimal case of the same kind of pattern, there is an unsoundness:

case class PEndo[X](x: X, f: X => X) {
  def next: X = f(x)
}
case class Pair[X](x: X, y: X)

val p = Pair[PEndo[_]](PEndo[String]("42", x => x + x), PEndo[Int](42, x => x + x))
// p: Pair[PEndo[_]], which means each element of the pair may have a different element type ("X")
val ohno: PEndo[_] = p match {
  case p: Pair[PEndo[a]] => PEndo(p.x.x, p.x.f andThen p.y.f)
  // but I'm allowed to pretend they have the _same_ X and bind that (nonexistent) type to a name (a)!
}
@main def main(): Unit = println(ohno.next)

This case gives a ClassCastException at runtime, since the bad pattern is not stopped at compile-time.

@howtonotwin howtonotwin added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Feb 17, 2023
@smarter smarter added area:typer 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 19, 2023
@smarter
Copy link
Member

smarter commented Feb 20, 2023

This looks similar to #15578 /cc @abgruszecki

@Kordyjan Kordyjan added this to the 3.3.0 backports milestone Feb 20, 2023
@abgruszecki
Copy link
Contributor

abgruszecki commented Feb 20, 2023

Well, looking at that issue (#15578), it seems we should have picked option 3. instead of 4, i.e. disallowing pat-mat from naming type arguments which are not top-level and do not correspond to a path in cDOT.

@Kordyjan Kordyjan modified the milestones: 3.3.0 backports, 3.4.0 Feb 27, 2023
@dwijnand dwijnand removed this from the 3.4.0 milestone Dec 11, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:typer itype:bug itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException)
Projects
None yet
Development

No branches or pull requests

5 participants