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

nested type inference not so good #7714

Open
scabug opened this issue Aug 1, 2013 · 6 comments
Open

nested type inference not so good #7714

scabug opened this issue Aug 1, 2013 · 6 comments

Comments

@scabug
Copy link

@scabug scabug commented Aug 1, 2013

Some[Any]?

class A {
  // Inferred type is Some[Any]
  def f1(x: Any) = x match { case y @ Some(Some(Some(_: String))) => y }
}
@scabug
Copy link
Author

@scabug scabug commented Aug 1, 2013

Loading

@scabug
Copy link
Author

@scabug scabug commented Aug 5, 2013

@retronym said (edited on Aug 5, 2013 1:28:21 PM UTC):
Isn't this as expected/specced? Type inference flows from the scrutinee's type.

If the case class is polymorphic, then its type parame- ters are instantiated so that the instantiation of c conforms to the expected type of the pattern. The instantiated formal parameter types of c’s primary constructor are then taken as the expected types of the component patterns p1, ..., pn. The pattern matches all objects created from constructor invocations c(v1, ..., vn) where each element pattern pi matches the corresponding value vi .

So this infers Some[String]:

class A {
  // Inferred type is Some[String]
  def f1(x: Any) = (x: Option[String]) match { case y @ Some(Some(_: String)) => y }
}

I'll reclassify this as "improvement" for now but I don't really see how we could change this.

Loading

@scabug
Copy link
Author

@scabug scabug commented Aug 5, 2013

@paulp said (edited by @retronym on Aug 5, 2013 2:30:53 PM UTC):
I don't consider the spec of much relevance when considering how to do things well. How is a pattern of the form 'Some(Some(Some(z)))' ever going to match a value which is not of the form 'Some(Some(Some(z)))' ?

Loading

@scabug
Copy link
Author

@scabug scabug commented Aug 5, 2013

@paulp said:
Also, and not that I expect soundness to suddenly be a subject of interest, but this is a soundness issue (that's how I encountered it.) Patterns cannot be typed this way.

case class Som[A](f: A => A)

object Test {
  def f(x: Any) = x match { case Som(f) => f }
  def g(x: Int): Int = x

  def main(args: Array[String]): Unit = {
    val x = Som[Int](g)
    val y = f(x)
    y("")
    // java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
  }
}

Loading

@scabug
Copy link
Author

@scabug scabug commented Aug 5, 2013

@paulp said:
To elaborate a bit more (and regardless of what the spec says) the expected type of a constructor pattern should be the intersection of the known type (the scrutinee) and the minimum type of a match, in this case Cell[]. Typing 'case Cell()' with pt=Any gives the typer the impression that no restrictions are necessary - but this is not true when there are bindings.

object Test {
  case class Cell[A](var x: A)
  def f1(x: Any)        = x match { case y @ Cell(_) => y }       // Inferred type is Cell[Any] -- unsound
  def f2[A](x: Cell[A]) = x match { case Cell(y @ Cell(_)) => y } // Inferred type is Cell[Any] -- unsound
  def f3(x: Cell[_])    = x match { case y @ Cell(_) => y }       // Inferred type is Cell[_]
  def f4[A](x: Cell[A]) = x match { case y @ Cell(_) => y }       // Inferred type is Cell[A]
}

As is so often true in our codebase, this has all been done before: see propagateKnownTypes in Checkable.scala. 80% of the code related to inferring the types of patterns is duplicative with 80% of the code related to assessing the checkability of types of patterns.

Loading

@scabug
Copy link
Author

@scabug scabug commented Aug 8, 2013

@paulp said:
Here's another one which might make one question the optimality of the current approach. And it infers the same with an invariant Some, which leaves it saying that T=Any and T=Int in the same T-invariant expression.

object Test {
  // Infers (Some[Any], Int)
  def f(p: Any) = p match { case x @ Some(y @ 5) => ((x, y)) }
}

Loading

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

Successfully merging a pull request may close this issue.

None yet
2 participants