diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 109929f0c6f5..93f8066d6b9f 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -248,7 +248,18 @@ trait ConstraintHandling {
     override def apply(tp: Type): Type = tp match
       case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) =>
         legalVar(tp)
-      // TypeParamRef can occur in tl bounds
+        // TypeParamRef can occur in tl bounds
+      case tp: TypeVar if tp.isInstantiated =>
+        /* `TypeMap` always strips instantiated type variables in `mapOver`.
+         * We can keep the original type var if its instance is not transformed
+         * by the LevelAvoidMap. This allows for simpler bounds and for
+         * derived skolems (see ApproximatingTypeMap#derivedSkolemType) to
+         * remain the same by keeping their info unchanged. Loosing skolems
+         * in the legalBound computation prevented type vars from being
+         * instantiated with theses skolems, even if they were within the bounds.
+         */
+        val res = apply(tp.instanceOpt)
+        if res eq tp.instanceOpt then tp else res
       case tp: TypeParamRef =>
         constraint.typeVarOfParam(tp) match
           case tvar: TypeVar =>
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index 3ea8b550f160..638455e7f2de 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -119,4 +119,7 @@ i7445b.scala
 
 # more aggresive reduce projection makes a difference
 i15525.scala
+i19955a.scala
+i19955b.scala
+i20053b.scala
 
diff --git a/tests/pos/i19955a.scala b/tests/pos/i19955a.scala
new file mode 100644
index 000000000000..b8ea95d41d24
--- /dev/null
+++ b/tests/pos/i19955a.scala
@@ -0,0 +1,27 @@
+
+trait Summon[R, T <: R]:
+  type Out
+object Summon:
+  given [R, T <: R]: Summon[R, T] with
+    type Out = R
+
+trait DFTypeAny
+trait DFBits[W <: Int] extends DFTypeAny
+class DFVal[+T <: DFTypeAny]
+type DFValAny = DFVal[DFTypeAny]
+type DFValOf[+T <: DFTypeAny] = DFVal[T]
+trait Candidate[R]:
+  type OutW <: Int
+object Candidate:
+  type Aux[R, O <: Int] = Candidate[R] { type OutW = O }
+  given [W <: Int, R <: DFValOf[DFBits[W]]]: Candidate[R] with
+    type OutW = W
+
+extension [L](lhs: L) def foo(using es: Summon[L, lhs.type]): Unit = ???
+extension [L <: DFValAny](lhs: L)(using icL: Candidate[L]) def baz: DFValOf[DFBits[icL.OutW]] = ???
+extension [L <: DFValAny, W <: Int](lhs: L)(using icL: Candidate.Aux[L, W])
+  def bazAux: DFValOf[DFBits[W]] = ???
+
+val x = new DFVal[DFBits[4]]
+val works = x.bazAux.foo
+val fails = x.baz.foo
\ No newline at end of file
diff --git a/tests/pos/i19955b.scala b/tests/pos/i19955b.scala
new file mode 100644
index 000000000000..99e101b312b1
--- /dev/null
+++ b/tests/pos/i19955b.scala
@@ -0,0 +1,17 @@
+
+trait Wrap[W]
+
+trait IsWrapOfInt[R]:
+  type Out <: Int
+given [W <: Int, R <: Wrap[W]]: IsWrapOfInt[R] with
+  type Out = Int
+
+trait IsInt[U <: Int]
+given [U <: Int]: IsInt[U] = ???
+
+extension [L](lhs: L) def get(using ev: IsWrapOfInt[L]): ev.Out = ???
+extension (lhs: Int) def isInt(using IsInt[lhs.type]): Unit = ???
+
+val x: Wrap[Int] = ???
+val works = (x.get: Int).isInt
+val fails = x.get.isInt
diff --git a/tests/pos/i20053b.scala b/tests/pos/i20053b.scala
new file mode 100644
index 000000000000..25180d56bbae
--- /dev/null
+++ b/tests/pos/i20053b.scala
@@ -0,0 +1,22 @@
+
+trait Sub[R, T >: R]
+given [R, T >: R]: Sub[R, T] with {}
+
+trait Candidate[-R]:
+  type OutP
+given [P]: Candidate[Option[P]] with
+  type OutP = P
+
+extension [L](lhs: L)
+  def ^^^[P](rhs: Option[P])
+            (using es: Sub[lhs.type, Any])
+            (using c: Candidate[L])
+            (using check: c.type <:< Any): Option[c.OutP] = ???
+
+val x: Option[Boolean] = ???
+
+val z1 = x ^^^ x // Ok
+val z2 = z1 ^^^ x // Ok
+val zz = ^^^[Option[Boolean]](x ^^^ x)(x) // Ok
+
+val zzz = x ^^^ x ^^^ x // Error before changes