Dotty: Match types combined with GADT pattern match not reducing as expected

[atennapel]

Minimized code

enum Bool {
  case True
  case False
}

import Bool._

enum SBool[B <: Bool] {
  case STrue extends SBool[True.type]
  case SFalse extends SBool[False.type]
}

import SBool._

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

def not[B <: Bool](b: SBool[B]): SBool[Not[B]] = b match {
  case STrue => SFalse
  case SFalse => STrue
}

Output

Found:    (SBool.STrue : SBool[(Bool.True : Bool)])
Required: SBool[Not[B]]

where:    B is a type in method not which is an alias of (Bool.False : Bool)

Expectation

I would expect the not function to pass typechecking, but it doesn't. Interestingly if I add a implicitly[Not[B] =:= False.type] in the first branch of not it will not complain, so it does know that B is actually True.type in that branch and it will reduce Not correctly if I ask for it.

It looks like the types are not reduced enough when checking the type of the branches against the return type of the function (not).

[bishabosha]

minimised to

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

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

[bishabosha]

in this case, it seems that the singleton type of enum values is treated differently to the singleton type of objects, e.g. this works:

sealed trait Bool
object Bool {
  case object True extends Bool
  case object False extends Bool
}

import Bool._

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

val f: Not[False.type] = True

[atennapel]

Writing Bool in that way still does not make my example typecheck.

[bishabosha]

Writing Bool in that way still does not make my example typecheck.

yes, what I found seems to be another issue :/

[OlivierBlanvillain]

Can this issue be minimized without enums? Match types on x.type where x is a val cannot be reduced by the compiler given that case _: x.type in a match expression desugars to a call to ==, which we know nothing about at compile time.

See my comments in https://github.com/lampepfl/dotty/issues/10511

[atennapel]

Could you suggest how I can change the example in my initial post to fix the issue? You are saying that

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

will not work well because I used an enum to create Bool, but if I use case object or case class then I can still not get this to work. Would love to know how to get this example working.

[OlivierBlanvillain]

Yes, I meant using traits and classes instead of enums to try to pin point the issue, like this:

sealed trait Bool
case object True extends Bool
case object False extends Bool

sealed trait SBool[B <: Bool]
case object STrue extends SBool[True.type]
case object SFalse extends SBool[False.type]

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

def not[B <: Bool](b: SBool[B]): SBool[Not[B]] = b match {
  case STrue => SFalse
  case SFalse => STrue
}

That minimization seems to be a duplicate #6687.

[atennapel]

Ooh I see now, your comment was about minimization of the example. Yes that might aid in debugging it.