trivial quoted pattern is refutable

[bishabosha]

Compiler version

3.2.1

Minimized code

import quoted.*

def foo(using Quotes)(x: Expr[Any]): Expr[Unit] =
  val '{ $y: Any } = x
  val '[List[Int]] = Type.of[List[Int]]
  '{}

Output

-- Warning: --------------------------------------------------------------------
4 |  val '{ $y: Any } = x
  |      ^^^^^^^^^^^^^^^^
  |pattern binding uses refutable extractor `x$1.asInstanceOf[scala.quoted.runtime.QuoteMatching].ExprMatch`
  |
  |If this usage is intentional, this can be communicated by adding `: @unchecked` after the expression,
  |which may result in a MatchError at runtime.
-- Warning: --------------------------------------------------------------------
5 |  val '[List[Int]] = Type.of[List[Int]]
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |pattern binding uses refutable extractor `x$1.asInstanceOf[scala.quoted.runtime.QuoteMatching].TypeMatch`
  |
  |If this usage is intentional, this can be communicated by adding `: @unchecked` after the expression,
  |which may result in a MatchError at runtime.

Expectation

It seems these patterns should always bind? can the refutability be improved or is it not possible

originally from the tests as seen here:
https://github.com/lampepfl/dotty/blob/4fa0715f20e7cabfae04defc4c3a71aa994578b4/tests/run-macros/paramSymss/Macro_1.scala#L8

[bishabosha]

also perhaps printing of quoted pattern extractors could be improved

[nicolasstucki]

We should be able to make quoted patterns irrefutable for

• '{ $x: T } for a U <: T an a scrutinee of type Expr[U]
• '{ $x: t }