Lowercase identifier in match-type pattern is treated as a reference instead of a binding

[Sporarum]

Compiler version

3.3.0 / 3.3.1-RC1

Minimized code & Output

type F[x, y] <: Boolean = x match
  case y => true
  case _ => false

def f(x: Int, y: Int): Boolean = x match
  case y => true
  case _ => false // warning: unreachable case

assert(f(3, 4) == true)

summon[F[3, 4] =:= false]

https://scastie.scala-lang.org/3rY95JNeTcOwEluPSrVuWg

Expectation

F[3,4] should return true: Since y is lowercase it should bind instead of being a reference, like in f for terms

Do note that lowercase identifiers do bind if they are part of a bigger pattern, see for example this Concat taken from the matchtype reference page:

type Concat[Xs <: Tuple, +Ys <: Tuple] <: Tuple = Xs match
  case EmptyTuple => Ys
  case x *: xs => x *: Concat[xs, Ys]

Any code with a lowercase identifier which is alone in its pattern can be rewritten by using _ on the left of the =>, and the scrutinee on the right of the =>, so fixing this syntax offers no new expressivity Conversly, not fixing this also offers no new expressivity, as it can also always be rewritten with ` around it instead

I still believe this bug should be fixed, as right now people toying around with matchtypes may be thaught the lesson that "lowercase identifiers never bind in matchtypes" which will cause a lot of confusion when they later see code that does bind !

[Sporarum]

I found this in that page of the reference: "Type variables in patterns start with a lower case letter, as usual." But it's not obvious what it means, what about type variables coming from outside the matchtype, should they also be written with a lowercase ? (rhetorical question)

[dwijnand]

Sounds reasonable to me. (It's technically a breaking change - by changing the meaning of legal, niche syntax, but hopefully niche enough we can do it.)

Currently we're just typedType'ing the Ident y. It needs to run through desugar.patternVar to become a binding y @ _. But I'd actually like if bindings were made available to the user in match types (sorry for hijacking/feature creeping your issue!). For instance it would be nice to be able to write tests/pos/i16706.scala from

type TupleUnionLub[T <: Tuple, Lub, Acc <: Lub] <: Lub = T match {
  case (h & Lub) *: t => TupleUnionLub[t, Lub, Acc | h]
  case EmptyTuple     => Acc
}

to

type TupleUnionLub[T <: Tuple, Lub, Acc <: Lub] <: Lub = T match {
  case (h @ Lub) *: t => TupleUnionLub[t, Lub, Acc | h]
  case EmptyTuple     => Acc
}

which I believe is the intent.

[SethTisue]

(Further on the hijacking tangent, both (h & Lub) and (h @ Lub) seem peculiar to me; I expected (h <: Lub), and Dale tells me that Lionel also made the same suggestion at #6047. But we should probably move the tangent to a different ticket/discussion.)

[Sporarum]

I believe this is really a bug ! Technically it is, since the reference is currently the spec and it doesn't mention this behaviour at all

I think a very convincing example of why this needs to be changed is the following:

type F1[x, y] <: Boolean = x match
  case y => true
  case _ => false

type F2[x, y] <: Boolean = (x *: EmptyTuple) match
  case (y *: EmptyTuple) => true
  case _ => false

summon[F1[3, 4] =:= false] // why is this different than F2 ???
summon[F2[3, 4] =:= true ] // expected; we need a way to use matchtypes to extract types

[Decel]

I believe this is really a bug ! Technically it is, since the reference is currently the spec and it doesn't mention this behaviour at all

I think a very convincing example of why this needs to be changed is the following:

type F1[x, y] <: Boolean = x match
  case y => true
  case _ => false

type F2[x, y] <: Boolean = (x *: EmptyTuple) match
  case (y *: EmptyTuple) => true
  case _ => false

summon[F1[3, 4] =:= false] // why is this different than F2 ???
summon[F2[3, 4] =:= true ] // expected; we need a way to use matchtypes to extract types

That is because it's notation for Tuple1

val a = implicitly[Tuple1[Int] =:= Int *: EmptyTuple]

And we can't prove that Tuple1[x] is disjoint from Tuple1[y]

[dwijnand]

And we can't prove that Tuple1[x] is disjoint from Tuple1[y]

We're not trying to. We're matching Tuple1[?y] to Tuple1[3], which matches, instantiating ?y to 3. The bug is in F1, where instead of instantiating a ?y to 3, we're trying to to match case 4 to 3.

[Sporarum]

Discussing with @sjrd (who is actively looking at the use of match types in the wild), this is actually a very common pattern ! It happens when there are nested matched types: extract a in the outer, use a as a pattern in the inner

So it seems there's not much we can do about it, apart from documenting it (which he is doing), and maybe emitting a warning (which might not be what we want if this pattern is common and useful)

[dwijnand]

So it seems there's not much we can do about it, apart from documenting it (which he is doing), and maybe emitting a warning (which might not be what we want if this pattern is common and useful)

Or we can fix the bug and people that accidentally relied on the bug fix their code. Modulo whatever -language/-source/-whatever we want to use to get us from the current behaviour to fixing the semantics.

[sjrd]

You can warn or even error on such code as a source-breaking release. But making compile with semantics 1 to compile with semantics 2, silently, should be avoided at almost all cost.

[dwijnand]

Sure. We can have one minor release that warns, requiring those use cases to use `y` and binding use cases to use the more verbose (and not currently supported but another reason to implement) y @ _, and a following minor release that stops warning.

[Sporarum]

This would still not be good, as for any number of releases between semantics 1 and semantics 2, there will be users that upgrade directly from on to the other (This was again pointed out to me by @sjrd)

[dwijnand]

Sure, the best we can do, if we don't want to give up on fixing the semantics, is pick what timeframe to use.

[dwijnand]

@odersky I just realised that match type trees only support types (rejectWildcardType(infixType())) as a type case clause. In order to support some form of bindings, like:

type TupleUnionLub[T <: Tuple, Lub, Acc <: Lub] <: Lub = T match {
  case (h @ Lub) *: t => TupleUnionLub[t, Lub, Acc | h]
  case EmptyTuple     => Acc
}

or a more simple

type MT[T <: Tuple] = T match
  case (h @ Int) *: _ => Long
  case _              => String

Would you be happy if we extended the parser to do more than parse types. In term match trees we have a whole concept of "patterns", which allows for binds.

[Sporarum]

@sjrd is overhauling the whole match-type specification, and I think it might include things like that (but I don't know more details)

[sjrd]

My current plan does not involve anything like that. A possible rewriting is

type TupleUnionLub[T <: Tuple, Lub, Acc <: Lub] <: Lub = T match {
  case h *: t =>
    h match
      case Lub => TupleUnionLub[t, Lub, Acc | h]
  case EmptyTuple     => Acc
}

[dwijnand]

My current plan does not involve anything like that.

Do you mean that bindings is outside of what your covering (which is more reduction specific) or that your plan is not to allow bindings?

Also, with rewrites like that I've found that breaking things down like that can at the very least make things more complicated (by having to extract duplication and reference it multiple times) for cases where you want cases to cascade. I've also seen it affect match reduction, but those might be bugs (which is what has blocked my match type bounds PR).

[sjrd]

My current plan does not introduce new stuff. So bindings are outside the scope. That said, they would be easier/safer to introduce on top of the new foundation, so there's that. I don't have anything against introducing bindings per se.