From 042b7e37a283dea00705ed2d41d2a944dcab0032 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 11 Jul 2022 14:53:21 +0800 Subject: [PATCH 1/5] insert GADT casts for if branches --- compiler/src/dotty/tools/dotc/typer/Typer.scala | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 8bd30e6f404a..35e4447945cb 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1135,6 +1135,12 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer case elsep: untpd.If => isIncomplete(elsep) case _ => false + def gadtAdaptBranch(tree: Tree, branchPt: Type): Tree = + TypeComparer.testSubType(tree.tpe.widenExpr, branchPt) match { + case CompareResult.OKwithGADTUsed => tree.cast(branchPt) + case _ => tree + } + val branchPt = if isIncomplete(tree) then defn.UnitType else pt.dropIfProto val result = @@ -1148,7 +1154,13 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer val elsep0 = typed(tree.elsep, branchPt)(using cond1.nullableContextIf(false)) thenp0 :: elsep0 :: Nil }: @unchecked - assignType(cpy.If(tree)(cond1, thenp1, elsep1), thenp1, elsep1) + + val resType = thenp1.tpe | elsep1.tpe + + val thenp2 = gadtAdaptBranch(thenp1, resType) + val elsep2 = gadtAdaptBranch(elsep1, resType) + + cpy.If(tree)(cond1, thenp2, elsep2).withType(resType) def thenPathInfo = cond1.notNullInfoIf(true).seq(result.thenp.notNullInfo) def elsePathInfo = cond1.notNullInfoIf(false).seq(result.elsep.notNullInfo) From a6a943f223a8a2df62bdac57048c23b46d6d8b93 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 27 Jun 2022 20:18:08 +0800 Subject: [PATCH 2/5] add GADT approximation of the stable type in GADT casting --- compiler/src/dotty/tools/dotc/typer/Typer.scala | 8 +++++++- tests/pos/gadt-cast-singleton.scala | 13 +++++++++++++ tests/pos/i14776-patmat.scala | 15 +++++++++++++++ tests/pos/i14776.scala | 16 ++++++++++++++++ 4 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 tests/pos/gadt-cast-singleton.scala create mode 100644 tests/pos/i14776-patmat.scala create mode 100644 tests/pos/i14776.scala diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 35e4447945cb..f5b7cb194502 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -3779,7 +3779,13 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer // The check "safeToInstantiate" in `maximizeType` works to prevent unsound GADT casts. val target = if tree.tpe.isSingleton then - val conj = AndType(tree.tpe, pt) + // In the target type, when the singleton type is intersected, we also intersect + // the GADT-approximated type of the singleton to avoid the loss of + // information. See #14776. + val gadtApprox = Inferencing.approximateGADT(tree.tpe.widen) + gadts.println(i"gadt approx $wtp ~~~ $gadtApprox") + val conj = + AndType(AndType(tree.tpe, gadtApprox), pt) if tree.tpe.isStable && !conj.isStable then // this is needed for -Ycheck. Without the annotation Ycheck will // skolemize the result type which will lead to different types before diff --git a/tests/pos/gadt-cast-singleton.scala b/tests/pos/gadt-cast-singleton.scala new file mode 100644 index 000000000000..57cd2bc8f578 --- /dev/null +++ b/tests/pos/gadt-cast-singleton.scala @@ -0,0 +1,13 @@ +enum SUB[-A, +B]: + case Refl[S]() extends SUB[S, S] + +trait R { + type Data +} +trait L extends R + +def f(x: L): x.Data = ??? + +def g[T <: R](x: T, ev: T SUB L): x.Data = ev match + case SUB.Refl() => + f(x) diff --git a/tests/pos/i14776-patmat.scala b/tests/pos/i14776-patmat.scala new file mode 100644 index 000000000000..570e8cc64bac --- /dev/null +++ b/tests/pos/i14776-patmat.scala @@ -0,0 +1,15 @@ +trait T1 +trait T2 extends T1 + +trait Expr[T] { val data: T = ??? } +case class Tag2() extends Expr[T2] + +def flag: Boolean = ??? + +def foo[T](e: Expr[T]): T1 = e match { + case Tag2() => + flag match + case true => new T2 {} + case false => e.data +} + diff --git a/tests/pos/i14776.scala b/tests/pos/i14776.scala new file mode 100644 index 000000000000..262a3750ff73 --- /dev/null +++ b/tests/pos/i14776.scala @@ -0,0 +1,16 @@ +trait T1 +trait T2 extends T1 + +trait Expr[T] { val data: T = ??? } +case class Tag2() extends Expr[T2] + +def flag: Boolean = ??? + +def foo[T](e: Expr[T]): T1 = e match { + case Tag2() => + if flag then + new T2 {} + else + e.data +} + From 95193e7d83a298b7c03389be6510fb806ad8b240 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 11 Jul 2022 17:11:42 +0800 Subject: [PATCH 3/5] refactor GADT cast insertion into a separate method --- .../src/dotty/tools/dotc/typer/Typer.scala | 62 ++++++++++++------- 1 file changed, 39 insertions(+), 23 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index f5b7cb194502..c7cc8b2b9601 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1137,7 +1137,8 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer def gadtAdaptBranch(tree: Tree, branchPt: Type): Tree = TypeComparer.testSubType(tree.tpe.widenExpr, branchPt) match { - case CompareResult.OKwithGADTUsed => tree.cast(branchPt) + case CompareResult.OKwithGADTUsed => + insertGadtCast(tree, tree.tpe.widen, branchPt) case _ => tree } @@ -1157,8 +1158,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer val resType = thenp1.tpe | elsep1.tpe - val thenp2 = gadtAdaptBranch(thenp1, resType) - val elsep2 = gadtAdaptBranch(elsep1, resType) + val thenp2 :: elsep2 :: Nil = + (thenp1 :: elsep1 :: Nil) map { t => + gadtAdaptBranch(t, resType) + }: @unchecked cpy.If(tree)(cond1, thenp2, elsep2).withType(resType) @@ -3775,26 +3778,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer gadts.println(i"unnecessary GADTused for $tree: ${tree.tpe.widenExpr} vs $pt in ${ctx.source}") res } => - // Insert an explicit cast, so that -Ycheck in later phases succeeds. - // The check "safeToInstantiate" in `maximizeType` works to prevent unsound GADT casts. - val target = - if tree.tpe.isSingleton then - // In the target type, when the singleton type is intersected, we also intersect - // the GADT-approximated type of the singleton to avoid the loss of - // information. See #14776. - val gadtApprox = Inferencing.approximateGADT(tree.tpe.widen) - gadts.println(i"gadt approx $wtp ~~~ $gadtApprox") - val conj = - AndType(AndType(tree.tpe, gadtApprox), pt) - if tree.tpe.isStable && !conj.isStable then - // this is needed for -Ycheck. Without the annotation Ycheck will - // skolemize the result type which will lead to different types before - // and after checking. See i11955.scala. - AnnotatedType(conj, Annotation(defn.UncheckedStableAnnot)) - else conj - else pt - gadts.println(i"insert GADT cast from $tree to $target") - tree.cast(target) + insertGadtCast(tree, wtp, pt) case _ => //typr.println(i"OK ${tree.tpe}\n${TypeComparer.explained(_.isSubType(tree.tpe, pt))}") // uncomment for unexpected successes tree @@ -4225,4 +4209,36 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer EmptyTree else typedExpr(call, defn.AnyType) + /** Insert GADT cast to target type `pt` on the `tree` + * so that -Ycheck in later phases succeeds. + * The check "safeToInstantiate" in `maximizeType` works to prevent unsound GADT casts. + */ + private def insertGadtCast(tree: Tree, wtp: Type, pt: Type)(using Context): Tree = + val target = + if tree.tpe.isSingleton then + // In the target type, when the singleton type is intersected, we also intersect + // the GADT-approximated type of the singleton to avoid the loss of + // information. See #14776. + val gadtApprox = Inferencing.approximateGADT(wtp) + gadts.println(i"gadt approx $wtp ~~~ $gadtApprox") + val conj = + TypeComparer.testSubType(gadtApprox, pt) match { + case CompareResult.OK => + // GADT approximation of the tree type is a subtype of expected type under empty GADT + // constraints, so it is enough to only have the GADT approximation. + AndType(tree.tpe, gadtApprox) + case _ => + // In other cases, we intersect both the approximated type and the expected type. + AndType(AndType(tree.tpe, gadtApprox), pt) + } + if tree.tpe.isStable && !conj.isStable then + // this is needed for -Ycheck. Without the annotation Ycheck will + // skolemize the result type which will lead to different types before + // and after checking. See i11955.scala. + AnnotatedType(conj, Annotation(defn.UncheckedStableAnnot)) + else conj + else pt + gadts.println(i"insert GADT cast from $tree to $target") + tree.cast(target) + end insertGadtCast } From 3d52d1e2b77b73e50287a4b633f542e16e88cc26 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 11 Jul 2022 17:25:16 +0800 Subject: [PATCH 4/5] add test case for #14776 See https://github.com/lampepfl/dotty/issues/14776#issuecomment-1171346127. --- tests/pos/gadt-cast-if.scala | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/pos/gadt-cast-if.scala diff --git a/tests/pos/gadt-cast-if.scala b/tests/pos/gadt-cast-if.scala new file mode 100644 index 000000000000..02a02f040cc1 --- /dev/null +++ b/tests/pos/gadt-cast-if.scala @@ -0,0 +1,12 @@ +trait Expr[T] + case class IntExpr() extends Expr[Int] + + def flag: Boolean = ??? + + def foo[T](ev: Expr[T]): Int | T = ev match + case IntExpr() => + if flag then + val i: T = ??? + i + else + (??? : Int) From 2255fdb67ac8bc11cac883f69f6667f99d6fb5b8 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 12 Jul 2022 15:58:54 +0800 Subject: [PATCH 5/5] add documentation and point to #15646 --- compiler/src/dotty/tools/dotc/typer/Typer.scala | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index c7cc8b2b9601..3aacd6659b79 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1135,6 +1135,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer case elsep: untpd.If => isIncomplete(elsep) case _ => false + // Insert a GADT cast if the type of the branch does not conform + // to the type assigned to the whole if tree. + // This happens when the computation of the type of the if tree + // uses GADT constraints. See #15646. def gadtAdaptBranch(tree: Tree, branchPt: Type): Tree = TypeComparer.testSubType(tree.tpe.widenExpr, branchPt) match { case CompareResult.OKwithGADTUsed => @@ -1157,9 +1161,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer }: @unchecked val resType = thenp1.tpe | elsep1.tpe - val thenp2 :: elsep2 :: Nil = (thenp1 :: elsep1 :: Nil) map { t => + // Adapt each branch to ensure that their types conforms to the + // type assigned to the if tree by inserting GADT casts. gadtAdaptBranch(t, resType) }: @unchecked @@ -4218,7 +4223,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer if tree.tpe.isSingleton then // In the target type, when the singleton type is intersected, we also intersect // the GADT-approximated type of the singleton to avoid the loss of - // information. See #14776. + // information. See #15646. val gadtApprox = Inferencing.approximateGADT(wtp) gadts.println(i"gadt approx $wtp ~~~ $gadtApprox") val conj =