Match type regression

[soronpo]

OK, I'm not clear what is supposed to happen here, and if this is a bug that I accidentally treated as a feature or it's supposed to work. Under 3.3.0 (LTS) this code compiles successfully, BUT I just noticed that if everything is in the same file and not across modules, then it does not.

Compiler version

Last good release: 3.4.0-RC1-bin-20230818-932c10d-NIGHTLY
First bad release: 3.4.0-RC1-bin-20230821-6e370a9-NIGHTLY
First bad commit: 34dbdd8
Regression from #18398

Minimized code

UBMatch.scala

type <:![T <: UB, UB] <: UB = T match
  case UB => T

UBMatch.test.scala

//> using test.dep org.scalameta::munit::0.7.29
trait Foo
type Of[T] <: Foo = T match
  case Foo => T <:! Foo

Output

4 |  case Foo => T <:! Foo
  |              ^^^^^^^^^
  |              Found:    T <:! Foo
  |              Required: Foo

Expectation

Should compile (not completely sure, see comment on the head of the issue)

Edit: Should not compile (see discussion)

[soronpo]

@sjrd I would love your comment on this, considering I used this match types trick for the lack of case t <: UB => t under the current match type implementation.

[sjrd]

These are all fully-defined match types (without type captures), so there's no reason they shouldn't work.

That said, I think your <:! can be implemented in a much simpler way as

type <:![T <: UB, UB] <: UB = T & UB

[soronpo]

These are all fully-defined match types (without type captures), so there's no reason they shouldn't work.

That said, I think your <:! can be implemented in a much simpler way as

type <:![T <: UB, UB] <: UB = T & UB

Oh, yeah, thanks! I think it's the third time I'm forgetting & exists in this way 🙈

[dwijnand]

These are all fully-defined match types (without type captures), so there's no reason they shouldn't work.

That said, I think your <:! can be implemented in a much simpler way as

type <:![T <: UB, UB] <: UB = T & UB

Do you mean

type <:![T <: UB, UB] = T & UB

?

[dwijnand]

4 |  case Foo => T <:! Foo
  |              ^^^^^^^^^
  |              Found:    T <:! Foo
  |              Required: Foo

Again, lack of GADT constraints during phases that aren't Typer...

T match
  case UB => T

is simplifying to T, while it should actually be simplifying to {T <: UB} T, which would make T <:! Foo remember it's<: Foo..

[soronpo]

These are all fully-defined match types (without type captures), so there's no reason they shouldn't work.
That said, I think your <:! can be implemented in a much simpler way as

type <:![T <: UB, UB] <: UB = T & UB

Do you mean

type <:![T <: UB, UB] = T & UB

?

Yes, that's what he meant and it works.

[sjrd]

4 |  case Foo => T <:! Foo
  |              ^^^^^^^^^
  |              Found:    T <:! Foo
  |              Required: Foo

Again, lack of GADT constraints during phases that aren't Typer...

T match
  case UB => T

is simplifying to T, while it should actually be simplifying to {T <: UB} T, which would make T <:! Foo remember it's<: Foo..

Ah, yes, I missed that the definition requires some GADT-style reasoning. There's not supposed to be GADT reasoning in match types. How come that definition then compiles in the separate compilation situation. It shouldn't there either. 🤨

And yes, that means relying on it was already relying on a bug. Not just relying on the current unspecified match type reduction.