Add type refinement for abstract type bindings

Author: nicolasstucki

compiler/src/dotty/tools/dotc/typer/Applications.scala

@@ -896,7 +896,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
      *  whereas overloaded variants need to have a conforming variant.
      */
     def trySelectUnapply(qual: untpd.Tree)(fallBack: Tree => Tree): Tree = {
-      // try first for non-overloaded, then for overloaded ocurrences
+      // try first for non-overloaded, then for overloaded occurrences
       def tryWithName(name: TermName)(fallBack: Tree => Tree)(implicit ctx: Context): Tree = {
         def tryWithProto(pt: Type)(implicit ctx: Context) = {
           val result = typedExpr(untpd.Select(qual, name), new UnapplyFunProto(pt, this))

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -1322,10 +1322,23 @@ class Typer extends Namer
         else {
           // for a singleton pattern like `x @ Nil`, `x` should get the type from the scrutinee
           // see tests/neg/i3200b.scala and SI-1503
-          val symTp =
+          val symTp0 =
             if (body1.tpe.isInstanceOf[TermRef]) pt1
             else body1.tpe.underlyingIfRepeated(isJava = false)
-          val sym = ctx.newPatternBoundSymbol(tree.name, symTp, tree.pos)
+
+          // If it is name based pattern matching, the type of the argument of the unapply is abstract and
+          // the return type has a type member `Refined`, then refine the type of the binding with the type of `Refined`.
+          val symTp1 = body1 match {
+            case Trees.UnApply(fun, _, _) if symTp0.typeSymbol.is(Deferred) =>
+              // TODO check that it is name based pattern matching
+              val resultType = fun.tpe.widen.finalResultType
+              val refined = resultType.select("Refined".toTypeName)
+              if (refined.exists) refined & symTp0
+              else symTp0
+            case _ => symTp0
+          }
+
+          val sym = ctx.newPatternBoundSymbol(tree.name, symTp1, tree.pos)
           if (ctx.mode.is(Mode.InPatternAlternative))
             ctx.error(i"Illegal variable ${sym.name} in pattern alternative", tree.pos)
           assignType(cpy.Bind(tree)(tree.name, body1), sym)

tests/run/refined-binding-nat.check

@@ -0,0 +1,6 @@
+Some((SuccClass(SuccClass(ZeroObject)),SuccClass(ZeroObject)))
+Some((ZeroObject,SuccClass(SuccClass(ZeroObject))))
+None
+Some((2,1))
+Some((0,2))
+None

tests/run/refined-binding-nat.scala

@@ -0,0 +1,118 @@
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    app(ClassNums)
+    app(IntNums)
+  }
+
+  def app(peano: Peano): Unit = {
+    import peano._
+    def divOpt(m: Nat, n: Nat): Option[(Nat, Nat)] = {
+      n match {
+        case Zero => None
+        case s @ Succ(_) => Some(safeDiv(m, s))
+      }
+    }
+    val two = Succ(Succ(Zero))
+    val five = Succ(Succ(Succ(two)))
+    println(divOpt(five, two))
+    println(divOpt(two, five))
+    println(divOpt(two, Zero))
+  }
+}
+
+trait Peano {
+  type Nat
+  type Zero <: Nat
+  type Succ <: Nat
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat)
+
+  implicit def succDeco(succ: Succ): SuccAPI
+  trait SuccAPI {
+    def pred: Nat
+  }
+
+  val Zero: Zero
+
+  val Succ: SuccExtractor
+  trait SuccExtractor {
+    def apply(nat: Nat): Succ
+    def unapply(nat: Nat): SuccOpt
+  }
+  trait SuccOpt {
+    type Refined = Succ
+    def isEmpty: Boolean
+    def get: Nat
+  }
+}
+
+object IntNums extends Peano {
+  type Nat  = Int
+  type Zero = Int
+  type Succ = Int
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat) = (m / n, m % n)
+
+  val Zero: Zero = 0
+
+  object Succ extends SuccExtractor {
+    def apply(nat: Nat): Succ = nat + 1
+    def unapply(nat: Nat): SuccOpt = new SuccOpt {
+      def isEmpty: Boolean = nat == 0
+      def get: Int = nat - 1
+    }
+  }
+
+  def succDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Nat = succ - 1
+  }
+}
+
+object ClassNums extends Peano {
+  trait NatTrait
+  object ZeroObject extends NatTrait {
+    override def toString: String = "ZeroObject"
+  }
+  case class SuccClass(predecessor: NatTrait) extends NatTrait with SuccOpt {
+    def isEmpty: Boolean = false
+    def get: NatTrait = this
+  }
+
+  object SuccNoMatch extends SuccOpt {
+    def isEmpty: Boolean = true
+    def get: NatTrait = throw new NoSuchElementException
+  }
+
+  type Nat  = NatTrait
+  type Zero = ZeroObject.type
+  type Succ = SuccClass
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat) = {
+    def intValue(x: Nat, acc: Int): Int = x match {
+      case nat: SuccClass => intValue(nat.predecessor, acc + 1)
+      case _ => acc
+    }
+    def natValue(x: Int): Nat =
+      if (x == 0) ZeroObject
+      else new SuccClass(natValue(x - 1))
+    val i = intValue(m, 0)
+    val j = intValue(n, 0)
+    (natValue(i / j), natValue(i % j))
+  }
+
+  val Zero: Zero = ZeroObject
+
+  object Succ extends SuccExtractor {
+    def apply(nat: Nat): Succ = new SuccClass(nat)
+    def unapply(nat: Nat): SuccOpt = nat match {
+      case nat: SuccClass => nat
+      case _ => SuccNoMatch
+    }
+  }
+
+  def succDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Nat = succ.predecessor
+  }
+
+}

tests/run/refined-binding.check

@@ -0,0 +1,2 @@
+ok
+9

tests/run/refined-binding.scala

@@ -0,0 +1,33 @@
+
+trait Foo {
+
+  type X
+  type Y <: X
+
+  def x: X
+
+  def f(y: Y) = println("ok")
+  object Z {
+    def unapply(arg: X): Opt = new Opt
+  }
+
+  class Opt {
+    type Refined = Y
+    def get: Int = 9
+    def isEmpty: Boolean = false
+  }
+}
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    test(new Foo { type X = Int; type Y = Int; def x: X = 1 })
+  }
+
+  def test(foo: Foo): Unit = {
+    foo.x match {
+      case x @ foo.Z(i) => // `x` is refined to type `Y`
+        foo.f(x)
+        println(i)
+    }
+  }
+}