Dotty: Pattern matching doesn't infer type equalities between singletons.

Created on 7 Aug 2020  路  7Comments  路  Source: lampepfl/dotty

Minimized code

image

sealed trait ModelNode {
  type Result
}
sealed trait RealNode {
  final type Result = Double
}

def eval(m: ModelNode): m.Result = m match {
  case m1: RealNode =>
    implicitly[m.type =:= m1.type]
    0.0
}

Expectation

Should compile. Both 0.0 : m.Result and implicitly[m.type =:= m1.type].

bug

All 7 comments

image

Corrected version that still doesn't compile (extends ModelNode):

sealed trait ModelNode {
  type Result
}
sealed trait RealNode extends ModelNode {
  final type Result = Double
}

def eval(m: ModelNode): m.Result = m match {
  case m1: RealNode =>
    implicitly[m.type =:= m1.type]
    0.0
}

This is a known limitation. I don't know if @AleksanderBG plans to solve it at some point or not, but in the meantime you can write this more explicit evidence-propagating version:

  case m1: (RealNode & m.type) =>
    implicitly[m.type =:= m1.type]
    0.0: m1.Result

I'm planning to solve this specific issue, that is: patterns not being typed as intersection of their type and the singleton type of the scrutinee.

Adding arbitrary constraints to singleton types is a bit more problematic. There's no good way to do this in Dotty if I remember correctly - nullable types were going in a similar direction, but in the end they were implemented differently. I'll probably take a look at how exactly they were implemented and if it's possible to generalise that implementation to arbitrary constraints, but I cannot promise anything.

Looks related to #8413.

@abgruszecki

I'm planning to solve this specific issue, that is: patterns not being typed as intersection of their type and the singleton type of the scrutinee.

Note that this was not enough to fix this specific issue. I also had to add the type ascription in 0.0: m1.Result.

Ah, right, so it's primarily about putting constraints on type members. Other than constraining singleton types, I don't think there's a principled way of doing that. @alexknvl since you say this is a minimised issue, is there a source project? If it's something important that worked in Scala 2, I can try to figure out whether there's something I can do.

@allanrenucci thanks for finding that issue! I wanted to look for it and you saved me the effort :)

@abgruszecki It was an experiment in our internal code base at work (no public source code available). It doesn't work in Scala 2 either. I was trying to figure out some replacement for GADTs as they don't work well with serialization / deserialization typeclass derivation (e.g. using Magnolia).

Was this page helpful?
0 / 5 - 0 ratings