Pattern matching does not deal with dependent singleton types in extractors #6130
Comments
|
Imported From: https://issues.scala-lang.org/browse/SI-6130?orig=1 |
|
@hubertp said: object Bug {
object Bar {
def unapply(x: AnyRef): Option[x.type] = x match {
case _ => Some(x)
}
}
def foo(z: AnyRef) {
z match {
case Bar(_) => ()
case _ => ()
}
}
}gives: error: error during expansion of this match (this is a scalac bug).
The underlying error was: type mismatch;
found : Option[<unapply-selector>.type]
required: Option[x.type]
z match {
^
one error found |
|
@adriaanm said: |
|
@retronym said (edited on Apr 16, 2014 8:59:45 AM UTC): object Test {
(null: Any) match {
case Extractor(otherExRep) =>
println(otherExRep)
}
trait T {
type U
}
object Extractor {
def unapply(t: T): Option[t.U] = ???
}
}
/*
{
<synthetic> val o8: Option[<unapply-selector>.U] = Test.this.Extractor.unapply(x2);
if (o8.isEmpty.unary_!)
{
val otherExRep: t.U = o8.get; // type error
matchEnd5(scala.this.Predef.println(otherExRep))
}
else
case7()
}
*/I tried to fix this by sprinking in some missing substitution, but there are deeper problems that get in the way (or, at least, a chain of shallow problems) My attempt and analysis: https://github.com/retronym/scala/compare/ticket;6130?expand=1 See also #7459 |
|
I agree is not a great error message, but I think we'll disagree on what is right :-) The spec says the subpatterns of an extractor pattern are typed with the expected type derived from the unapply's result type. In this case, the pattern In order to allow this pattern to type check, you'd have to widen the type |
|
@adriaanm Thanks for getting back to this. Haven't looked at tricky bug reports like this in ages, so apologies if I'm rusty.
Let's put it this way: this is incomplete type inference, but I concede this incompleteness might be unavoidable or even mandated by the spec. I say this because you're not arguing that the typing derivation I asked for is unsound. And because we need to talk about two subtly different things, so we need proper jargon. As a new incompleteness issue I filed #10503—a simplified version of this without dependent types. But my analysis is still below. With dependent types there seem to be extra issues beyond #10503: singleton types aren't being propagated well (maybe because of the substitution bugs); it also seems Dotty might be running into some of your criticism. If I think about this, it seems unfortunate that the spec (according to your description) mandates a specific algorithmic type rule instead of a declarative one. IIRC I took this idea from some Haskell GADT paper, saying that programmers understand declarative rules better than algorithmic ones—makes sense to me. On the other hand, it's not obvious anyway how to get a reasonable algorithm from the declarative rule I propose—yet, in some simpler cases without singleton types in sight, Dotty manages (sorry to mention!). I'd ask "does the widening have to be unconditional?", but I guess your sentence is pretty strict:
because the expected type is an input. To understand your description: def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => z }I guess then If I think of the declarative type rule I'd like here, it seems that, in general, we want to allow the pattern to have a supertype of the expected type it is typed with. Surprisingly, this fails in Scala. Unsurprisingly, this works in Dotty. Scalac: scala> object &&& { def unapply[A <: AnyRef](a: A): Some[(A, A)] = Some(a, a) }
defined object $amp$amp$amp
scala> class ArrayApply2[T](arr: Exp[Array[T]], idx: Exp[Int]) extends ArrayApply(arr, idx)
defined class ArrayApply2
scala> new ArrayApply2[Int](null, null) match { case ArrayApply(z, i) => z }
<console>:16: error: constructor cannot be instantiated to expected type;
found : ArrayApply[T]
required: ArrayApply2[Int]
new ArrayApply2[Int](null, null) match { case ArrayApply(z, i) => z }
^
scala> (new ArrayApply2[Int](null, null): ArrayApply[Int]) match { case ArrayApply(z, i) => z }
res10: Exp[Array[Int]] = null
Dotty: scala> object &&& { def unapply[A <: AnyRef](a: A): Some[(A, A)] = Some(a, a) }
defined module &&&
scala> class ArrayApply2[T](arr: Exp[Array[T]], idx: Exp[Int]) extends ArrayApply(arr, idx)
defined class ArrayApply2
scala> new ArrayApply2[Int](null, null) match { case ArrayApply(z, i) => z }
val res1: Exp[Array[Int]] = nullAlso, IIUC you're suggesting Scalac is giving type Welcome to Scala 2.12.3 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_144).
Type in expressions for evaluation. Or try :help.
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => y : x.type }
<console>:15: error: constructor cannot be instantiated to expected type;
found : ArrayApply[T]
required: <unapply-selector>.type
def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => y : x.type }
^
<console>:15: error: type mismatch;
found : <unapply-selector>.type with ArrayApply[t]
required: x.type
def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => y : x.type }
^
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & _ => y : x.type }
<console>:15: error: type mismatch;
found : <unapply-selector>.type with ArrayApply[t]
required: x.type
def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & _ => y : x.type }
^
scala> import scala.language.existentials
import scala.language.existentials
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & _ => y }
f: [T <: AnyRef](x: Exp[T])Exp[T] with ArrayApply[t] forSome { type t }
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & _ => y : y.type }
f: [T <: AnyRef](x: Exp[T])y.type forSome { val y: <unapply-selector>.type with ArrayApply[t]; val <unapply-selector>: Exp[T]; type t }For the record, I'm not sure we're happy with Dotty here—though we know Dotty doesn't yet instantiate type variables in patterns properly, especially in the second example (/cc @smarter). It does sound like Dotty is doing the widening you're complaining about— Starting dotty REPL...
Welcome to Scala.next (pre-alpha, git-hash: 21b3149) (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_144).
Type in expressions to have them evaluated.
Type :help for more information.
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => z }
-- Warning: <console>:8:78 -----------------------------------------------------
8 |def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => z }
| ^^^^^^^^^^^^^^^^
| There is no best instantiation of pattern type ArrayApply[T^]
| that makes it a subtype of selector type Exp[T](?1).
| Non-variant type variable T' cannot be uniquely instantiated.
|
| where: ?1 is an unknown value of type Exp[T]
| T is a type in method f with bounds <: AnyRef
| T' is a type variable with constraint
|
| (This would be an error under strict mode)
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => y : x.type }
-- Warning: <console>:8:78 -----------------------------------------------------
8 |def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => y : x.type }
| ^^^^^^^^^^^^^^^^
| There is no best instantiation of pattern type ArrayApply[T^]
| that makes it a subtype of selector type Exp[T](?1).
| Non-variant type variable T' cannot be uniquely instantiated.
|
| where: ?1 is an unknown value of type Exp[T]
| T is a type in method f with bounds <: AnyRef
| T' is a type variable with constraint
|
| (This would be an error under strict mode)
-- [E007] Type Mismatch Error: <console>:8:88 ----------------------------------
8 |def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & ArrayApply(z, i) => y : x.type }
| ^
| found: ArrayApply[t](y)
| required: Exp[T](x)
|
scala> def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & _ => y : x.type }
-- [E007] Type Mismatch Error: <console>:8:73 ----------------------------------
8 |def f[T <: AnyRef](x: Exp[T]) = x match { case (y: ArrayApply[t]) & _ => y : x.type }
| ^
| found: ArrayApply[t](y)
| required: Exp[T](x)
| |
|
👏 Bet that wasn't easy. |
|
Thanks! Indeed, bit of a slog, that was. |
Dependent method types and singleton types allow me to turn this extractor:
into this one, with a more precise type:
(Note that the
<: AnyRefbound is only there to allow usinga.type, so is unnecessary in the first example).However, the new extractor does not work, and Paul Phillips said it's a bug (https://groups.google.com/d/msg/scala-language/gcGGjkDazwE/8nmHdVudE2QJ). For instance, given these declarations:
at the REPL we see that:
Apparently, the dependent method type in the result,
a.typewitha = x: Exp[T], is not resolved toExp[T].The same code works fine with the previous definition of
&:The bug clearly requires dependent method types, but it also seems to require singleton types, since the variation below with dependent method types works fine.
The text was updated successfully, but these errors were encountered: