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.

[soronpo]

Ok, in this case a bug was fixed (the multi-module code should not compile) and this issue needs to be resolved as a neg test.

[dwijnand]

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. 🤨

I don't see why GADT reasoning, or, rather, subtype reconstruction, shouldn't apply for match types.

[dwijnand]

To minimise:

trait Foo
type MT[A] <: Foo = A match
  case Foo => A

should compile, rather than

==> constrainPatternType(Foo, A)?
  ==> constraining simple pattern type A >:< Any?
  <== constraining simple pattern type A >:< Any = false gadt = GadtConstraint()
  ==> constraining simple pattern type Any >:< Any?
  <== constraining simple pattern type Any >:< Any = false gadt = GadtConstraint()
<== constrainPatternType(Foo, A) = true
-- [E007] Type Mismatch Error: i18448.scala:3:14 -------------------------------
3 |  case Foo => A
  |              ^
  |              Found:    A
  |              Required: Foo

[sjrd]

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. 🤨

I don't see why GADT reasoning, or, rather, subtype reconstruction, shouldn't apply for match types

You would need to write a spec for exactly what subtype reconstruction does in every possible situation and with the exact outcome, and then never change it anymore, if you want to apply it to match types.

[dwijnand]

We don't have that for term match trees, so why is it necessary for match type trees?

[sjrd]

For term match trees, whatever the type checker comes up with is then persisted in TASTy in the form of synthetic asInstanceOfs. We cannot do that for match types, since the computation needs to be redone under separate compilation.

[dwijnand]

Then I guess we could cop out some more of doing any spec-ing with some type level synthetic casting types.

How come that definition then compiles in the separate compilation situation. It shouldn't there either. 🤨

Btw, coming back to this earlier point, it's because in

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

we don't conforms check T with UB (on top of not bounds checking match type bounds, which I originally thought was the cause).

[dwijnand]

Btw, coming back to this earlier point, it's because in

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

we don't conforms check T with UB (on top of not bounds checking match type bounds, which I originally thought was the cause).

Nvm, it is bounds checking, but not here, in the other match type. In that match type, T conforms to UB. But in the other:

trait Foo
type Of[T] <: Foo = T match
  case Foo => T <:! Foo

T isn't known to be <:< Foo so doesn't match the first type parameter bound, unless we allow for the subtyping constraints for matching the pattern...