Add test from i7586

Author: EugeneFlesselle

tests/pos/i7586.scala

@@ -0,0 +1,54 @@
+/*
+sealed trait Nat
+case object Z extends Nat
+case class S[N <: Nat](pred: N) extends Nat
+type Z = Z.type
+
+given [N <: Nat](using n: N): S[N] = S(n)
+given zero: Z = Z
+
+case class Sum[N <: Nat, M <: Nat, R <: Nat](r: R)
+
+given [N <: Nat](using n: N): Sum[Z, N, N] = Sum(n)
+given [N <: Nat, M <: Nat, R <: Nat](
+	using sum: Sum[N, M, R]
+): Sum[S[N], M, S[R]] = Sum(S(sum.r))
+
+def add[N <: Nat, M <: Nat, R <: Nat](n: N, m: M)(using sum: Sum[N, M, R]): R = sum.r
+*/
+
+
+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 = add(Z, S(Z))
+	summon[n1.type <:< S[Z]]
+
+	val n3 = add(S(S(Z)), S(Z))
+	summon[n3.type <:< S[S[S[Z]]]]
+
+	val n3_2 = add(S(Z), S(S(Z)))
+	summon[n3_2.type <:< S[S[S[Z]]]]
+
+