diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 0f0b7267fff3..3fc6280865c5 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -439,8 +439,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
           (tp1.widenSingletons ne tp1) &&
           recur(tp1.widenSingletons, tp2)
 
-        if (tp2.atoms.nonEmpty && canCompare(tp2.atoms))
-          tp1.atoms.nonEmpty && tp1.atoms.subsetOf(tp2.atoms)
+        if (tp2.atoms().nonEmpty && canCompare(tp2.atoms()))
+          val atoms1 = tp1.atoms(widenOK = true)
+          atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms())
         else
           widenOK
           || joinOK
@@ -620,8 +621,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         }
         compareTypeLambda
       case OrType(tp21, tp22) =>
-        if (tp2.atoms.nonEmpty && canCompare(tp2.atoms))
-          return tp1.atoms.nonEmpty && tp1.atoms.subsetOf(tp2.atoms) || isSubType(tp1, NothingType)
+        if (tp2.atoms().nonEmpty && canCompare(tp2.atoms()))
+          val atoms1 = tp1.atoms(widenOK = true)
+          return atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms()) || isSubType(tp1, NothingType)
 
         // The next clause handles a situation like the one encountered in i2745.scala.
         // We have:
@@ -1797,9 +1799,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     else if ((tp2 isRef AnyClass) || (tp2 isRef AnyKindClass) || (tp1 isRef NothingClass)) tp2
     else {
       def mergedLub: Type = {
-        val atoms1 = tp1.atoms
+        val atoms1 = tp1.atoms(widenOK = true)
         if (atoms1.nonEmpty && !widenInUnions) {
-          val atoms2 = tp2.atoms
+          val atoms2 = tp2.atoms(widenOK = true)
           if (atoms2.nonEmpty) {
             if (atoms1.subsetOf(atoms2)) return tp2
             if (atoms2.subsetOf(atoms1)) return tp1
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index cc0d6982c5e5..ce3ea5b49eb7 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1156,8 +1156,10 @@ object Types {
     /** If this type is an alias of a disjunction of stable singleton types,
      *  these types as a set, otherwise the empty set.
      *  Overridden and cached in OrType.
+     *  @param widenOK  If type proxies that are upperbounded by types with atoms
+     *                  have the same atoms. 
      */
-    def atoms(implicit ctx: Context): Set[Type] = dealias match {
+    def atoms(widenOK: Boolean = false)(implicit ctx: Context): Set[Type] = dealias match {
       case tp: SingletonType =>
         def normalize(tp: Type): Type = tp match {
           case tp: SingletonType =>
@@ -1171,12 +1173,13 @@ object Types {
             }
           case _ => tp
         }
-        val underlyingAtoms = tp.underlying.atoms
+        val underlyingAtoms = tp.underlying.atoms(widenOK)
         if (underlyingAtoms.isEmpty && tp.isStable) Set.empty + normalize(tp)
         else underlyingAtoms
-      case tp: ExprType => tp.resType.atoms
-      case tp: OrType => tp.atoms // `atoms` overridden in OrType
-      case tp: AndType => tp.tp1.atoms & tp.tp2.atoms
+      case tp: ExprType => tp.resType.atoms(widenOK)
+      case tp: OrType => tp.atoms(widenOK) // `atoms` overridden in OrType
+      case tp: AndType => tp.tp1.atoms(widenOK) & tp.tp2.atoms(widenOK)
+      case tp: TypeProxy if widenOK => tp.underlying.atoms(widenOK)
       case _ => Set.empty
     }
 
@@ -2894,22 +2897,26 @@ object Types {
 
     private var atomsRunId: RunId = NoRunId
     private var myAtoms: Set[Type] = _
+    private var myWidenedAtoms: Set[Type] = _
     private var myWidened: Type = _
 
     private def ensureAtomsComputed()(implicit ctx: Context): Unit =
       if (atomsRunId != ctx.runId) {
-        val atoms1 = tp1.atoms
-        val atoms2 = tp2.atoms
+        val atoms1 = tp1.atoms()
+        val atoms2 = tp2.atoms()
         myAtoms = if (atoms1.nonEmpty && atoms2.nonEmpty) atoms1 | atoms2 else Set.empty
+        val widenedAtoms1 = tp1.atoms(widenOK = true)
+        val widenedAtoms2 = tp2.atoms(widenOK = true)
+        myWidenedAtoms = if (widenedAtoms1.nonEmpty && widenedAtoms2.nonEmpty) widenedAtoms1 | widenedAtoms2 else Set.empty
         val tp1w = tp1.widenSingletons
         val tp2w = tp2.widenSingletons
         myWidened = if ((tp1 eq tp1w) && (tp2 eq tp2w)) this else tp1w | tp2w
         atomsRunId = ctx.runId
       }
 
-    override def atoms(implicit ctx: Context): Set[Type] = {
+    override def atoms(widenOK: Boolean)(implicit ctx: Context): Set[Type] = {
       ensureAtomsComputed()
-      myAtoms
+      if widenOK then myAtoms else myWidenedAtoms
     }
 
     override def widenSingletons(implicit ctx: Context): Type = {
diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
index 8ff7e0c26697..ba8dba54868b 100644
--- a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
@@ -118,7 +118,7 @@ object ErrorReporting {
       else if (ctx.settings.explainTypes.value)
         i"""
            |${ctx.typerState.constraint}
-           |${TypeComparer.explained((found <:< expected)(_))}"""
+           |${TypeComparer.explained(found <:< expected)}"""
       else
         ""
     }
diff --git a/tests/pos/i8129.scala b/tests/pos/i8129.scala
new file mode 100644
index 000000000000..8512b3c5846e
--- /dev/null
+++ b/tests/pos/i8129.scala
@@ -0,0 +1,4 @@
+object Test {
+  type F[N <: 0 | 1] = N
+  def fl[N <: 0 | 1]: F[N] = ???
+}
\ No newline at end of file