Equality of type projection and existential type

On Sat, Sep 3, 2011 at 10:05 AM, Lars Hupel wrote:
> scala> class Outer { class Inner }
> defined class Outer
>
> Given this definition, I didn't expect that Outer#Inner and o.Inner
> forSome { val o: Outer } are equivalent, only that one of them conforms
> to the other one.
>
> scala> implicitly[<:<[o.Inner forSome { val o: Outer }, Outer#Inner]]
> res3: <:<[o.Inner forSome { val o: Outer },Outer#Inner] =
>
> As expected. But the other way round, I noticed that:
>
> scala> implicitly[Outer#Inner <:< o.Inner forSome { val o: Outer }]
> :9: error: Cannot prove that Outer#Inner <:< Outer#Inner.
>              implicitly[Outer#Inner <:< o.Inner forSome { val o: Outer }]
>
> which is quite strange because apparently the compiler simplifies the
> existential type to the projection type. Obviously, the compiler also
> fails to prove equality:
>
> scala> implicitly[Outer#Inner =:= o.Inner forSome { val o: Outer }]
> :9: error: Cannot prove that Outer#Inner =:= Outer#Inner.
>              implicitly[Outer#Inner =:= o.Inner forSome { val o: Outer }]

Interesting. It _is_ sometimes said that Outer#Inner is equivalent to
o.Inner forSome { val o : Outer }. But that's not what the spec says,
and it's quite clear that that can't be the case: in fact the
equivalence should only work for a _universal_ rather than an
existential quantifier.

Here are a few more examples illustrating that,

scala> implicitly[(o.Inner forSome { val o : Outer }) <:< Outer#Inner]
res24: <:<[o.Inner forSome { val o: Outer },Outer#Inner] =

scala> val o1 = new Outer
o1: Outer = Outer@d551e1

scala> val o2 = new Outer
o2: Outer = Outer@15fc2d5

scala> implicitly[o1.Inner <:< Outer#Inner]
res25: <:<[o1.Inner,Outer#Inner] =

scala> implicitly[o2.Inner <:< Outer#Inner]
res26: <:<[o2.Inner,Outer#Inner] =

These are all exactly the results we would expect if Outer#Inner were
defined as the (hypothetical, not current Scala) o.Inner forAll { val
o : Outer }.

Somewhat relatedly, I've come around to the idea that the rendering
for Java raw types as parametrized types with a hidden existential is
back to front: I think they should actually be treated as parametrized
types with a hidden *universal* quantifier, ie. java.util.List should
be interpreted as java.util.List[T] forAll { type T } rather than as
java.util.List[T] forSome { type T } as it currently is.

Cheers,

Miles

On Sat, Sep 3, 2011 at 10:05 AM, Lars Hupel wrote:
> scala> class Outer { class Inner }
> defined class Outer
>
> Given this definition, I didn't expect that Outer#Inner and o.Inner
> forSome { val o: Outer } are equivalent, only that one of them conforms
> to the other one.
>
> scala> implicitly[<:<[o.Inner forSome { val o: Outer }, Outer#Inner]]
> res3: <:<[o.Inner forSome { val o: Outer },Outer#Inner] =
>
> As expected. But the other way round, I noticed that:
>
> scala> implicitly[Outer#Inner <:< o.Inner forSome { val o: Outer }]
> :9: error: Cannot prove that Outer#Inner <:< Outer#Inner.
>              implicitly[Outer#Inner <:< o.Inner forSome { val o: Outer }]
>
> which is quite strange because apparently the compiler simplifies the
> existential type to the projection type. Obviously, the compiler also
> fails to prove equality:
>
> scala> implicitly[Outer#Inner =:= o.Inner forSome { val o: Outer }]
> :9: error: Cannot prove that Outer#Inner =:= Outer#Inner.
>              implicitly[Outer#Inner =:= o.Inner forSome { val o: Outer }]

There's definitely something strange going on here,

scala> class Outer { class Inner }
defined class Outer

scala> val o = new Outer
o: Outer = Outer@7b1b33

scala> val i = new o.Inner
i: o.Inner = Outer$Inner@1a13207

scala> val i1 : Outer#Inner = i
i1: Outer#Inner = Outer$Inner@1a13207

scala> val i2 : x.Inner forSome { val x : Outer } = i
:10: error: type mismatch;
found : x.Inner
required: x.Inner forSome { val x: => Outer }
val i2 : x.Inner forSome { val x : Outer } = i
^
:10: error: type mismatch;
found : o.Inner
required: x.Inner forSome { val x: => Outer }
val i2 : x.Inner forSome { val x : Outer } = i
^

scala> val i3 = (i : x.Inner forSome { val x : Outer })
i3: Outer#Inner = Outer$Inner@1a13207

scala> type OI = x.Inner forSome { val x : Outer }
defined type alias OI

scala> val i4 : OI = i
i3: OI = Outer$Inner@1a13207

scala> val i5 = (i : OI)
i4: Outer#Inner = Outer$Inner@1a13207

I can't see any obvious reason for the difference between i2 and i3
here, and any reason at all for the difference between i2 and i4.

Cheers,

Miles

> scala> class Outer { class Inner }
> defined class Outer
>
> scala> val o = new Outer
> o: Outer = Outer@7b1b33
>
> scala> val i = new o.Inner
> i: o.Inner = Outer$Inner@1a13207
>
> scala> val i1 : Outer#Inner = i
> i1: Outer#Inner = Outer$Inner@1a13207
>
> scala> val i2 : x.Inner forSome { val x : Outer } = i
> :10: error: type mismatch;
> found : x.Inner
> required: x.Inner forSome { val x: => Outer }
> val i2 : x.Inner forSome { val x : Outer } = i
> ^
> :10: error: type mismatch;
> found : o.Inner
> required: x.Inner forSome { val x: => Outer }
> val i2 : x.Inner forSome { val x : Outer } = i
> ^
>
> scala> type OI = x.Inner forSome { val x : Outer }
> defined type alias OI
>
> scala> val i4 : OI = i
> i3: OI = Outer$Inner@1a13207
>
> I can't see any obvious reason for the difference between i2 and i3
> here, and any reason at all for the difference between i2 and i4.

I noticed the difference between i2 and i4, too, although I couldn't say
it's not an error in parsing, mostly because of that:

> implicitly[x.Inner forSome { val x : Outer } <:< Outer#Inner]
:1: error: ']' expected but identifier found.

After a quick search in Jira I couldn't find any related bugs, so I
think there should be one.

On Sun, Sep 4, 2011 at 8:58 AM, Lars Hupel wrote:
>> scala> class Outer { class Inner }
>> defined class Outer
>>
>> scala> val o = new Outer
>> o: Outer = Outer@7b1b33
>>
>> scala> val i = new o.Inner
>> i: o.Inner = Outer$Inner@1a13207
>>
>> scala> val i1 : Outer#Inner = i
>> i1: Outer#Inner = Outer$Inner@1a13207
>>
>> scala> val i2 : x.Inner forSome { val x : Outer } = i
>> :10: error: type mismatch;
>>  found   : x.Inner
>>  required: x.Inner forSome { val x: => Outer }
>>        val i2 : x.Inner forSome { val x : Outer } = i
>>            ^
>> :10: error: type mismatch;
>>  found   : o.Inner
>>  required: x.Inner forSome { val x: => Outer }
>>        val i2 : x.Inner forSome { val x : Outer } = i
>>                                                     ^
>>
>> scala> type OI = x.Inner forSome { val x : Outer }
>> defined type alias OI
>>
>> scala> val i4 : OI = i
>> i3: OI = Outer$Inner@1a13207
>>
>> I can't see any obvious reason for the difference between i2 and i3
>> here, and any reason at all for the difference between i2 and i4.
>
> I noticed the difference between i2 and i4, too, although I couldn't say
> it's not an error in parsing, mostly because of that:
>
>> implicitly[x.Inner forSome { val x : Outer } <:< Outer#Inner]
> :1: error: ']' expected but identifier found.

That looks fine ... you just need to enclose the LHS of the <:<
operator in brackets.

> After a quick search in Jira I couldn't find any related bugs, so I
> think there should be one.

Cheers,

Miles