Failure to refine @-bound variables (x @ <pattern>) when pattern is a literal

[TomasMikula]

Compiler version

3.6.4

Minimized code

def bad[S <: String](s: S): Unit =
  s match
    case x @ "x" =>
      x: S       // OK
      x: "x"     // Error: Found: (x : S), Required: ("x" : String)
      x: S & "x" // Error: Found: (x : S), Required: S & ("x" : String)

Output

-- [E007] Type Mismatch Error: test.scala:5:6 ----------------------------------
5 |      x: "x"     // Error: Found: (x : S), Required: ("x" : String)
  |      ^
  |      Found:    (x : S)
  |      Required: ("x" : String)
  |
  |      where:    S is a type in method bad with bounds <: String
  |
  | longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: test.scala:6:6 ----------------------------------
6 |      x: S & "x" // Error: Found: (x : S), Required: S & ("x" : String)
  |      ^
  |      Found:    (x : S)
  |      Required: S & ("x" : String)
  |
  |      where:    S is a type in method bad with bounds <: String
  |
  | longer explanation available when compiling with `-explain`
-- [E129] Potential Issue Warning: test.scala:4:6 ------------------------------
4 |      x: S       // OK
  |      ^^^^
  |      A pure expression does nothing in statement position
  |
  | longer explanation available when compiling with `-explain`
1 warning found
2 errors found

Expectation

The type of variable x in x @ "x" should be refined to S & "x", analogous to how it works with non-literal patterns:

sealed trait Foo
case class Bar() extends Foo

def good[S <: Foo](s: S): Unit =
  s match
    case b @ Bar() =>
      b: S       // OK
      b: Bar     // OK
      b: S & Bar // OK

Note

I believe this issue will be easier to fix than #22887, as this one is about assigning a more precise type to a newly bound variable, rather than locally (within a pattern case) refining type of an existing variable.

[som-snytt]

case "x" is not case _: "x". Is the expectation that they ought to be treated the same?

I had the same question about your recent similar ticket, where it did not make a difference.

For a constructor pattern, I would expect a type test; but I also had a question about the semantics of Scala 3 patterns here (because of the internal representation).

I think I looked for documentation or spec in vain; but maybe there is institutional knowledge.

Edit: related ticket is #16821

[TomasMikula]

case "x" is not case _: "x". Is the expectation that they ought to be treated the same?

That's not something I'm trying to argue in this ticket (although I believe they should be effectively the same for literal types).

Note that I only used case x @ <pattern> in my snippets above (i.e. no case x: <type>).

[som-snytt]

On the related ticket, Dale pushes back on anything except an equality test. (Which I think is not sufficient.)

[TomasMikula]

On the related ticket, Dale pushes back on anything except an equality test. (Which I think is not sufficient.)

Not exactly sure what you mean, but I'm just arguing that case x @ "x" should behave analogously to case x @ Bar().

[som-snytt]

To explain what I mean, case 42 only means 42 == x, not x.type <:< 42. The related ticket says you have to enforce 42 <:< x.type (which matters for interpreting the literal).

I think what you're asking is a spec change (which I think is a good change). But on the related ticket, they're not (even) willing to enforce what is already in the spec. (I don't know if this is a case of "just syntax", since case x: "x" currently serves the purpose.)

[TomasMikula]

FWIW, I think what I'm asking for is in the spec (but I sure don't mind updating the spec if it makes Scala better):

8.1.3 Pattern Binders

Pattern2        ::=  varid ‘@’ Pattern3

A pattern binder x@p consists of a pattern variable x and a pattern p. The type of the variable x is the static type T implied by the pattern p. This pattern matches any value v matched by the pattern p, and it binds the variable name to that value.

A pattern p implies a type T if the pattern matches only values of the type T.

https://www.scala-lang.org/files/archive/spec/3.4/08-pattern-matching.html#pattern-binders

According to the above, the type of variable x in x @ "x" should be the type implied by pattern "x", which is "x". However, my snippet shows this is violated:

x: "x" // Error: Found: (x : S), Required: ("x" : String)

EDIT: The definition of "implies" in the spec is unfortunate. For example, any pattern implies (among others) the type Any, since any pattern "matches only values of the type Any." This is likely unintended, as the previous paragraph suggests uniqueness of the type implied by a pattern: "the static type T implied by the pattern p."