Unexpected union of skolems as `Singleton` type argument

[mbovel]

import scala.language.experimental.modularity

class Box1[T <: Singleton](val x: T)
class Box2[T : Singleton](val x: T)
def id(x: Int): x.type = x
def readInt(): Int = ???

def Test = ()
  val x /*: Box1[(?1 : Int) | (?2 : Int)]*/ = Box1(id(readInt()))

  val y = Box2(id(readInt())) // error: Failed to synthesize an instance of type
                              // Singleton{type Self = (?1 : Int) | (?2 : Int)}:
                              // (?1 : Int) | (?2 : Int) is not a singleton

sbt:scala3> scalac -Xprint-types -Xprint:typer tests/pos/singleton-skolem.scala
...
    val x: Box1[(<?3:Int> : Int) | (<?4:Int> : Int)] =
      <
        <<<new Box1:Box1>:([T <: Singleton](x: T): Box1[T])>[
          (<?3:Int> : Int) | (<?4:Int> : Int)]:
          ((x: (<?3:Int> : Int) | (<?4:Int> : Int)):
            Box1[(<?3:Int> : Int) | (<?4:Int> : Int)])
        >
      (<<id:((x: Int): x.type)>(<<readInt:((): Int)>():Int>):(<?4:Int> : Int)>):
        Box1[(<?3:Int> : Int) | (<?4:Int> : Int)]>
...

id(readInt()) gets a skolem type (?4: Int) as expected.

But then the type argument of Box1 is inferred to be (?3: Int) | (?4: Int). I don't understand where (?3: Int) | comes from. I would expect it to just be (?4: Int)

Compiler version: 8598403.

Same behavior since 3.0:

class Box1[T <: Singleton](val x: T)
def id(x: Int): x.type = x
def readInt(): Int = ???

def Test = ()
  val x /*: Box1[(?1 : Int) | (?2 : Int)]*/ = Box1(id(readInt()))

$ scala compile -S 3.0 --server=false -Xprint:typer tests/pos/singleton-skolem.scala
...
    val x: Box1[(?1 : Int) | (?2 : Int)] = new Box1[((?1 : Int) | (?2 : Int))](id(readInt()))
...

[mbovel]

Related:

class Box[+T <: Singleton](val x: T)
def id(x: Int): x.type = x
def readInt(): Int = ???

def Test = ()
  val x /*: Box[Int]*/ = Box(id(readInt())) // error: Type argument Int does not conform
                                            // to upper bound Singleton in inferred type Box[Int]

[EugeneFlesselle]

Conjecturing here: it may be that when Box is invariant, we perform an isSameType test, which triggers two isSubType tests. Each could be generating separate skolems (necessary because we have different approximation directions?), added to the constraint set, yielding the union type. We may also be missing the avoidance of the skolems here because they are below a union type.

May be related to #20175.