New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Enumerate subtypes by approximating type skolems to their upper bound #9479
Conversation
Very similar to #9472. |
Related to #9472, yes, but that one fixes a pretty easy-to-understand bug, whereas here, the example code in scala/bug#9657 seems rather esoteric and has a lot of moving parts. So it's hard for me to convince myself that this is both correct and complete, but on the other hand, it's esoteric enough that I'm inclined to shrug if all the tests still pass. I guess my main review question: how sure are we that the original bug report is minimized? If a simpler test case can be constructed, I think that would be valuable. If not, oh well. |
The fishy bit, IMO, is the indirection of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this looks good.
Do you have an explanation why adding a case Bicycle
is not marked as unreachable? enumerateSubtypes
seems to correctly return Bus(_), Car(_)
.
I hadn't yet studied the reachability logic that layers on top of the rest of the patmat/SAT logic, so I went ahead and did that. I'm going to record my notes, as it's been taxing enough for one day. Here's where things go wonky: First of all, there's a disagreement on what the variable can be:
The domain knows it can't be Bicycle, but the variables constants still contains the Bicycle constant. When it's looping case-by-case to see if they're reachable, it starts correctly:
English: if V1 must be Bus, Car xor null, and it's not Car, can V1 be a Bus? Yes, if V1 is Bus, that's satisfied. Then a wild Bicycle reappears:
English: if V1 (same as before) must be Bus, Car xor null, and it's not Car AAAAND it's not Bus, can it be Bicycle? Yes, if V1 is both the null and non-null Bicycle at the same time... 🙄
|
This comes from registering the variable = constant equalities from the case defs, i.e. the actual object gatherEqualities extends PropTraverser {
override def apply(p: Prop) = p match {
case Eq(v, NullConst) if !modelNull => vars += v // not modeling equality to null
case Eq(v, c) => vars += v; v.registerEquality(c)
case _ => super.apply(p)
}
} And the reason before this patch we got:
is because there the SAT solving fails instantly:
If V1 is null, can it be (non-null) Bus? No, unreachable. Where does I guess at least I feel less concerned about the domain being a subset and not equal to the variable consts. But something is going wrong as the solver is assigning V1 to a constant it can't be. |
93ed083
to
3fa823b
Compare
Ah, I see. It's not obvious from the debug text, but it's not Bicycle the type, it's Bicycle the value. So it's Tough... I think I'll have to park this detail if/until I get smarter and/or more knowledgeable. |
Thanks! It sounds like with enough time you can work your way through; in any case the fix in this PR seems right, and the wild Bicycle appearing is a separate issue. |
I've changed my patch to hand this (via deSkolemize), but I'm not sure about it... |
Have a look... The test case comes from chatting about Seth about whether the original test case is minimised enough and/or makes sense. I wrote what I felt was a slightly more reasonable reason to run into the original problem ("less fishy") and it ended up opening a can of worms. There's a pun, for @som-snytt, the pun-maestro: What came first? The fishy code or the can of worms? |
d14f642
to
3fa823b
Compare
This still fails: https://scastie.scala-lang.org/WgY7KC87QeeGv9RPbA29Yw (reported on the shapeless Discord channel) |
I tried changing it to |
Fixes scala/bug#9657