Skip to content

[Draft] A more dependent pattern matching prototype #21828

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

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

noti0na1
Copy link
Member

Sometime, it is useful to track the dependency between the selector and the pattern-bind variable.

case class A(x: String)

def test(a: A) = a match
  case b @ A(y) => ???

Given the example, in the body of the case, we should be able to tell:

  • a and b are the same reference;
  • a.x, b.x and y are same as well.

This PR made following modifications:

  • For a case class and ith parameter x: T, if x is not a var, generate def _i: this.x = this.x, instead of def _i: T = this.x.
  • The default unapply for a case class A becomes def unapply(a: A): a.type = a.
  • Do not widen stable TermRefs when typing patterns. If pt is a singleton type, we use intersection to add pt to the new pattern-bind variable.

With this PR, the following code can be type checked:

trait A:
  val x: Int
  type T

case class B(x: Int, y: Int) extends A:
  type T = String
  val z: T = "B"

case class C(x: Int) extends A:
  type T = Int
  val z: T = 1

object BParts:
  def unapply(b: B): Option[(b.x.type, b.y.type)] = Some((b.x, b.y))

def test1(a: A) = a match
  case b @ B(x, y) =>
    // b: a.type & B
    // x: (a.type & B).x.type
    // y: (a.type & B).y.type
    val e1: a.type = b
    val e2: a.x.type = b.x
    val e3: a.x.type = x
    val e4: b.x.type = x
    x + y
  case C(x) =>
    val e1: a.x.type = x
    x
  case BParts(x, y) =>
    val e1: a.x.type = x
    x + y
  case _ => 0

def test2(a: A): a.T =
  a match
    case b: B =>
      // b: a.type & B
      // b.z: b.T = (a & B)#T = a.T & String
      b.z
    case c: C => c.z

def test3(a: A): a.T =
  a match
    case b: B =>
      // b: a.type & B; hence b.T <:< a.T & String
      // We don't have a: b.type in the body,
      // so we can't prove String <:< a.T
      val x: b.T = b.z + ""
      x
    case c: C =>
      val x: c.T = c.z + 0
      x

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.

1 participant