Summon allows to ignore type bounds

[Decel]

Compiler version

3.3.0-RC1

Minimized code

scala> type F[X <: String] = X
// defined alias type F[X <: String] = X
                                                                                
scala> val a = summon[F[Int] =:= Int]
val a: Int =:= Int = generalized constraint

Output

Works. Both in REPL and Compiler.

Expectation

-- [E057] Type Mismatch Error: -------------------------------------------------
  |val a = summon[F[Int] =:= Int]
  |                 ^
  |                 Type argument Int does not conform to upper bound String

[odersky]

I think that's due to the way summon works, and the fact that it is a transparent inline function. If I just write

type S = F[Int] =:= Int

I get

-- [E057] Type Mismatch Error: test.scala:5:11 ---------------------------------
5 |type S = F[Int] =:= Int
  |           ^
  |           Type argument Int does not conform to upper bound String
  |
  | longer explanation available when compiling with `-explain`
1 error found

But the problem is that the bounds check happens after typer (why only then? Because of F-bounds which can force cyclic reference errors otherwise). But since summon runs at typer, it means we only get to see summon's result when we do the bounds checking, and that result has no trace of F anymore:

    val a: Int =:= Int =
      {
        val x$proxy1: Int =:= Int = <:<.refl[Int]
        x$proxy1
      }

[odersky]

To fix this, we could simply change the Inlined case in PostTyper like this:

        case Inlined(call, bindings, expansion) if !call.isEmpty =>
          val pos = call.sourcePos
          CrossVersionChecks.checkExperimentalRef(call.symbol, pos)
          super.transform(call)   <<<<<<<<<<<<< insert this line
          val callTrace = Inlines.inlineCallTrace(call.symbol, pos)(using ctx.withSource(pos.source))
          cpy.Inlined(tree)(callTrace, transformSub(bindings), transform(expansion)(using inlineContext(call)))

But I am worried that this could give exponential blowup of checks for deeply nested inlines. So we probably need something a little smarter than this.