Prune impossible types from exhaustivity checker #3574
Conversation
| NoType | ||
| } else { | ||
| result | ||
| } | ||
| } |
There was a problem hiding this comment.
In the check, there's a facility named implementability from a contributor which does more or less the same thing. What do you think we can generalise/adapt implementability to handle the case?
In particular, I think it's good to rename it to def inhabited(tp: Type): Boolean, and it should be able to handle the current case as well. WDYT?
There was a problem hiding this comment.
I think implementability computes if a type can be implemented by other types (singleton types can't!), while inhabited would need to check if there could actually exists an instance of that type, so I'm not sure two logics can be merged.
@AleksanderBG what's your opinion on that?
There was a problem hiding this comment.
I think implementability should be refactored to have the semantics of inhabited. According to the core algorithm of exhaustivity check, it should only depend on the semantics of def inhabited(tp: Type): Boolean.
There was a problem hiding this comment.
@OlivierBlanvillain I believe @liufengyun is correct - the function can be safely changed to check if a type is inhabited instead. This won't change the result for and-types, which is the only result intersectUnrelatedAtomicTypes should care about. I considered a similar refactoring myself when working on #3454. With the benefit of hindsight, type inhabitation is a far more generic notion and I should've tried to implement it from the beginning.
The exhaustivity checker sometimes looks for impossible types.
The test case added by this PR is an example taken from the shapeless test suite where a sealed trait is extended in two different scopes. The added case classes
OneandTwocan only appear withing objectAtoms01andAtoms02respectively. On master the exhaustivity checker reports missing cases of the following form:PathVariantDefns.Atom2 & PathVariantDefns.Atoms01.type(PathVariantDefns.Atoms01).Two(_). Given thatPathVariantDefns.Atoms01.typeis the type of an object, the intersection between this type and any unrelated type is always empty. This PR adds a check toinstantiatethat detect and remove these cases.@liufengyun WDYT?