Allow refinements that refine already refined types.

Previously, a double definition errorfor `T` was produced in a case like this:

     type T1 = C { T <: A }
     type T2 = T1 { T <: B }

This was caused by the way T1 was treated in the refinement class
that is used to typecheck the type. Desugaring of T2 with `refinedTypeToClass`
would give

     trait <refinement> extends T1 { type T <: B }

and `normalizeToClassRefs` would transform this to:

     trait <refinement> extends C { type T <: A; type T <: B }

Hence the double definition. The new scheme desugars the rhs of `T2` to:

     trait <refinement> extends C { this: T1 => type T <: B }

which avoids the problem.

Also, added tests that #232 (fix/boundsPropagation) indeed considers all refinements
together when comparing refined types.

Author: odersky

src/dotty/tools/dotc/ast/Desugar.scala

@@ -834,17 +834,45 @@ object desugar {
     }
   }.withPos(tree.pos)
 
-  /** Create a class definition with the same info as this refined type.
+  /** Create a class definition with the same info as the refined type given by `parent`
+   *  and `refinements`.
+   *
    *      parent { refinements }
    *  ==>
-   *      trait <refinement> extends parent { refinements }
+   *      trait <refinement> extends core { this: self => refinements }
+   *
+   *  Here, `core` is the (possibly parameterized) class part of `parent`.
+   *  If `parent` is the same as `core`, self is empty. Otherwise `self` is `parent`.
+   *
+   *  Example: Given
+   *
+   *      class C
+   *      type T1 extends C { type T <: A }
+   *
+   *  the refined type
    *
-   *  If the parent is missing, Object is assumed.
-   *  The result is used for validity checking, is thrown away afterwards.
+   *      T1 { type T <: B }
+   *
+   *  is expanded to
+   *
+   *      trait <refinement> extends C { this: T1 => type T <: A }
+   *
+   *  The result of this method is used for validity checking, is thrown away afterwards.
+   *  @param parentType   The type of `parent`
    */
-  def refinedTypeToClass(tree: RefinedTypeTree)(implicit ctx: Context): TypeDef = {
-    val parent = if (tree.tpt.isEmpty) TypeTree(defn.ObjectType) else tree.tpt
-    val impl = Template(emptyConstructor, parent :: Nil, EmptyValDef, tree.refinements)
+  def refinedTypeToClass(parent: tpd.Tree, refinements: List[Tree])(implicit ctx: Context): TypeDef = {
+    def stripToCore(tp: Type): Type = tp match {
+      case tp: RefinedType if tp.argInfos.nonEmpty => tp // parameterized class type
+      case tp: TypeRef if tp.symbol.isClass => tp        // monomorphic class type
+      case tp: TypeProxy => stripToCore(tp.underlying)
+      case _ => defn.AnyType
+    }
+    val parentCore = stripToCore(parent.tpe)
+    val untpdParent = TypedSplice(parent)
+    val (classParent, self) =
+      if (parent.tpe eq parentCore) (untpdParent, EmptyValDef)
+      else (TypeTree(parentCore), ValDef(nme.WILDCARD, untpdParent, EmptyTree))
+    val impl = Template(emptyConstructor, classParent :: Nil, self, refinements)
     TypeDef(tpnme.REFINE_CLASS, impl).withFlags(Trait)
   }
 

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

@@ -756,7 +756,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
 
   def typedRefinedTypeTree(tree: untpd.RefinedTypeTree)(implicit ctx: Context): RefinedTypeTree = track("typedRefinedTypeTree") {
     val tpt1 = if (tree.tpt.isEmpty) TypeTree(defn.ObjectType) else typedAheadType(tree.tpt)
-    val refineClsDef = desugar.refinedTypeToClass(tree)
+    val refineClsDef = desugar.refinedTypeToClass(tpt1, tree.refinements)
     val refineCls = createSymbol(refineClsDef).asClass
     val TypeDef(_, Template(_, _, _, refinements1)) = typed(refineClsDef)
     assert(tree.refinements.length == refinements1.length, s"${tree.refinements} != $refinements1")

test/dotc/tests.scala

@@ -106,6 +106,7 @@ class tests extends CompilerTest {
   @Test def neg_t1569_failedAvoid = compileFile(negDir, "t1569-failedAvoid", xerrors = 1)
   @Test def neg_cycles = compileFile(negDir, "cycles", xerrors = 8)
   @Test def neg_boundspropagation = compileFile(negDir, "boundspropagation", xerrors = 4)
+  @Test def neg_refinedSubtyping = compileFile(negDir, "refinedSubtyping", xerrors = 2)
 
   @Test def dotc = compileDir(dotcDir + "tools/dotc", twice)(allowDeepSubtypes)
   @Test def dotc_ast = compileDir(dotcDir + "tools/dotc/ast", twice)

tests/neg/refinedSubtyping.scala

@@ -0,0 +1,23 @@
+// tests that a refinement subtype satisfies all constraint
+// of its refinemen supertype
+class Test3 {
+
+  trait A
+  trait B
+
+  class C { type T }
+
+  type T1 = C { type T <: A }
+  type T2 = T1 { type T <: B }
+
+  type U1 = C { type T <: B }
+  type U2 = C { type T <: A }
+
+  var x: T2 = _
+  val y1: U1 = ???
+  val y2: U2 = ???
+
+  x = y1 // error
+  x = y2 // error
+
+}

tests/pos/refinedSubtyping.scala

@@ -17,3 +17,46 @@ class Test {
   y = x
 
 }
+
+class Test2 {
+
+  trait A
+  trait B
+
+  class C { type T }
+
+  type T1 = C { type T <: A } { type T <: B }
+
+  type U1 = C { type T <: B } { type T <: A }
+
+  var x: T1 = _
+  var y: U1 = _
+
+  x = y
+  y = x
+}
+
+
+class Test3 {
+
+  trait A
+  trait B
+
+  class C { type T }
+
+  type T1 = C { type T <: A }
+  type T2 = T1 { type T <: B }
+
+  type U1 = C { type T <: B }
+  type U2 = U1 { type T <: A }
+
+  var x: T2 = _
+  var y: U2 = _
+
+  val x1 = x
+  val y1 = y
+
+  x = y
+  y = x
+
+}