Refinement on using Mirror not checked when automatically deriving mirrors

[eejbyfeldt]

Compiler version

3.3.5 and 3.6.4

Minimized code

object Test {
  def first[T <: Product](t: T)(using
      m: scala.deriving.Mirror.ProductOf[T] {
        type MirroredElemTypes <: NonEmptyTuple
      }
  ): Tuple.Head[m.MirroredElemTypes] = ??? 

  first(EmptyTuple)
}

Output

The code compiles.

Expectation

Changing the code to explicitly supply the mirror

object Test {
  def first[T <: Product](t: T)(using
      m: scala.deriving.Mirror.ProductOf[T] {
        type MirroredElemTypes <: NonEmptyTuple
      }
  ): Tuple.Head[m.MirroredElemTypes] = ???

  val m = summon[scala.deriving.Mirror.ProductOf[EmptyTuple]]
  first(EmptyTuple)(using m)
}

fails to compile with

$  scala3-3.6.4-x86_64-pc-linux/bin/scalac first.scala 
-- [E007] Type Mismatch Error: first.scala:9:26 ----------------------------------------------------------------------------------------------------------------------------------------------
9 |  first(EmptyTuple)(using m)
  |                          ^
  |                  Found:    (Test.m : scala.deriving.Mirror.Singleton{type MirroredMonoType = EmptyTuple; type MirroredType = EmptyTuple; type MirroredLabel = ("EmptyTuple" : String)})
  |                  Required: scala.deriving.Mirror.ProductOf[EmptyTuple.type]{type MirroredElemTypes <: NonEmptyTuple}
  |
  | longer explanation available when compiling with `-explain`
1 error found

Expectation is that the original code should fail to compile saying that it unable to find the Mirror.

[bishabosha]

there is usually a check on subtype matching of MirroredElemTypes, i think perhaps it is not being used specifically for singleton mirrors - so that should be investigated