Also checkRefinement for Singleton mirror

Also improves the refinement check to also handle bounds properly.

Author: eejbyfeldt

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -1753,6 +1753,8 @@ object Types extends TypeUtils {
               if (pre.refinedName ne name) loop(pre.parent) else tp.alias
             case tp: SingletonType =>
               if pre.refinedName ne name then loop(pre.parent) else tp
+            case tp: RealTypeBounds =>
+              if pre.refinedName ne name then loop(pre.parent) else tp
             case _ =>
               loop(pre.parent)
           }

compiler/src/dotty/tools/dotc/typer/Synthesizer.scala

@@ -316,7 +316,7 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
 
   private def checkRefinement(formal: Type, name: TypeName, expected: Type, span: Span)(using Context): Unit =
     val actual = formal.lookupRefined(name)
-    if actual.exists && !(expected =:= actual)
+    if actual.exists && !(actual.bounds.contains(expected))
     then report.error(
       em"$name mismatch, expected: $expected, found: $actual.", ctx.source.atSpan(span))
 
@@ -504,6 +504,8 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
         case MirrorSource.Singleton(_, tref) =>
           val singleton = tref.termSymbol // prefer alias name over the original name
           val singletonPath = tpd.singleton(tref).withSpan(span)
+          checkRefinement(formal, tpnme.MirroredElemTypes, defn.EmptyTupleModule.termRef, span)
+          checkRefinement(formal, tpnme.MirroredElemLabels, defn.EmptyTupleModule.termRef, span)
           if tref.classSymbol.is(Scala2x) then // could be Scala 3 alias of Scala 2 case object.
             val mirrorType = formal.constrained_& {
               mirrorCore(defn.Mirror_SingletonProxyClass, mirroredType, mirroredType, singleton.name)

tests/neg/i22851.scala

@@ -0,0 +1,10 @@
+object Test {
+  def first[T <: Product](t: T)(using
+      m: scala.deriving.Mirror.ProductOf[T] {
+        type MirroredElemTypes <: NonEmptyTuple
+      }
+  ): Tuple.Head[m.MirroredElemTypes] = ??? 
+
+  first(EmptyTuple) // error
+  // MirroredElemTypes missmatch, expected: EmptyString, found: <: NonEmptyTuple.
+}