scala3
scala3 copied to clipboard
Ban classes that incompatibly refine type params
Where "incompatibly" means outside of sub/supertypes. Intending to resolve #11834. Actually, it's resolving what the "Towards Improved GADT Reasoning in Scala" paper calls "an Old Paradox". (cc @LPTK and @Blaisorblade).
But I had to change the check because invariant refinement only was too strict for some legitimate cases, from the various strawman collection ideas in the test suite. So I came up with another way of checking, which seems to pass all the tests, which compares the combined basetype with the basetype without any parts of the type the involve the middle class.
Sent a draft for some early feedback on how best to do the baseTypeWithout part. Now I need to make use of this ban in GADT reasoning, see the tests I copied into disabled.
Can you explain what's the high-level idea? As in, formally state the rules of what is accepted and what is rejected.
Not as of yet. As in, I have something that accepts the right classes and rejects the wrong ones, but I'm not sure how to describe it in words. I'm working on the failures in the real scala 2.13 collections (as opposed to the strawman collection tests I handle already) which might change the test. Ideally in a way which makes the test simpler and therefore easier to describe.
@dwijnand it would be good to have a textual description of the changes and to have Martin's yea/nay on it.