Skip to content

Commit 321dbb0

Browse files
committed
Fix lampepfl#7044: Added GADT recovery with fallback to default error on failure.
1 parent 03e34a2 commit 321dbb0

File tree

4 files changed

+42
-43
lines changed

4 files changed

+42
-43
lines changed

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -213,21 +213,8 @@ object Inferencing {
213213
mapOver(tp)
214214
}
215215

216-
// private class UpperInstantiator(implicit ctx: Context) extends TypeAccumulator[Unit] {
217-
// def apply(x: Unit, tp: Type): Unit = {
218-
// tp match {
219-
// case tvar: TypeVar if !tvar.isInstantiated =>
220-
// instantiate(tvar, fromBelow = false)
221-
// case _ =>
222-
// }
223-
// foldOver(x, tp)
224-
// }
225-
// }
226-
227216
def process(tp: Type): Type = {
228-
val res = apply(tp)
229-
// if (res && toMaximize) new UpperInstantiator().apply((), tp)
230-
res
217+
apply(tp)
231218
}
232219
}
233220

compiler/src/dotty/tools/dotc/typer/Typer.scala

Lines changed: 27 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -2765,7 +2765,7 @@ class Typer extends Namer
27652765
*/
27662766
def adapt(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean = true)(using Context): Tree = {
27672767
val last = Thread.currentThread.getStackTrace()(2).toString;
2768-
trace/*.force*/(i"adapting (tryGadtHealing=$tryGadtHealing) $tree to $pt\n{callsite: $last}", typr, show = true) {
2768+
trace(i"adapting (tryGadtHealing=$tryGadtHealing) $tree to $pt\n{callsite: $last}", typr, show = true) {
27692769
record("adapt")
27702770
adapt1(tree, pt, locked, tryGadtHealing)
27712771
}
@@ -2775,7 +2775,6 @@ class Typer extends Namer
27752775
adapt(tree, pt, ctx.typerState.ownedVars)
27762776

27772777
private def adapt1(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean)(using Context): Tree = {
2778-
// assert(pt.exists && !pt.isInstanceOf[ExprType])
27792778
assert(pt.exists && !pt.isInstanceOf[ExprType] || ctx.reporter.errorsReported)
27802779
def methodStr = err.refStr(methPart(tree).tpe)
27812780

@@ -3272,6 +3271,7 @@ class Typer extends Namer
32723271
foo = $foo
32733272
pt.isInstanceOf[SelectionProto] = ${pt.isInstanceOf[SelectionProto]}
32743273
ctx.gadt.nonEmpty = ${ctx.gadt.nonEmpty}
3274+
ctx.gadt = ${ctx.gadt.debugBoundsDescription}
32753275
pt.isMatchedBy = ${
32763276
if (pt.isInstanceOf[SelectionProto])
32773277
pt.asInstanceOf[SelectionProto].isMatchedBy(foo).toString
@@ -3316,20 +3316,31 @@ class Typer extends Namer
33163316
def recover(failure: SearchFailureType) =
33173317
{
33183318
debug.println("recover")
3319-
if (isFullyDefined(wtp, force = ForceDegree.all) &&
3320-
ctx.typerState.constraint.ne(prevConstraint)) readapt(tree)
3321-
// else if ({
3322-
// debug.println(i"tryGadtHealing=$tryGadtHealing && \n\tctx.gadt.nonEmpty=${ctx.gadt.nonEmpty}")
3323-
// tryGadtHealing && ctx.gadt.nonEmpty
3324-
// })
3325-
// {
3326-
// debug.println("here")
3327-
// readapt(
3328-
// tree = tpd.Typed(tree, TypeTree(Inferencing.approximateGADT(wtp))),
3329-
// shouldTryGadtHealing = false,
3330-
// )
3331-
// }
3332-
else err.typeMismatch(tree, pt, failure)
3319+
if (isFullyDefined(wtp, force = ForceDegree.all) &&
3320+
ctx.typerState.constraint.ne(prevConstraint)) readapt(tree)
3321+
else if ({
3322+
debug.println(i"tryGadtHealing=$tryGadtHealing && \n\tctx.gadt.nonEmpty=${ctx.gadt.nonEmpty}")
3323+
tryGadtHealing && ctx.gadt.nonEmpty
3324+
})
3325+
{
3326+
debug.println("//try recover with GADT approximation")
3327+
val nestedCtx = ctx.fresh.setNewTyperState()
3328+
val res =
3329+
readapt(
3330+
tree = tpd.Typed(tree, TypeTree(Inferencing.approximateGADT(wtp))),
3331+
shouldTryGadtHealing = false,
3332+
)(using nestedCtx)
3333+
if (!nestedCtx.reporter.hasErrors) {
3334+
nestedCtx.typerState.commit()
3335+
debug.println("// GADT recovery successful")
3336+
res
3337+
} else {
3338+
// otherwise fail with the error that would have been reported without GADT recovery
3339+
debug.println("// GADT recovery failed, falling back to original error")
3340+
err.typeMismatch(tree, pt, failure)
3341+
}
3342+
}
3343+
else err.typeMismatch(tree, pt, failure)
33333344
}
33343345
if ctx.mode.is(Mode.ImplicitsEnabled) && tree.typeOpt.isValueType then
33353346
if pt.isRef(defn.AnyValClass) || pt.isRef(defn.ObjectClass) then

tests/neg/boundspropagation.scala

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -25,19 +25,6 @@ object test3 {
2525
}
2626
}
2727

28-
// Example contributed by Jason.
29-
object test4 {
30-
class Base {
31-
type N
32-
33-
class Tree[-S, -T >: Option[S]]
34-
35-
def g(x: Any): Tree[_, _ <: Option[N]] = x match {
36-
case y: Tree[_, _] => y // error -- used to work (because of capture conversion?)
37-
}
38-
}
39-
}
40-
4128
class Test5 {
4229
"": ({ type U = this.type })#U // error
4330
}

tests/pos/i7044.scala

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
object i7044 {
2+
case class Seg[T](pat:Pat[T], body:T)
3+
4+
trait Pat[T]
5+
object Pat {
6+
case class Expr() extends Pat[Int]
7+
case class Opt[S](el:Pat[S]) extends Pat[Option[S]]
8+
}
9+
10+
def test[T](s:Seg[T]):Int = s match {
11+
case Seg(Pat.Expr(),body) => body + 1
12+
case Seg(Pat.Opt(Pat.Expr()),body) => body.get
13+
}
14+
}

0 commit comments

Comments
 (0)