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

Casts inserted when pattern matching for equality on singletons are unsound #1503

Closed
scabug opened this Issue Nov 10, 2008 · 33 comments

Comments

Projects
None yet
4 participants
@scabug

scabug commented Nov 10, 2008

I've added a test to pending/run/castsingleton.scala:

object Test extends Application {
  case class L();
  object N extends L();

  def empty(xs : L) : Unit = xs match {
    case x@N => println(x); println(x);
  }

  empty(L())
} 

The problem is that the compiler inserts a cast of xs to N.type, which is unsound: The pattern match will succeed for any L, because N == L().

@scabug

This comment has been minimized.

scabug commented Nov 10, 2008

@scabug

This comment has been minimized.

scabug commented Nov 10, 2008

@DRMacIver said:
Incidentally, this is going to be very annoying to fix. It's totally unclear what type x should have in this match.

@scabug

This comment has been minimized.

scabug commented Nov 12, 2008

@DRMacIver said:
After some discussion the conclusion is that the specced behaviour for this is broken.

The suggested fix is that stable identifier patterns defined behaviour will be modified so that something matches it if and only if it is equal to that stable identifier and is an instance of the static type of that identifier. Thus in this case L() will not match the pattern N because it is not an instance of N.type.

@scabug

This comment has been minimized.

scabug commented Jul 5, 2009

@paulp said:
Implemented as described by DRMacIver in r18215. (Assuming it works out, I think the spec remains to be updated.)

@scabug

This comment has been minimized.

scabug commented Jul 12, 2009

@odersky said:
First, we should not close a ticket without updating the spec. Second, I am having second thoughts about this. The proposed change adds a non-obvious type test to something which should be really very fast. Most of the time the type test is not needed. I am also not sure whether the fix is sufficient to cover all soundness problems. So I tried to have a look at the spec, but to my surprise found that
variable binds x@p are not covered! I have now tried to come up with wordings. Paul, if you agree let's implement this instead of the current fix.

\subsection{Pattern Binders}
\label{sec:pattern-binders}
\syntax
\begin{lstlisting}
Pattern2 ::= varid `@' Pattern3
\end{lstlisting}
A pattern binder \lstinline|$$x$$@$$p$$| consists of a pattern variable $$x$$ and a
pattern $$p$$. The type of the variable $$x$$ is the static type $$T$$ of the pattern $$p$$.
This pattern matches any value $$v$$ matched by the pattern $$p$$,
provided the run-time type of $$v$$ is also an instance of $$T$$,
and it binds the variable name to that value.

(The differences are, obviously, that the runtime test could apply to more than just equality checks (needs to me analyzed carefully, so that we generate the right amount of runtime checks), and that runtime checks are only needed when an `@' is present.

@scabug

This comment has been minimized.

scabug commented Jul 12, 2009

@paulp said:
Yes, shouldn't have closed the ticket.

I also thought of this approach, but I did not think you'd want to have different semantics for matching solely based on the presence/absence of a binding - that is, if I'm understanding correctly we're saying given this:

    case N => true
case x @ N => true

the first will match and the second won't, given the same scrutinee of L() from the test case.

I am assuming that is indeed what you mean - I am all for it and will implement it in the near future.

@scabug

This comment has been minimized.

scabug commented Jul 13, 2009

@odersky said:
Yes, that is indeed a disadvantage. I also thought of another approach, which is cleaner, but the worry is that it might break old code: We need to work out carefully what is known about the type of a variable in a binder. The variable certainly has the pattern's expected type. And some patterns also contribute type information. The intersection of these two types would then be the type of the variable.

For instance:

val foo: List[String]

foo match {
case n @ Nil => ... // expected type: List[String], pattern type: ?
case c: ::[_] => // expected type: List[String], pattern type: ::[?]
...
}

In the first case, the best type for n is List[String], the expected type.
In the first case it would be List[String] with ::[?], and by some other piece
of not yet implemented type checking inference we could infer this to be equal to
::[String].

I think this would be the most logical approach. But I am not sure how many old programs would break, because some variables would get assigned weaker types than before.

Anyway, it looks more and more like there is a paper in this. Things are far from trivial.

@scabug

This comment has been minimized.

scabug commented Sep 26, 2009

