Enum Value singleton fails to reduce in match type

[bishabosha]

Minimised Code

enum Bool {
  case True
  case False
}

import Bool._

type Not[B <: Bool] = B match {
  case True.type => False.type
  case False.type => True.type  
}

val f: Not[False.type] = True

Output

13 |val f: Not[False.type] = True
   |                         ^^^^
   |                         Found:    (Bool.True : Bool)
   |                         Required: Not[(Bool.False : Bool)]

Expectation

if I replace enum Bool with a sealed trait and case objects then the code compiles:

+sealed trait Bool
+object Bool {
+  case object True extends Bool
+  case object False extends Bool
-enum Bool {
-  case True
-  case False
 }
...

Originally posted by @bishabosha in #10510 (comment)

[OlivierBlanvillain]

if I replace enum Bool with a sealed trait and case objects then the code compiles:

That's not very surprizing given that this enum doesn't create new types for its cases, just vals.

The question here is what's the meaning of the patterns in the following example:?

def not[B <: Bool](b: B) = b match {
  case _: True.type => False.type
  case _: False.type => True.type  
}

Given that True and False are vals, _: True.type and _: False.type desugar to calls to ==, which we know nothing at compile time, so there is nothing we can do on the match type side.

[OlivierBlanvillain]

I think this is another example that shows that users don't read the enum spec and are surprised by the differences between case True() and case True in an enum. In my opinion it would be better to desugar case True to a case object, but we already had this discussion before.

[bishabosha]

@OlivierBlanvillain matching on singleton types becomes a test on identity with eq, not with ==, so that is disjoint in the case of enum values

[OlivierBlanvillain]

Yes my bad, but in the general case there is no way to statically conclude that a.eq(b) evaluates to false for two vals a and b since they could point to the same object. By the time the Not match type is reduced, the Bool enum is indistinguishable from the following:

sealed trait Bool
object Bool {
  val True = new Bool
  val False = True
}

[bishabosha]

@OlivierBlanvillain all symbols of enum value definitions will also have the EnumValue flag, is it possible to check for that? (i guess then they would have to be distinguished by name in case one is a cloned symbol)

[odersky]

@OlivierBlanvillain @bishabosha Not sure where we are with this. Is there a concrete action item? if not please close.

[OlivierBlanvillain]

Even if what @bishabosha suggests is technically feasible, I think that it would a deviation from the current design of enums and match types. An enum defines values, not types, so from an ideological standpoint, users interested in doing type-level programming should defines their types using traits and classes, not enums.

[bishabosha]

An enum defines values, not types, so from an ideological standpoint, users interested in doing type-level programming should defines their types using traits and classes, not enums.

I am confused about this point, all val definitions define a type: their singleton type.

we already have a case in the Inliner to support treating enum values as defining a unique type, used in inline match:
https://github.com/lampepfl/dotty/blob/1ab80f78b1177290654f7935e8c571e27141b7e3/compiler/src/dotty/tools/dotc/typer/Inliner.scala#L349

[OlivierBlanvillain]

I am confused about this point, all val definitions define a type: their singleton type.

The meaning of case _: T changes depending on T, if T is a ground type that type test evaluates using a .isInstanceOf[T], whereas when T is a singleton type of form v.type, the type test evaluates using a .eq(v). The fact that enum Bar { case Foo } does not define a non singleton type for Foo thus makes a huge difference for match types.

Enum were designed to be a desugaring step which makes them super simple; if we have to special case the type checker at every corner to handle enums we lose some of that simplicity. I'm not saying we shouldn't do it, but it falls into the needs-spec/feature-request category. (Feel free to reopen if you're not convinced, I don't want to impose my views!)

[bishabosha]

@odersky I will reopen due to the linked PR #10938 which enables the snippet in this issue to compile.

I agree that not having a new backing class for each singleton enum value causes some friction but then again I fail to see why we could promote enum as a drop in replacement if it were not able to participate in the key metaprogramming advances of Scala 3.