Narrowing the type of `MirroredElemLabels` is not equivalent to using `<:<`

[arainko]

Compiler version

3.4.1, 3.5.0-RC1-bin-20240429-e2c456f-NIGHTLY

Minimized code

//> using scala 3.4.1

import scala.deriving.Mirror

enum YesNo {
  case Yes, No
}

enum NoYes {
  case No, Yes
}


object Repro {
  def derived[A](using A: Mirror.SumOf[A] { type MirroredElemLabels = ("Yes", "No") }) = ???

  def derivedWithEvidence[A](using A: Mirror.SumOf[A], ev: A.MirroredElemLabels <:< ("Yes", "No")) = ???

  derived[YesNo] // compiles, as expected
  derived[NoYes] // compiles, yet NoYes.MirroredElemLabels is ("No", "Yes")

  derivedWithEvidence[YesNo] // compiles, as expected
  // derivedWithEvidence[NoYes] // compilation fails, as expected
}

Expectation

I'd expect derived[NoYes] (just like derivedWithEvidence[NoYes]) to fail the compilation since its MirroredElemLabels is ("No", "Yes) but the method's A argument refined to only allow ("Yes", "No")

[bishabosha]

this is what is resolves to:

Repro.derived[NoYes](
        NoYes.$asInstanceOf[

            scala.deriving.Mirror.Sum{
              type MirroredMonoType = NoYes; type MirroredType = NoYes;
                type MirroredLabel = ("NoYes" : String);
                type MirroredElemTypes = ((NoYes.No : NoYes),
                  (NoYes.Yes : NoYes));
                type MirroredElemLabels >: (("Yes" : String), ("No" : String)) |
                   (("No" : String), ("Yes" : String)) <: (("Yes" : String),
                  ("No" : String)) & (("No" : String), ("Yes" : String))
            }

        ]
      )

this is impossible to type manually btw

scala> type MirroredElemLabels >: ("Yes", "No") | ("No", "Yes") <: ("Yes", "No") & ("No", "Yes")
-- Error: ----------------------------------------------------------------------
1 |type MirroredElemLabels >: ("Yes", "No") | ("No", "Yes") <: ("Yes", "No") & ("No", "Yes")
  |^
  |object rs$line$2 cannot be instantiated since it has a member MirroredElemLabels with possibly conflicting bounds (("Yes" : String), ("No" : String)) | (("No" : String), ("Yes" : String)) <: ... <: (("Yes" : String), ("No" : String)) & (("No" : String), ("Yes" : String))
1 error found

actually, you can get around the check with a cast, as is done for the synthesised mirror argument:

scala> null.asInstanceOf[deriving.Mirror.Sum {
     |   type MirroredElemLabels >: ("Yes", "No") | ("No", "Yes") <: ("Yes", "No") & ("No", "Yes")
     | }]

so perhaps to fix this we should do checkRealizableBounds on the synthesised mirror - or their types at least