-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Show GADT bounds in type mismatch message #3990
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. micro optimisation: val bounds = ctx.gadt.bounds(sym)
val info = if (bounds != null) sym.info & bounds else sym.info There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't think micro-optimizing error messages is worth it. |
||
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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. micro optimisation: ctx.gadt.bounds(sym) != TypeBounds.empty // since it returns null if not in the gadt bounds map There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. we would also have to check != null |
||
case _ => | ||
assert(false, "unreachable") | ||
false | ||
} | ||
|
||
val toExplain: List[(String, Recorded)] = seen.toList.flatMap { | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This overall testcase is cool! Wondering how to explain where these type variables come from. They come from the match (hard to show), and they show up in the types of a and b, which is easier to show, most easily by showing the whole typing context. That might be too much, but I think GHC sometimes does it, and both Agda and Coq absolutely do it and have to do it. Not sure where to draw a line. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah, if you can think of a good way to display this information I'm interested, I haven't checked what other compilers do. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't get it. If "T is a type in method eval which is an alias of (_$1, _$2)", why is there a type error? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
The second type parameter of the tuple differs |
||
} | ||
|
||
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) | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)) | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you need to do the intersection? Can you simply return
ctx.gadt.bounds(sym)
?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think so, we used to do something similar in PostTyper.