Fix #11178: remove unsound tweak for F-bounds in isInstanceOf check #11768
Conversation
liufengyun
changed the title
This reverts scala#9789. We have made several improvements to F-bounds, the unsound tweak is no longer needed.
It is possible that a subtype of MdNode extends Seq.
It's unclear why the operation is needed.
| P1 <:< X | ||
| withMode(Mode.GadtConstraintInference) { | ||
| TypeComparer.constrainPatternType(P1, X, widenParams = false) | ||
| debug.println(TypeComparer.explained(_.constrainPatternType(P1, X, widenParams = false))) |
There was a problem hiding this comment.
I think I understand the intent here, but it's a bit surprising that we don't widen the params, given that doing so is necessary for soundness. What would be a motivating example for not widening them here?
There was a problem hiding this comment.
The motivation for not widening is something specific to the algorithm: here for P1 = pre.F[Xs], all Xs are type variables. We want the Xs to be constrained.
There was a problem hiding this comment.
I feel very happy the work on the GADT makes the checking so elegant that we remove a lot of ad-hoc tweaks. The fact that the algorithm is simpler and it found more bugs in the compiler gives more confidence.
There was a problem hiding this comment.
One example is the following:
// tests/neg-custom-args/isInstanceOf/JavaSeqLiteral.scala
trait Tree[-T]
class JavaSeqLiteral[-T] extends Tree[T]
trait Type
class DummyTree extends JavaSeqLiteral[Any]
def foo1(tree: Tree[Type]) =
tree.isInstanceOf[JavaSeqLiteral[Type]]In checking whether the test tree.isInstanceOf[JavaSeqLiteral[Type]] is realizable, we want to constrain JavaSeqLiteral[X] <: Tree[Type], such that we can infer X = Type and JavaSeqLiteral[X] <:< JavaSeqLiteral[Type].
If we perform widening, we will get X = Nothing, and we don't have JavaSeqLiteral[X] <:< JavaSeqLiteral[Type] any more.
There was a problem hiding this comment.
Ok, I think what we're doing here is sound, but with small changes we could easily make it unsound. I'll need to add a comment explaining what's going on, and then we can merge the PR.
There was a problem hiding this comment.
Yes, I'll add a comment explaining the code.
There was a problem hiding this comment.
Comment added in aa296ba
Fix #11178: remove unsound tweak for F-bounds
This reverts #9789. We have made several improvements to F-bounds,
the unsound tweak is no longer needed.