summonInline[B <:< A] compiles when quoted despite B not being a subtype of A

[maphi]

Minimized code

// using 3.0.0-M2

import scala.quoted._
import scala.compiletime.summonInline

object Invalid {
  inline def apply[A, B]: Any = ${ invalidImpl[A, B] }

  def invalidImpl[A, B](using qctx: Quotes, tpeA: Type[A], tpeB: Type[B]): Expr[Any] = {
    '{summonInline[B <:< A]}
  }
}

/************ other file ************/

class A
class B extends A
println(Invalid[A, B]) // compiles as expected
println(Invalid[B, A]) // does also compile!

Expectation

'{summonInline[B <:< A]} should not compile when subtyping rules are violated

[smarter]

invalidImpl evalutes to:

    def invalidImpl[A >: Nothing <: Any, B >: Nothing <: Any](using 
      qctx: quoted.Quotes
    , tpeA: quoted.Type[A], tpeB: quoted.Type[B]): quoted.Expr[Any] = 
      {
        '{
          {
            val t: B <:< A = <:<.refl[B].$asInstanceOf$[B <:< A]
            t:B <:< A
          }
        }.apply(qctx)
      }

So the implicit search happens early (and I don't see how it can succeed given that we don't know that B <:< A at this point?), unlike what the documentation of summonInline says:

The summoning is delayed until the call has been fully inlined.

It does work as expected if we remove invalidImpl and replace the apply method by:

inline def apply[A, B]: Any = summonInline[B <:< A]

[nicolasstucki]

summonInline should no be inlined inside of the quote. The guard before inlining some code (Inliner.inlineCall(tree) in Typer) is missing that check.