Get concrete bounds of TypeRepr

[s5bug]

After my success with https://scastie.scala-lang.org/O4YhUozxSnO2PdXGKwivwQ, I want to create a macro which automatically rejects cases where the match would be non-exhaustive.

For A =:!= B, this means getting a concrete AL and AU s.t. A >: AL <: AU, and likewise for B. How do I do this? I don't see any method to grab TypeBounds off of a TypeRepr. I currently have

  inline given notSubMacro: [A, B] => <:!<[A, B] =
    ${ NotSubPlatform.impl[A, B] }

Consider the case where someone writes

def foo[T <: CharSequence] = summon[String <:!< T]

This should fail, as T = String is a valid possibility. However,

def bar[T <: String] = summon[CharSequence <:!< T]

should succeed, as CharSequence is never going to be widenable to T.

It's impossible to implement this with just subtype checks on T. Consider foo[CharSequence]:

test -- TypeRef(ThisType(TypeRef(NoPrefix,module class lang)),class String) <:!< TypeRef(NoPrefix,type T)
TypeRef(ThisType(TypeRef(NoPrefix,module class lang)),class String) <:< TypeRef(NoPrefix,type T) -- false
TypeRef(NoPrefix,type T) <:< TypeRef(ThisType(TypeRef(NoPrefix,module class lang)),class String) -- false

This false, false result, when summoning the <:!< should fail, is the exact same as a succeeding case:

test -- TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int) <:!< TypeRef(ThisType(TypeRef(NoPrefix,module class lang)),class String)
TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int) <:< TypeRef(ThisType(TypeRef(NoPrefix,module class lang)),class String) -- false
TypeRef(ThisType(TypeRef(NoPrefix,module class lang)),class String) <:< TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int) -- false

---

Assume that type A >: AL <: AU, type B >: BL <: BU, where AL, AU, BL, BU are all concrete. (ex. a generic with no bounds, i.e. def foo[A], would have AL = Nothing and AU = Any.) An A <:!< B should be legal iff:

• BU <:< AL and !(AL =:= BU) (widening to the upper bound of B would not enter the lower bound of A), or
• ProvablyDisjoint[A, B]
  Otherwise, A and B are possibly not disjoint, and if one is joint with the other, they share at least one type of overlap

For an A =:!= B to be legal:

• BU <:< AL and !(AL =:= BU) (A <:!< B), or
• AU <:< BL and !(BL =:= AU) (B <:!< A), or
• ProvablyDisjoint[A, B]

I think ProvablyDisjoint is easy once I have AL, AU, BL, BU: I just check that there's no possible subtyping relationships between any of the bounds. However, the difficulty still lies in finding those four types. Is there something in the macro system that will give them to me?

[sjrd]

ProvablyDisjoint is not at all easy. It's one of the two hard spec algorithms behind match types. Fortunately, that means you can use match types to implement it:

type ProbablyDisjoint[A, B] <: Boolean = A match 
  case B => false 
  case _ => true

(Request with using ProvablyDisjoint[A, B] =:= true.)

For the other situation, it's hard to even specify what you want. Lower bounds are tricky. But usually they are Nothing anyway, so I would expect that clause not to be very usable in practice. I wouldn't bother with it.

[s5bug]

What I really want is a way to immediately abort a macro if the generated match (see the Scastie linked in OP) would raise a non-exhaustive warning. The subtyping stuff is just the way I imagined I could get there / reimplement the logic.

[sjrd]

That's not realistically possible. The conditions under which a match are exhaustive are much, much more involved than a few type tests. There's a full constraints engine in there.

I mean you could copy-paste the entire implementation of the space engine into your macro, of course, but that's a big bazooka.

[s5bug]

I don't need all of the conditions for match exhaustion: mine's actually very simple. The issue is grabbing the bounds out of an abstract type: if I could just do that, I could do all of this without needing ProvablyDisjoint or match-exhaustion checking, and I could use it just to verify that my specific tiny match would be exhaustive.