scala3 icon indicating copy to clipboard operation
scala3 copied to clipboard

Ban classes that incompatibly refine type params

Open dwijnand opened this issue 3 years ago • 2 comments

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.

dwijnand avatar Mar 31 '22 15:03 dwijnand

Can you explain what's the high-level idea? As in, formally state the rules of what is accepted and what is rejected.

LPTK avatar Apr 04 '22 01:04 LPTK

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 avatar Apr 04 '22 16:04 dwijnand

@dwijnand it would be good to have a textual description of the changes and to have Martin's yea/nay on it.

abgruszecki avatar Aug 12 '22 11:08 abgruszecki