Skip to content
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

Merged
merged 1 commit into from Feb 15, 2021

Conversation

dwijnand
Copy link
Member

@dwijnand dwijnand commented Feb 2, 2021

@scala-jenkins scala-jenkins added this to the 2.13.5 milestone Feb 2, 2021
@dwijnand
Copy link
Member Author

dwijnand commented Feb 2, 2021

Very similar to #9472.

@SethTisue
Copy link
Member

SethTisue commented Feb 2, 2021

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.

@dwijnand
Copy link
Member Author

dwijnand commented Feb 2, 2021

The fishy bit, IMO, is the indirection of P <: Petrol.type - there's no reason for that not to be inlined in the parameter type. So instead of can make a PetroleumBasedPowerSource sealed trait, with Petrol and Coal as case object subclasses, make PetroleumBasedPowerSource the upper bound of the type parameter and double check again.

Copy link
Member

@lrytz lrytz left a 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(_).

@dwijnand
Copy link
Member Author

dwijnand commented Feb 3, 2021

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:

reachability, vars:
V1: Vehicle{type A = P} ::= Bus | Car | null// Set(Bus, Bicycle, null, Car) // = x1

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:

trying to reach:
  And(Set(Not(V1=null#1), V1=Bus#3))
under prefix:
  And(Set(Or(Set(V1=Bus#3, V1=Car#2, V1=null#1)), AtMostOne(List(V1=Bus#3, V1=Car#2, V1=null#1))))
  Or(Set(V1=null#1, Not(V1=Car#2)))
reached model:
  V1=Car#2 -> false
  V1=null#1 -> false
  V1=Bus#3 -> true
var assignments:
V1(=x1: Vehicle{type A = P}) == (Bus)  != (Car, null)

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:

trying to reach:
  V1=Bicycle#4
under prefix:
  And(Set(Or(Set(V1=Bus#3, V1=Car#2, V1=null#1)), AtMostOne(List(V1=Bus#3, V1=Car#2, V1=null#1))))
  Or(Set(V1=null#1, Not(V1=Car#2)))
  Or(Set(V1=null#1, Not(V1=Bus#3)))
reached model:
  V1=Car#2 -> false
  V1=Bus#3 -> false
  V1=null#1 -> true
  V1=Bicycle#4 -> true
var assignments:
V1(=x1: Vehicle{type A = P}) == (null, Bicycle)  != (Car, Bus)

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... 🙄

        // should never be more than one value in trues...

@dwijnand
Copy link
Member Author

dwijnand commented Feb 3, 2021

First of all, there's a disagreement on what the variable can be:

reachability, vars:
V1: Vehicle{type A = P} ::= Bus | Car | null// Set(Bus, Bicycle, null, Car) // = x1

The domain knows it can't be Bicycle, but the variables constants still contains the Bicycle constant.

This comes from registering the variable = constant equalities from the case defs, i.e. the actual case Bicycle:

      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:

test/files/neg/t9657.scala:14: warning: unreachable code
    case Bus(_)  => Bus(100) // was: "unreachable code" warning 1
                       ^

is because there the SAT solving fails instantly:

reachability, vars: V1: Vehicle{type A = P} ::= null// Set(Bicycle, Car, Bus, null) // = x1
equality axioms:
  And(Set(Or(Set(V1=null#1))))
trying to reach:
  And(Set(Not(V1=null#1), V1=Bus#3))
under prefix:
  V1=null#1
  Or(Set(V1=null#1, Not(V1=Car#2)))

If V1 is null, can it be (non-null) Bus? No, unreachable.

Where does V1=null come from? Well it's Or(Set(V1=null#1, Not(V1=Car#2))) except here without the Car part, because it doesn't consider Car to be a subtype of Vehicle { type A = P } with the P <: Petrol.type skolem.

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.

@dwijnand dwijnand force-pushed the patmat-unreachable-refinement branch from 93ed083 to 3fa823b Compare February 3, 2021 16:08
@dwijnand
Copy link
Member Author

dwijnand commented Feb 3, 2021

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... 🙄

        // should never be more than one value in trues...

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 null, within the domain of Vehicle, and Bicycle as in the ValueConst Bicycle.

Tough... I think I'll have to park this detail if/until I get smarter and/or more knowledgeable.

@lrytz
Copy link
Member

lrytz commented Feb 4, 2021

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.

@dwijnand
Copy link
Member Author

dwijnand commented Feb 4, 2021

there's no reason for that not to be inlined in the parameter type. So instead of can make a PetroleumBasedPowerSource sealed trait, with Petrol and Coal as case object subclasses, make PetroleumBasedPowerSource the upper bound of the type parameter and double check again.

I've changed my patch to hand this (via deSkolemize), but I'm not sure about it...

@dwijnand
Copy link
Member Author

dwijnand commented Feb 4, 2021

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?

@dwijnand dwijnand requested a review from lrytz February 4, 2021 12:53
@joroKr21
Copy link
Member

This still fails: https://scastie.scala-lang.org/WgY7KC87QeeGv9RPbA29Yw (reported on the shapeless Discord channel)

@joroKr21
Copy link
Member

joroKr21 commented Nov 24, 2021

I tried changing it to approximateAbstracts instead, because the upper bound makes sense only in covariant positions.
But then the warning flipped from unreachable code to non-exhaustive match 🤔

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
5 participants