Refinements on types declared by member vals - possible?

I really would like if something like this was possible:

trait Ref[T] {
  type Loaded <: Boolean with Singleton
  def get :T

trait Entity {
  val other :Ref[Entity]

trait EntityStore {
  def load :Entity
  def loadWithOther :Entity { type other.Loaded = true }

  def get[X](smth :Entity { type other.Loaded = true }) :T = smth.other.get

Is there a good argument why it should not? Would that be a big change to the compiler / language semantics? Now, of course, with every language feature, the onus of proving usefulness lies with the proposer of the change, but I think the above example illustrates one good use, and it is a very simple one. It considerably increases the expressiveness of the language and I think people would could really go to town with it. While the example above could be made by declaring an OtherLoaded type in Entity and make it a ‘master’ declaration, it moves the effort from the library to the user which, at least in this example, in my opinion makes it impractical. As written, the extra code is limited to the library and the use site, so extra ‘dynamic’ type safety is almost free.

You can already do this but without your proposed “lens” syntax.

trait EntityStore {
  def load: Entity
  def loadWithOther: Entity { val other: Ref[Entity]{ type Loaded = true }}

  def get[X](smth: Entity { val other: Ref[Entity]{ type Loaded = true }}): Entity = smth.other.get

Of course. Awesome!!! :slight_smile: Thank you.