From 67ae35782ae306aef368c29c63d46b8dcfc8d82c Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Sun, 26 Nov 2023 22:06:09 +0100 Subject: [PATCH 1/6] Instantiate type vars which occur in arguments applications --- .../dotty/tools/dotc/typer/Inferencing.scala | 18 +++++++++++------- tests/pos/i18578.scala | 17 +++++++++++++++++ 2 files changed, 28 insertions(+), 7 deletions(-) create mode 100644 tests/pos/i18578.scala diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index 7e35b8be8caa..eb36cae3e0ab 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala @@ -392,8 +392,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 +408,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..3dfbb9208c25 --- /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) // WORKS + f(Set(new Dog)) // FAILS + // instantiates to From 1df7d83f9e605c05298e01bafbc047c191f21af2 Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Mon, 27 Nov 2023 16:01:14 +0100 Subject: [PATCH 2/6] Add test from i7586 --- tests/pos/i18578.scala | 6 +++--- tests/pos/i7586.scala | 38 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 3 deletions(-) create mode 100644 tests/pos/i7586.scala diff --git a/tests/pos/i18578.scala b/tests/pos/i18578.scala index 3dfbb9208c25..ee0ec6628c66 100644 --- a/tests/pos/i18578.scala +++ b/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] + 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]]]]] + + From 700fa5e625fdcbaca7767f9175de5a1ef875f53a Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Mon, 4 Dec 2023 17:02:44 +0100 Subject: [PATCH 3/6] Fix libretto community-project --- community-build/community-projects/libretto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/community-build/community-projects/libretto b/community-build/community-projects/libretto index d229f3ccb9c4..e0ea45b36739 160000 --- a/community-build/community-projects/libretto +++ b/community-build/community-projects/libretto @@ -1 +1 @@ -Subproject commit d229f3ccb9c49aa3b0fef1b3f7425e986155cc97 +Subproject commit e0ea45b36739f36aba7babb5cee361d67b91b79b From a77a69a38d9c36f35517b2b37f318a97242b870a Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Thu, 7 Dec 2023 15:13:47 +0100 Subject: [PATCH 4/6] mend --- community-build/community-projects/libretto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/community-build/community-projects/libretto b/community-build/community-projects/libretto index e0ea45b36739..1210480c0100 160000 --- a/community-build/community-projects/libretto +++ b/community-build/community-projects/libretto @@ -1 +1 @@ -Subproject commit e0ea45b36739f36aba7babb5cee361d67b91b79b +Subproject commit 1210480c010013dd974d4994238d9b121afa6dc6 From 5e8f8f61ac763078128bd95d54aef505b1f684d1 Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Thu, 7 Dec 2023 15:28:58 +0100 Subject: [PATCH 5/6] Community-build update --- community-build/community-projects/libretto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/community-build/community-projects/libretto b/community-build/community-projects/libretto index 1210480c0100..64de079d5a7c 160000 --- a/community-build/community-projects/libretto +++ b/community-build/community-projects/libretto @@ -1 +1 @@ -Subproject commit 1210480c010013dd974d4994238d9b121afa6dc6 +Subproject commit 64de079d5a7cf3efe3345421ac3e375a718f57f7 From 21520f4e896967fa6fa13caa7a8d27717ab76126 Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Mon, 29 Jan 2024 15:28:24 +0100 Subject: [PATCH 6/6] update doc --- compiler/src/dotty/tools/dotc/typer/Inferencing.scala | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index eb36cae3e0ab..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]`