@paulp said:
Noting for the record that I reverted this patch after martin reported it changed the behavior of this snippet, because Byte doesn't have the static type of Char:

val buf: Array[Byte]

def processVerbatim(i: Int, end: String): Int = {
      val END = end.charAt(0)
    
     def processCode(pre: String, i: Int): Int = {...
        buf(i) match {
          case END if startsWith(i, end) =>
            // return
}                                                                               
    

Interestingly I can't reproduce this in a simple example, but I did reproduce the behavior in verbfilterScala.scala, and I did verify that reverting the patch for this ticket restored the original matching behavior.

@scabug

This comment has been minimized.

scabug commented Oct 21, 2009

@paulp said:
This is now implemented as martin describes, with an instance check only when a variable binding exists, in r19170. The spec has been updated (section 8.1.3) and after sleeping on it I don't have any better ideas, so I am closing this ticket with a clean conscience.

@scabug

This comment has been minimized.

scabug commented Dec 5, 2012

@paulp said:
I don't know how this even looked fixed.

case object Foo {
  def bippy = 1
  override def equals(other: Any) = true
}

object Test extends App {
  ("": Any) match { case p @ Foo => p.bippy }
}
[paulp@conifer Dec05 (master)]$ scala3 Test
java.lang.ClassCastException: java.lang.String cannot be cast to Foo$
	at Test$delayedInit$body.apply(a.scala:8)
	at scala.Function0$class.apply$mcV$sp(Function0.scala:40)
	at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:12)
	at scala.App$$anonfun$main$1.apply(App.scala:71)
	at scala.App$$anonfun$main$1.apply(App.scala:71)
	at scala.collection.immutable.List.foreach(List.scala:294)
@scabug

This comment was marked as outdated.

scabug commented Feb 2, 2013

@adriaanm said:
probably too big a change for 2.10.1

@scabug

This comment has been minimized.

scabug commented Dec 10, 2013

@retronym said:
Just to add an example that doesn't require extending a case class or writing a constant equals:

scala> (IndexedSeq(): Any) match { case n @ Nil => n.mapConserve(x => x) }
java.lang.ClassCastException: scala.collection.immutable.Vector cannot be cast to scala.collection.immutable.List
@scabug

This comment has been minimized.

scabug commented Dec 10, 2013

@paulp said:
Geez, you don't even need mapConserve. Pattern matcher will be glad to arrange the CCE for you. Full service! Very classy.

scala> (Vector(): Any) match { case n @ Nil => n }
java.lang.ClassCastException: scala.collection.immutable.Vector cannot be cast to scala.collection.immutable.Nil$
  ... 32 elided
@scabug

This comment has been minimized.

scabug commented Jan 28, 2014

@adriaanm said:
Fix originally proposed for #5024: https://github.com/adriaanm/scala/commits/ticket-5024, see also #4577.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@adriaanm said:
This only breaks programs built on a type-lie, as far as I can tell.

I've implemented Martin's alternative proposal, which calls for determining the type implied by a pattern matching a certain value. Usually, this is the pattern's type because pattern matching implies instance-of checks.

However, Stable Identifier and Literal patterns are matched using ==, which does not imply a type for the binder that binds the matched value. The behavior change due to this fix is that programs that used to crash with a CCE now get a weaker type instead (and no cast). They may still type check, or they may not.

case x@Foo => x should be changed to case x: Foo.type => x if type propagation is important -- NOTE that I also intend to fix #4577, so that matching will use eq for singleton types, not == (so that the types are not a lie).

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@paulp said:
I very much question the suggestion that this program is "built on a type lie" or that changing the inferred type from a List of Ints to Any isn't going to break anything.

object Test {
  def f(xs: Any) = xs match {
    case xs @ Nil => xs
    case _        => List[Int]()
  }
}
@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@adriaanm said:
Well, Nil == Vector(), but this is a lie: Vector(): List[Int], wouldn't you (and your example above) say?

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@paulp said:
It is, but that's scala's bug, not theirs. The author of that method wrote it in in a perfectly obvious way, which has worked forever; it's probably the explicitly recommended way in one or more official scala things. They only ever call the method with Lists, not Vectors, which they've never heard of. It will never fail - until it is broken out from under them to fix a bug not of their making and which they could never have anticipated.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@adriaanm said:
I don't think we recommend matching on any when a list is all you care about. In any case, this is why I submitted the pr before adding more tests. I expect the discussion to last longer than it takes me to write those.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@paulp said:
"Any" is for contrast. The example can be made arbitrarily realistic, but one can hope for effort on the receiving side as well.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@adriaanm said:
I'm not trying to be facetious. It would work if the expected type was a list. The whole compiler + lib requires two changes. To improve on the case where any is the expected type, we could improve that automatically to the lub of the expected types of the cases.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@paulp said (edited on Jan 29, 2014 3:59:00 AM UTC):
It is a systemic risk to assume things based on how they impact the compiler and library, a codebase written by a very small number of people with lots of overlap in their habits and methods.

I think the responsible thing to do is issue a warning when the inferred type as-calculated-until-now differs from the inferred type as-calculated-after-now. It is the silent changes in behavior which can easily accompany any change in type inference which I think unreasonable in this case, because people generally find ClassCastExceptions all by themselves if the code path is ever exercised. That means that in the short run the only likely effect of changing this will be to make code which used to compile stop compiling and to make code which used to work stop working.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@adriaanm said:
Fair enough. I still wonder about the ratio would-work-but-no-longer-typechecks / potential-crash-prevented-by-type-error.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@retronym said:
-Xstrict-inference might be a good place for this one if its too risky for broader release.

Just as a reminder, we also need to fix the regression noted in #5900/#7886 before 2.11.0-RC1. That might involve rolling back the changes of #7886 (unsound pattern inference). That patch actually only superfically improved the state of play.

These sort of unresolved questions suggests to me that the schedule for RC1 isn't realistic and that we need another month or so.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@adriaanm said:
I was thinking -Xfuture for this one.

PS: I'm against further delays. Let's fix what we can (only) fix in 2.11.0 now, reverting where necessary. Everything else goes to 2.11.1 or 2.12.

@scabug

This comment has been minimized.

scabug commented Jan 29, 2014

@scabug

This comment has been minimized.

scabug commented Feb 5, 2014

@paulp said:
Moors - have you looked at SI-7714? Does your proposed change handle those cases?

@scabug

This comment has been minimized.

scabug commented Feb 5, 2014

@adriaanm said:
I had not. Thanks for the pointer. Will add it to the investigation for my next available bugfixing slot.

@scabug

This comment has been minimized.

scabug commented Feb 19, 2014

@adriaanm said (edited on Feb 25, 2014 8:46:29 PM UTC):
Xlint warning for 2.11: scala/scala#3559

@scabug

This comment has been minimized.

scabug commented Nov 24, 2015

Brian Kent (bkent314) said:
Is it possible for the compiler to offer more guidance in addition to the current warnings?

For example, in doing case x@N => ..., the compiler could offer:
bq. you probably want case x:N.type => ...

Currently it just says something is dangerous buy offers no alternatives.

@scabug

This comment has been minimized.

scabug commented Jul 22, 2016

@milessabin said:
In 2.12.x the example in this ticket produces a non-exhaustive match warning,

> scala
[info] Running scala.tools.nsc.MainGenericRunner -usejavacp                                                                                 
Welcome to Scala 2.12.0-20160722-172732-9ee8124 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_102).                                        
Type in expressions for evaluation. Or try :help.                                                                                           
                                                                                                                                            
scala> :paste
// Entering paste mode (ctrl-D to finish)                                                                                                   
                                                                                                                                            
object Test extends App {                                                                                                                   
  case class L();                                                                                                                           
  object N extends L();                                                                                                                     
                                                                                                                                            
  def empty(xs : L) : Unit = xs match {                                                                                                     
    case x@N => println(x); println(x);                                                                                                     
  }                                                                                                                                         
                                                                                                                                            
  empty(L())                                                                                                                                
}                                                                                                                                           
                                                                                                                                            
// Exiting paste mode, now interpreting.                                                                                                    
                                                                                                                                            
<console>:15: warning: match may not be exhaustive.
It would fail on the following input: L()
         def empty(xs : L) : Unit = xs match {
                                    ^
defined object Test
@SethTisue

This comment has been minimized.

Member

SethTisue commented Apr 17, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment