| [#1193] | project: compiler | priority: low | category: bug | |
|---|---|---|---|---|
| submitter | assigned to | status | date submitted | |
| Martin | Adriaan | open | 2007-06-29 15:20:28.0 | |
| subject | Higher kinded existential types have problems. | |||
| code |
class C[T](x: T)
object existentials {
val x = { class D[T]; new C(new D[Int]) }
}
|
|||
| what happened | C:\scala\test\files\run>java -Xms20m -Xmx256m -ea scala.tools.nsc.Main -d \classes existentials.scala -explaint\
ypes
existentials.scala:86: error: type mismatch;
found : C[D(in object Test)[Int]]
required: C[D(in value x)[Int]] forSome { type D(in value x)[T] <: AnyRef with ScalaObject }
val x = { class D[T]; new C(new D[Int]) }
^
C[D(in object Test)[Int]] < C[D(in value x)[Int]] forSome { type D(in value x)[T] <: AnyRef with ScalaObject }?
\
C[D(in object Test)[Int]] < C[?*D(in value x)[T]]?
?*D(in value x)[T] < D(in object Test)[Int]?
true
D(in object Test)[Int] < ?*D(in value x)[T]?
true
true
[T]AnyRef with ScalaObject = D(in value x)[T]?
false
D(in object Test)[Int] < >: [T]Nothing <: [T]AnyRef with ScalaObject?
false
[T]Nothing < D(in object Test)[Int]?
true
D(in object Test)[Int] < [T]AnyRef with ScalaObject?
false
false
one error found
|
|||
| what expected | Successful compilation. The -explaintypes trace gives some clue what goes wrong:
The type checker needs to prove
C[D(in object Test)[Int]] < C[D(in value x)[Int]] forSome { type D(in value x)[T] <: AnyRef with ScalaObject }?
To do that, it converts the right hand side to a type variable (here named ?*D)
C[D(in object Test)[Int]] < C[?*D(in value x)[T]]?Solving this equation yields a solution of D[Int] for ?*D. This is already wrong; it should be just D. Incidentally, the solve method in nsc is exactly the same which is used for inferring type parameters -- it was moved from Infer to Types. Then, the type checker tries to prove that the inferred solution D[Int] conforms to the type variable bounds which are [T] >: Nothing <: AnyRef with ScalaObjectand that fails, of course, because the bounds are higher-kinded but the type is not. Btw if you want more info there are two commented lines in the case for ExistentialType in method isSubType0 in Types.scala:
case (_, ExistentialType(tparams2, res2)) =>
val tvars = tparams2 map (tparam => new TypeVar(tparam.tpe, new TypeConstraint))
val ires2 = res2.instantiateTypeParams(tparams2, tvars)
(tp1 <:< ires2) && {
// println("solve: "+tparams2)
solve(tvars, tparams2, tparams2 map (x => 0), false)
// println("check bounds: "+tparams2+" aginst "+(tvars map (_.constr.inst)))
isWithinBounds(NoPrefix, NoSymbol, tparams2, tvars map (_.constr.inst))
}
If you uncomment these you see exactly what the result of solve is.
|
|||
| [back to overview] | ||||
| Adriaan edited on 2007-06-29 16:07:36.0 |
On first exploration, it seems relevant to note that this compiles:
class C[T](x: T)
object existentials {
val x: C[SomeD[Int]] forSome { type SomeD[x] } = { class D[T]; new C(new D[Int]) }
}
I haven't looked at the code yet, but my guess would be that SomeD[T] is inferred as a kind-* type applied to some unknown T, instead of the higher-kinded SomeD. I hope my intuition turns out to be wrong, as fixing higher-order type inference is going to be nontrivial (for me, at least).. I'll report back once I actually looked at the code ;-)
|