Add test from i7586

Author: EugeneFlesselle

tests/pos/i18578.scala

@@ -12,6 +12,6 @@ def f[T: Ev](v: T): Unit = ???
 
 def main =
 	val s = Set(new Dog)
-//	f(s) // WORKS
-	f(Set(new Dog)) // FAILS
-	// instantiates to
+	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]
+

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]]]]]
+
+