Can we add a NOT operator to match types to force disjointness?

Language Design
1

Consider the following simple example:

type IsSingleton[T <: Int] = T match
  case Singleton => true
  case _ => false

It fails to reduce if we attempt IsSingleton[Int] due to failure to prove disjointness, which is correct.
I kind of wish there was a NOT operator specially available in match types so we can force disjointness by specifying what is not an upper bound.

type IsSingleton[T <: Int] = T match
  case Singleton => true
  case NOT[Singleton] => false
1 Like
2

Alternatively, we could create a type HasUpperBound[T, UB] <: Boolean under scala.compiletime, that acts like the various compiletime ops, but works in general and not just for literals. This can then be applied within the match types for IF/Else conditioning of upper bounds that return true/false. However, I don’t know if this can yield unsound results under certain conditions.

3

None of that would be sound. Under narrowing (replacing a supertype by a subtype through substitutions), this would turn a false result into a true. And obviously, true is not a subtype of false, so that’s unsound.

4 Likes