Can't compile quotations matching with HK type arguments involved

[rssh]

Minimized code

package a

import scala.quoted._

trait CPM[F[_]]

def fun[M[_],T](t:T)(using m:CPM[M]):M[T] = ???

object M {

  inline def transform[F[_],T](t:T): F[T] =
     ${ transformImpl[F,T]('t) }

  def transformImpl[F[_]:Type,T:Type](t:Expr[T])(using Quotes):Expr[F[T]] = {
     import quotes.reflect._
     t match {
       case '{ a.fun[$mt,$tt]($t)(using $m) } => ???
     }

  }

}

Output

[error] -- [E057] Type Mismatch Error: /Users/rssh/tests/scala-misc/dotty/match-hk-hk/match-hk-hk/src/main/scala/a/M.scala:17:22 
[error] 17 |       case '{ a.fun[$mt,$tt]($t)(using $m) } => ???
[error]    |                      ^
[error]    |Type argument $mt does not conform to upper bound [_$1] =>> Any in subpart a.CPM[$mt] of inferred type scala.quoted.Expr[a.CPM[$mt]]
[error] one error found

Expectation

should compile

[rssh]

And here is failing to check lower bound 'Nothing':

package a

import scala.quoted._

trait CPM[F[_]]

def fun[M[_],T](t:M[T])(using m:CPM[M]):M[T] = ???

object M {

  inline def transform[F[_],T](t:T): F[T] =
     ${ transformImpl[F,T]('t) }

  def transformImpl[F[_]:Type,T:Type](t:Expr[T])(using qctx:QuoteContext):Expr[F[T]] = {
     import qctx.tasty._
     t match {
       case '{ a.fun[$mt,$tt]($t)(using $m) } => ???
     }

  }

}

result:

[error] -- [E057] Type Mismatch Error: /Users/rssh/tests/scala-misc/dotty/match-hk-hk/match-hk-hk/src/main/scala/a/M.scala:17:22 
[error] 17 |       case '{ a.fun[$mt,$tt]($t)(using $m) } => ???
[error]    |                      ^
[error]    |Type argument $mt[$tt] does not conform to lower bound Nothing in inferred type scala.quoted.Expr[$mt[$tt]]
[error] -- [E057] Type Mismatch Error: /Users/rssh/tests/scala-misc/dotty/match-hk-hk/match-hk-hk/src/main/scala/a/M.scala:17:31 
[error] 17 |       case '{ a.fun[$mt,$tt]($t)(using $m) } => ???
[error]    |                               ^
[error]    |          Type argument $mt[$tt] does not conform to lower bound Nothing
[error] two errors found

[nicolasstucki]

The correct way to set the bound of mt is by declaring the type variable explicitly with the correct kind.

       case '{ type mt[_]; a.fun[`mt`, tt]($t)(using $m) } => ???

After #17362 we will be able to write

       case '{ type mt[_]; a.fun[mt, tt]($t)(using $m) } => ???