diff --git a/community-build/community-projects/libretto b/community-build/community-projects/libretto
index d229f3ccb9c4..64de079d5a7c 160000
--- a/community-build/community-projects/libretto
+++ b/community-build/community-projects/libretto
@@ -1 +1 @@
-Subproject commit d229f3ccb9c49aa3b0fef1b3f7425e986155cc97
+Subproject commit 64de079d5a7cf3efe3345421ac3e375a718f57f7
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index 7e35b8be8caa..fd8507a7d961 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -383,8 +383,9 @@ object Inferencing {
   def isSkolemFree(tp: Type)(using Context): Boolean =
     !tp.existsPart(_.isInstanceOf[SkolemType])
 
-  /** The list of uninstantiated type variables bound by some prefix of type `T` which
-   *  occur in at least one formal parameter type of a prefix application.
+  /** The list of uninstantiated type variables bound by some prefix of type `T` or
+   *  by arguments of an application prefix, which occur at least once as a formal type parameter
+   *  of an application either from a prefix or an argument of an application node.
    *  Considered prefixes are:
    *    - The function `f` of an application node `f(e1, .., en)`
    *    - The function `f` of a type application node `f[T1, ..., Tn]`
@@ -392,8 +393,10 @@ object Inferencing {
    *    - The result expression `e` of a block `{s1; .. sn; e}`.
    */
   def tvarsInParams(tree: Tree, locked: TypeVars)(using Context): List[TypeVar] = {
-    @tailrec def boundVars(tree: Tree, acc: List[TypeVar]): List[TypeVar] = tree match {
-      case Apply(fn, _) => boundVars(fn, acc)
+    def boundVars(tree: Tree, acc: List[TypeVar]): List[TypeVar] = tree match {
+      case Apply(fn, args) =>
+        val argTpVars = args.flatMap(boundVars(_, Nil))
+        boundVars(fn, acc ++ argTpVars)
       case TypeApply(fn, targs) =>
         val tvars = targs.filter(_.isInstanceOf[InferredTypeTree]).tpes.collect {
           case tvar: TypeVar
@@ -406,16 +409,18 @@ object Inferencing {
       case Block(_, expr) => boundVars(expr, acc)
       case _ => acc
     }
-    @tailrec def occurring(tree: Tree, toTest: List[TypeVar], acc: List[TypeVar]): List[TypeVar] =
+    def occurring(tree: Tree, toTest: List[TypeVar], acc: List[TypeVar]): List[TypeVar] =
       if (toTest.isEmpty) acc
       else tree match {
-        case Apply(fn, _) =>
+        case Apply(fn, args) =>
+          val argsOcc = args.flatMap(occurring(_, toTest, Nil))
+          val argsNocc = toTest.filterNot(argsOcc.contains)
           fn.tpe.widen match {
             case mtp: MethodType =>
-              val (occ, nocc) = toTest.partition(tvar => mtp.paramInfos.exists(tvar.occursIn))
-              occurring(fn, nocc, occ ::: acc)
+              val (occ, nocc) = argsNocc.partition(tvar => mtp.paramInfos.exists(tvar.occursIn))
+              occurring(fn, nocc, occ ::: argsOcc ::: acc)
             case _ =>
-              occurring(fn, toTest, acc)
+              occurring(fn, argsNocc, argsOcc ::: acc)
           }
         case TypeApply(fn, targs) => occurring(fn, toTest, acc)
         case Select(pre, _) => occurring(pre, toTest, acc)
diff --git a/tests/pos/i18578.scala b/tests/pos/i18578.scala
new file mode 100644
index 000000000000..ee0ec6628c66
--- /dev/null
+++ b/tests/pos/i18578.scala
@@ -0,0 +1,17 @@
+
+trait Animal
+class Dog extends Animal
+
+trait Ev[T]
+
+given Ev[Dog] = ???
+given Ev[Animal] = ???
+given[T: Ev]: Ev[Set[T]] = ???
+
+def f[T: Ev](v: T): Unit = ???
+
+def main =
+	val s = Set(new Dog)
+	f(s) // Ok
+	f(Set(new Dog)) // Error before changes: Ambiguous given instances: both given instance given_Ev_Dog and given instance given_Ev_Animal match type Ev[T]
+
diff --git a/tests/pos/i7586.scala b/tests/pos/i7586.scala
new file mode 100644
index 000000000000..364c99478337
--- /dev/null
+++ b/tests/pos/i7586.scala
@@ -0,0 +1,38 @@
+
+trait Nat
+case object Z extends Nat
+case class S[N <: Nat](pred: N) extends Nat
+
+type Z = Z.type
+given zero: Z = Z
+given succ[N <: Nat](using n: N): S[N] = S(n)
+
+case class Sum[N <: Nat, M <: Nat, R <: Nat](result: R)
+
+given sumZ[N <: Nat](using n: N): Sum[Z, N, N] = Sum(n)
+given sumS[N <: Nat, M <: Nat, R <: Nat](
+	using sum: Sum[N, M, R]
+): Sum[S[N], M, S[R]] = Sum(S(sum.result))
+
+def add[N <: Nat, M <: Nat, R <: Nat](n: N, m: M)(
+	using sum: Sum[N, M, R]
+): R = sum.result
+
+case class Prod[N <: Nat, M <: Nat, R <: Nat](result: R)
+
+
+@main def Test: Unit =
+
+	val n1: S[Z] = add(Z, S(Z))
+	summon[n1.type <:< S[Z]] // OK
+
+	val n3: S[S[S[Z]]] = add(S(S(Z)), S(Z))
+	summon[n3.type <:< S[S[S[Z]]]] // Ok
+
+	val m3_2 = add(S(Z), S(S(Z)))
+	summon[m3_2.type <:< S[S[S[Z]]]] // Error before changes: Cannot prove that (m3_2 : S[S[Nat]]) <:< S[S[S[Z]]]
+
+	val m4_2 = add(S(Z), S(S(S(Z))))
+	summon[m4_2.type <:< S[S[S[S[Z]]]]]
+
+