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