Fix #1754: Don't narrow GADTs to lower bounds #3918
Conversation
There was a problem hiding this comment.
Hello, and thank you for opening this PR! 🎉
All contributors have signed the CLA, thank you! ❤️
Commit Messages
We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).
Please stick to these guidelines for commit messages:
- Separate subject from body with a blank line
- When fixing an issue, start your commit message with
Fix #<ISSUE-NBR>:- Limit the subject line to 72 characters
- Capitalize the subject line
- Do not end the subject line with a period
- Use the imperative mood in the subject line ("Added" instead of "Add")
- Wrap the body at 80 characters
- Use the body to explain what and why vs. how
adapted from https://chris.beams.io/posts/git-commit
Have an awesome day! ☀️
|
test performance please |
|
performance test scheduled: 1 job(s) in queue, 1 running. |
|
Performance test finished successfully: Visit http://dotty-bench.epfl.ch/3918/ to see the changes. Benchmarks is based on merging with master (5b1b747) |
|
test performance please |
|
performance test scheduled: 1 job(s) in queue, 0 running. |
odersky
changed the title
|
Performance test finished successfully: Visit http://dotty-bench.epfl.ch/3918/ to see the changes. Benchmarks is based on merging with master (5b1b747) |
|
test performance please |
|
performance test scheduled: 1 job(s) in queue, 0 running. |
|
Performance test finished successfully: Visit http://dotty-bench.epfl.ch/3918/ to see the changes. Benchmarks is based on merging with master (5b1b747) |
| * binders in `t` are maintained by rewrapping binders around the type tree. | ||
| * E.g. if `t` is `C[t @ (>: L <: H)]`, replace with | ||
| * `t @ TC[_ >: L <: H]`. The body of the binder `t` is now wrong, but this does | ||
| * not matter, as we only need the info of `t`. |
There was a problem hiding this comment.
I understand what the code does but I'm confused by the documentation :). What are C and TC here? Are you referring to two differents t when you say "t is C[t @ (>: L <: H)]" ? The comment also says that we rewrap binders around the type tree but the code wraps the type tree with an annotation, not a bind.
| def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean = | ||
| if (tycon2bounds.lo eq tycon2bounds.hi) | ||
| if (tyconIsTypeRef) recur(tp1, tp2.superType) | ||
| else isSubApproxHi(tp1, tycon2bounds.lo.applyIfParameterized(args2)) |
There was a problem hiding this comment.
Is subapprox needed here given that tycon2bounds.lo eq tycon2bounds.hi ?
| @@ -826,6 +826,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling { | |||
| false | |||
| } else isSubType(tp1, tp2, approx.addLow) | |||
|
|
|||
| def isSubApproxHi(tp1: Type, tp2: Type): Boolean = | |||
| (tp2 ne NothingType) && isSubType(tp1, tp2, approx.addHigh) | |||
There was a problem hiding this comment.
Is the Nothing check an optimization? Any chance it could do the wrong thing if tp1 is a refinement of Nothing like Nothing { type T } ?
|
After rebasing, the bytecode test for efficient try/catch added in #3929 started failing. I pushed a commit to fix this by adding a |
An empty type bounds as a signal to suppress checking does not work if the argument type is higher-kinded. Using NoType avoids this problem.
Needs to be classified as a Num + AST node. Was misclassified before which lead to a crash in scanTrees. This needs a bump of the major version of Tasty.
In a type pattern, a wildcard argument and a type variable needs to be treated the same.
I.e. it should make no difference if I have
C[_ >: L <: H]
or
C[t >: L <: H]
where `t` is unused. Previously, the two constructs had largely different codepaths with
different things that failed and worked. This fix is necessary to mitigate the fix for
scala#1754. The latter fix uncovered several problems with the way wildcard arguments in
patterns were treated.
The change also uncovered a problem in transforms: FirstTransform eliminates all type
nodes wnd with it any binders bound type symbols. This means that subsequently patVars
is wrong, and therefore a TreeTypeMap over a pattern will no longer duplicate pattern-
bound type variables. This caused Ycheck to fail after TailRec.
The fix is to keep pattern bound type variables around in an internal annotation, which
is understood by patVars.
neg/i1754.scala succeeded because a GADT bound for `A` in `A <: B` was narrowed to the lower bound of `B` (which was nothing) instead of `B` itself. Fixing this uncovered several other problems that were hidden by the overly aggressive narrowing "feature".
Don't narrow GADT bounds or constraint if compared types are imprecise. Narrowing GADT bounds to imprecise types is unsound. Narrowing constraints to imprecise types loses possible types.
With the new info about approximations it's no longer needed.
Passing it as an additional parameter seemed to cause a slight (~2%) performance degradation.
toTypeTree now wraps TypeTrees types with an annotation in some cases.
The fix of scala#3627 got lost when merging the GADT subtype changes.
|
I am going to merge now because other PR #3841 depends on the fixes here. |
neg/i1754.scala succeeded because a GADT bound for
AinA <: Bwas narrowed to the lower bound of
B(which wasNothing) instead ofBitself. Fixing this uncovered several other problems that werehidden by the overly aggressive narrowing "feature".
In the end the PR had to do a major cleanup so that now type bounds and type
variables in patterns are treated the same. I.e. it makes no difference whether
one writes a type pattern
C[_ >: L <: H]orC[t >: L <: H]wheretis otherwisenot used.
It also involved a major refactoring in TypeComparer to make it harder to accidentally narrow to bounds that are too tight.
Based on #3889.