From eababc050752220f382b5ec7de1b6cd5354219b5 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Mon, 12 Feb 2018 18:57:24 +0100 Subject: [PATCH 1/2] Show GADT bounds in type mismatch message The inferred GADT bounds can be non-trivial so it makes sense to display them. This commit also showcases the now-improved GADT support in Dotty (both tests/pos/gadt-eval.scala and tests/neg/gadt-eval.scala used to compile, and both compile in Scala 2). --- .../tools/dotc/printing/Formatting.scala | 13 ++++++-- tests/neg/gadt-eval.scala | 33 +++++++++++++++++++ tests/pos/gadt-eval.scala | 19 +++++++++++ 3 files changed, 63 insertions(+), 2 deletions(-) create mode 100644 tests/neg/gadt-eval.scala create mode 100644 tests/pos/gadt-eval.scala diff --git a/compiler/src/dotty/tools/dotc/printing/Formatting.scala b/compiler/src/dotty/tools/dotc/printing/Formatting.scala index e9f88523d8b8..d33e0af00ddb 100644 --- a/compiler/src/dotty/tools/dotc/printing/Formatting.scala +++ b/compiler/src/dotty/tools/dotc/printing/Formatting.scala @@ -168,7 +168,12 @@ object Formatting { case param: TypeParamRef => s"is a type variable${addendum("constraint", ctx.typeComparer.bounds(param))}" case sym: Symbol => - s"is a ${ctx.printer.kindString(sym)}${sym.showExtendedLocation}${addendum("bounds", sym.info)}" + val info = + if (ctx.gadt.bounds.contains(sym)) + sym.info & ctx.gadt.bounds(sym) + else + sym.info + s"is a ${ctx.printer.kindString(sym)}${sym.showExtendedLocation}${addendum("bounds", info)}" case tp: SkolemType => s"is an unknown value of type ${tp.widen.show}" } @@ -183,7 +188,11 @@ object Formatting { def needsExplanation(entry: Recorded) = entry match { case param: TypeParamRef => ctx.typerState.constraint.contains(param) case skolem: SkolemType => true - case _ => false + case sym: Symbol => + ctx.gadt.bounds.contains(sym) && ctx.gadt.bounds(sym) != TypeBounds.empty + case _ => + assert(false, "unreachable") + false } val toExplain: List[(String, Recorded)] = seen.toList.flatMap { diff --git a/tests/neg/gadt-eval.scala b/tests/neg/gadt-eval.scala new file mode 100644 index 000000000000..fad0fc04700e --- /dev/null +++ b/tests/neg/gadt-eval.scala @@ -0,0 +1,33 @@ +sealed trait Exp[T] +case class Lit(value: Int) extends Exp[Int] +case class Pair[A, B](fst: Exp[A], snd: Exp[B]) extends Exp[(A, B)] + +object Test { + def eval[T](e: Exp[T]): T = e match { + case Lit(x) => + x + case Pair(a, b) => + (eval(a), eval(a)) // error: + // -- [E007] Type Mismatch Error: tests/neg/gadt-eval.scala:10:6 ------------------ + // 10 | (eval(a), eval(a)) + // | ^^^^^^^^^^^^^^^^^^ + // | found: (_$1, _$1) + // | required: T + // | + // | where: T is a type in method eval which is an alias of (_$1, _$2) + } + + def eval2[T](e: Exp[T]): T = e match { + case e: Lit => + e.value + case e: Pair[t1, t2] => + (eval(e.fst), eval(e.fst)) // error: + //-- [E007] Type Mismatch Error: tests/neg/gadt-eval.scala:24:6 ------------------ + //24 | (eval(e.fst), eval(e.fst)) + // | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + // | found: (t1, t1) + // | required: T + // | + // | where: T is a type in method eval2 which is an alias of (t1, t2) + } +} diff --git a/tests/pos/gadt-eval.scala b/tests/pos/gadt-eval.scala new file mode 100644 index 000000000000..2cebba3f378d --- /dev/null +++ b/tests/pos/gadt-eval.scala @@ -0,0 +1,19 @@ +sealed trait Exp[T] +case class Lit(value: Int) extends Exp[Int] +case class Pair[A, B](fst: Exp[A], snd: Exp[B]) extends Exp[(A, B)] + +object Test { + def eval[T](e: Exp[T]): T = e match { + case Lit(x) => + x + case Pair(a, b) => + (eval(a), eval(b)) + } + + def eval2[T](e: Exp[T]): T = e match { + case e: Lit => + e.value + case e: Pair[t1, t2] => + (eval(e.fst), eval(e.snd)) + } +} From 39af805e459ce849fe001b50ebb57c9e33b18404 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Mon, 12 Feb 2018 19:11:45 +0100 Subject: [PATCH 2/2] Fix PostTyper doc comment We no longer convert GADT bounds into normal bounds since #3233 was merged. --- compiler/src/dotty/tools/dotc/transform/PostTyper.scala | 2 -- 1 file changed, 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala index a5c32c568687..4cab1bbdea25 100644 --- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala +++ b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala @@ -44,8 +44,6 @@ import reporting.diagnostic.messages.{NotAMember, SuperCallsNotAllowedInline} * (11) Minimizes `call` fields of `Inline` nodes to just point to the toplevel * class from which code was inlined. * - * (12) Converts GADT bounds into normal type bounds - * * The reason for making this a macro transform is that some functions (in particular * super and protected accessors and instantiation checks) are naturally top-down and * don't lend themselves to the bottom-up approach of a mini phase. The other two functions