Show GADT bounds in type mismatch message #3990
Conversation
| // | 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.
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.
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.
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.
found: (_$1, _$1)
expected: (_$1, _$2)
The second type parameter of the tuple differs
smarter
force-pushed
the
fix/gadt-error
branch
from
2e8c967 to
8367f08
Compare
| case sym: Symbol => | ||
| ctx.gadt.bounds.contains(sym) && ctx.gadt.bounds(sym) != TypeBounds.empty | ||
| case _ => | ||
| false |
There was a problem hiding this comment.
assert(false, "unreachable")?
smarter
force-pushed
the
fix/gadt-error
branch
from
8367f08 to
65e4ec0
Compare
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).
We no longer convert GADT bounds into normal bounds since scala#3233 was merged.
smarter
force-pushed
the
fix/gadt-error
branch
from
65e4ec0 to
39af805
Compare
| if (ctx.gadt.bounds.contains(sym)) | ||
| sym.info & ctx.gadt.bounds(sym) | ||
| else | ||
| sym.info |
There was a problem hiding this comment.
micro optimisation:
val bounds = ctx.gadt.bounds(sym)
val info = if (bounds != null) sym.info & bounds else sym.infoThere was a problem hiding this comment.
I don't think micro-optimizing error messages is worth it.
| @@ -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.
micro optimisation:
ctx.gadt.bounds(sym) != TypeBounds.empty // since it returns null if not in the gadt bounds mapThere was a problem hiding this comment.
we would also have to check != null
| 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) |
There was a problem hiding this comment.
Do you need to do the intersection? Can you simply return ctx.gadt.bounds(sym)?
There was a problem hiding this comment.
I think so, we used to do something similar in PostTyper.
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).