Does Dotty support refinements?

I am reading in dread what will come with Scala 3, paying particular attention to changes to compound types. They were always somewhat of a hack, so clean, true intersection types are certainly an improvement. I couldn't find though anything about what happens to the actual refinement part of the compound type. I rely heavily in my current project on strongly interwoven types in an attempt to have every returned value be as narrow as possible. So, for example, having

trait Thing { thisThing =>
    type A
    type B
    type C

    def something :Thing { 
        type A = <related to thisThing.A> 
        type B <: <related to thisThing.B>
        type C = <etc>
    }

Is it even still possible? How to achieve this goal with the new semantics? As I understand, refinements of abstract types will almost certainly be not allowed, so it will be difficult to have a 'self type' declaration in a root of a type hierarchy:

trait Thing {
    type ThisThing <: Thing
    type A
    type B
    def copy(...) :ThisThing { type A = ...; type B = ... }
}

On a somewhat related note, I was looking at structural types. I must say I like how we can dynamic member selection/implementation with static declarations. Is it though possible for abstract classes? Could I write something like:

trait Record(members :(String, Any)*) extends Selectable { ... }

val r = new Record { val name :String; val age :Int }

EDIT: I found the relative bit of documentation and it looks like anonymous Selectable instance are exempt from the rule that the type of an anonymous class is the intersection of its extended types - good.

Solution

As I understand, refinements of abstract types will almost certainly be not allowed...

type A <: {
  type U
}

trait B {
  type T <: A
}

object o extends B {
  type T = A { type U = Int }
}

perfectly compiles.

https://scastie.scala-lang.org/Nbz3GxoaTSe3VhXZz406vQ

What is not allowed is type projections of abstract types T#U

trait B {
  type T <: A
  type V = T#U // B.this.T is not a legal path since it is not a concrete type
}

https://scastie.scala-lang.org/xPylqOOkTPK9CvWyDdLvsA

http://dotty.epfl.ch/docs/reference/dropped-features/type-projection.html

Maybe you meant that

type A {
  type U
}

is not parseable. But in Scala 2 it isn't either. Correct is either

trait A {
  type U
}

type A <: {
  type U
}