Path dependent types level checking false negatives

[nicolasstucki]

minimized code

import scala.quoted._

class M {
  type E
}

def f[T: Type](using Quotes) =
  Expr.summon[M] match
    case Some('{ $mm : tt }) =>
      '{
        val m = $mm
        type ME = m.E
        ${ g[ME](using Type.of[ME]) }
        ${ g[m.E](using Type.of[ME]) }
        ${ g[ME](using Type.of[m.E]) }
        ${ g[m.E](using Type.of[m.E]) }
        ${ g[ME] }
        ${ g[m.E] }
      }

def g[T](using Type[T]) = ???

Has false negatives when checking the level of m in the types.

Compilation output

-- Error: Foo.scala:16:13 ------------------------------------------------------
16 |        ${ g[m.E](given '[ME]) }
   |             ^
   |             access to value m from wrong staging level:
   |              - the definition is at level 1,
   |              - but the access is at level 0.
-- Error: Foo.scala:18:13 ------------------------------------------------------
18 |        ${ g[m.E](given '[m.E]) }
   |             ^
   |             access to value m from wrong staging level:
   |              - the definition is at level 1,
   |              - but the access is at level 0.
-- Error: Foo.scala:19:16 ------------------------------------------------------
19 |        ${ g[ME] }
   |                ^
   |       access to type E from wrong staging level:
   |        - the definition is at level 0,
   |        - but the access is at level 1.
   |
   |        The access would be accepted with a given scala.quoted.Type[m.E]
-- Error: Foo.scala:20:13 ------------------------------------------------------
20 |        ${ g[m.E] }
   |             ^
   |             access to value m from wrong staging level:
   |              - the definition is at level 1,
   |              - but the access is at level 0.

expectation

They should all compile and be equivalent