Add type refinement for abstract type bindings

Author: nicolasstucki

compiler/src/dotty/tools/dotc/core/StdNames.scala

@@ -488,6 +488,7 @@ object StdNames {
     val productPrefix: N        = "productPrefix"
     val raw_ : N                = "raw"
     val readResolve: N          = "readResolve"
+    val refinedScrutinee: N     = "refinedScrutinee"
     val reflect : N             = "reflect"
     val reflectiveSelectable: N = "reflectiveSelectable"
     val reify : N               = "reify"

compiler/src/dotty/tools/dotc/transform/FirstTransform.scala

@@ -108,7 +108,29 @@ class FirstTransform extends MiniPhase with InfoTransformer { thisPhase =>
     cpy.Template(impl)(self = EmptyValDef)
   }
 
-  override def transformDefDef(ddef: DefDef)(implicit ctx: Context) = {
+  override def transformDefDef(ddef: DefDef)(implicit ctx: Context): Tree = {
+    if (ddef.name == nme.unapply && !ddef.symbol.is(Synthetic)) {
+      val resultType = ddef.tpt.tpe.finalResultType
+//      println("Checking: ")
+//      println(ddef.show)
+//      println()
+//      println()
+//      println()
+//      val refined = resultType.select(tpnme.UncheckedRefinedArgument)
+//      if (refined.typeSymbol.exists) {
+//        val arg = ddef.vparamss.head.head
+//        if (!(refined <:< arg.tpt.tpe)) {
+//          ctx.error(i"Abstract type refinement $refined (${refined.widenDealias}) is not a subtype of the unapply argument (${arg.tpt.tpe.widenDealias})", ddef.pos)
+//        } else if (!(refined <:< arg.tpe)) {
+//          ctx.warning(
+//            i"""Abstract type refinement $refined (${refined.widenDealias}) should be a subtype of the unapply argument singleton type(${arg.name}.type).
+//               |
+//               |This type constraint can be added as follows:
+//               |  def unapply(x: T): U { type ${tpnme.UncheckedRefinedArgument} <: x.type } = ...
+//             """.stripMargin, ddef.pos)
+//        }
+//      }
+    }
     if (ddef.symbol.hasAnnotation(defn.NativeAnnot)) {
       ddef.symbol.resetFlag(Deferred)
       DefDef(ddef.symbol.asTerm,

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

@@ -1323,10 +1323,29 @@ 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
+              fun.tpe.widen match {
+                case mt: MethodType =>
+                  val resultType = mt.resType.substParam(mt.paramRefs.head, symTp0)
+                  val refinedType = resultType.select(nme.refinedScrutinee).widen.resultType
+                  if (refinedType.exists) refinedType
+                  else symTp0
+                case _ =>
+                  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-safe-upper-bound.check

@@ -0,0 +1,123 @@
+
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    app(ClassNums)
+    app(IntNums)
+  }
+
+  def app(peano: Peano): Unit = {
+    import peano._
+    // FIXME
+//    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 { type UncheckedRefinedArgument <: nat.type }
+  }
+  trait SuccOpt {
+    type UncheckedRefinedArgument <: 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) = new SuccOpt {
+      type UncheckedRefinedArgument = nat.type
+      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 {
+    type UncheckedRefinedArgument = this.type
+    def isEmpty: Boolean = false
+    def get: NatTrait = this
+  }
+
+  object SuccNoMatch extends SuccOpt {
+    type UncheckedRefinedArgument = Nothing
+    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) = nat match {
+      case nat: (SuccClass & nat.type) => nat
+      case _ => SuccNoMatch
+    }
+  }
+
+  def succDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Nat = succ.predecessor
+  }
+
+}

tests/run/refined-binding-nat-safe-upper-bound.scala

@@ -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.check

@@ -0,0 +1,125 @@
+
+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 Scrutinee <: Singleton
+    def isEmpty: Boolean
+    def refinedScrutinee: Succ & Scrutinee
+    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 {
+      type Scrutinee = nat.type
+      def isEmpty: Boolean = nat == 0
+      def refinedScrutinee: Succ & Scrutinee = nat
+      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 {
+    type Scrutinee = this.type
+    def isEmpty: Boolean = false
+    def refinedScrutinee: this.type = this
+    def get: NatTrait = this
+  }
+
+  object SuccNoMatch extends SuccOpt {
+    type Scrutinee = Nothing
+    def isEmpty: Boolean = true
+    def refinedScrutinee: Nothing = throw new NoSuchElementException
+    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-nat.scala

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

tests/run/refined-binding.check

@@ -0,0 +1,38 @@
+
+sealed trait Foo {
+
+  type X
+  type Y <: X
+
+  def x: X
+
+  def f(y: Y) = println("ok")
+
+  object Z {
+    def unapply(arg: X) = new Opt {
+      type Scrutinee = arg.type
+      def refinedScrutinee: Y & Scrutinee = arg.asInstanceOf[Y & Scrutinee]
+    }
+  }
+
+  abstract class Opt {
+    type Scrutinee <: Singleton
+    def refinedScrutinee: Y & Scrutinee
+    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)
+    }
+  }
+}