In some cases it make sense to reuse a type constraint in both refinement and definition. E.g. the following definitions for Thing1 & Thing2 should be extensionally equivalent:
object TypeMixin {
trait Thing {
type TT
}
type ThingAux[T] = Thing { type TT = T }
object Thing1 extends Thing {
type TT = Int
}
object Thing2 extends Thing with ThingAux[Int]
}
Thing2 has less boilerplate, but won't be compiled properly:
TypeMixin.scala:16:36: com.tribbloids.spike.dotty.TypeMixin.Thing{TT = Int} is not a class type
one error found
My question is: what's the repercussion of allowing the type system to resolve Thing2? What's the counter-example for which this syntax will causes some unsound definition?