SI-8177 co-evolve more than just RefinedTypes

[adriaanm]

[Rebase and improvement of #3482]

asSeenFrom produced a typeref of the shape T'#A where A referred to a symbol
defined in a T of times past.

More precisely, the TypeRef case of TypeMap's mapOver correctly modified a prefix
from having an underlying type of { type A = AIn } to { type A = Int },
with a new symbol for A (now with info Int), but the symbol in the outer
TypeRef wasn't co-evolved (so it still referred to the A in { type A = AIn }
underlying the old prefix).

coEvolveSym used to only look at prefixes that were directly RefinedTypes,
but this bug shows they could also be SingleType/ThisTypes with an underlying RefinedType,
so we look for a prefix's for a refinement class for a type symbol instead.

Review by @retronym

[adriaanm]

thanks for pushing this a bit further, @paulp & @retronym -- looks like I found the right balance. :fingerscrossed:

[adriaanm]

Cleaned up the test cases in the last commit a bit.

[adriaanm]

FWIW, the tests pass locally

[retronym]

LGTM

[adriaanm]

The IDE failure is because the jenkins slaves are overloaded and the IDE's scalacheck tests are timing out

[adriaanm]

I'll rebuild the ide job individually. It should be fine.

[paulp]

At some point I offered a variation of pos/t8177.scala which at the time didn't compile. I don't see it. It had one extra line and added a type alias. Is that somewhere to be found?

[paulp]

It IS compiling with this PR, assuming I remember it correctly. But since at one point it wasn't, maybe throw it into the test case mix.

// exercise coevolveSym: SingleType with an underlying RefinedType
trait Thing { type A }
object IntThing extends Thing { type A = Int }
object ThingHolder { type Alias[AIn] = Thing { type A = AIn } }

// The following erroneously failed with  error: method f overrides nothing.
// because asSeenFrom produced a typeref of the shape T'#A where A referred to a symbol defined in a T of times past
// More precisely, the TypeRef case of TypeMap's mapOver correctly modified prefix
// from having an underlying type of { type A = Ain } to { type A = Int }, with a new symbol for A (now with info Int),
// but the symbol in the outer type ref wasn't co-evolved (so it still referred to the { type A = AIn } underlying the old prefix)
// coEvolveSym used to only look at prefixes that were directly RefinedTypes, but they could also be SingleTypes with an underlying RefinedType
class View[AIn](val in: ThingHolder.Alias[AIn]) {          def f(p: in.A): in.A = p }
class SubView extends View[Int](IntThing)       { override def f(p: in.A): in.A = p }

[adriaanm]

Sorry, I must have missed that one somehow. I'll add it an trigger a rebuild that way, then.

[adriaanm]

i christened it t8177b

[paulp]

The comment with that test case enclosed began "Tsk Tsk Dude", and here I thought that would be memorable.

[adriaanm]

My suppressing those is another interesting insight into my psychology, I guess.

[paulp]

Happily everyone can have their own definition of "interesting".

[adriaanm]

That's why that word is so interesting.

[adriaanm]

Finally! All green! (on jenkins)

[retronym]

The second commit broke shapeless:

https://gist.github.com/8973653

https://jenkins-dbuild.typesafe.com:8499/job/Community-2.11.x-retronym/26/console

I'm minimizing.

/cc @milessabin

[retronym]

trait A { type Result }

class PolyTests {
  def wrong(x: A { type Result = Int })
             : A { type Result = String} = x
}

[retronym]

@adriaanm I poked around at this here:

https://github.com/retronym/scala/compare/ticket;8177-3?expand=1

[adriaanm]

Thanks! The fix SGTM, looks like SI-7753 (or some permutation of its digits) broke t0764. It really should compile (at some point -- it is another bug after all), since subtyping on type members is covariant:

found   : Node{type T = _1.type} where val _1: Node{type T = NextType}
required: Node{type T = Main.this.AType} (which expands to)  Node{type T = Node{type T = NextType}}

so the subtpying question becomes _1.type <: Main.this.AType, or:

(T forSome {type T <: Node{type T = NextType} with Singleton}) <: Node{type T = NextType}

skolemizing, and applying to T-SUB-TRANSITIVE:

T& <:  Node{type T = NextType} with Singleton <: Node{type T = NextType} <: Node{type T = NextType}

[paulp]

subtyping on type members is covariant

Can't be. Subtyping on abstract type members ok, but not once they have been specified.

Example with current master:

trait A {
  type Member
  def f(x: Member): Member
}
object Test extends App {
  var x: A { type Member = String } = new A { type Member = String ; def f(x: String): String = { x.length ; x } }
  var y: A { type Member = AnyRef } = x

  y.f(Nil)
}
// java.lang.ClassCastException: scala.collection.immutable.Nil$ cannot be cast to java.lang.String

[paulp]

And I still think t0764 should compile, but the reason is that I think the singleton type of v should propagate all the way through.

[retronym]

Adriaan made the fatal error of replying before his third cup of coffee this morning...

Regrading t0764, I made a few types explicit when I moved it to neg.

https://github.com/retronym/scala/compare/ticket;8177-3?expand=1#diff-57560366739c20af01965fe137b150eeR6

This part must remain a type error, no?:

t0764.scala:16: error: type mismatch;
  found   : Node{type T = _1.type} where val _1: Node{type T = NextType}
  required: Node{type T = Main.this.AType}

[adriaanm]

Subtyping of type aliases is invariant. That was my kryptonite

On Thursday, February 13, 2014, Jason Zaugg notifications@github.com
wrote:

Adriaan made the fatal error of replying before his third cup of coffee
this morning...

Regrading t0764, I made a few types explicit when I moved it to neg.

https://github.com/retronym/scala/compare/ticket;8177-3?expand=1#diff-57560366739c20af01965fe137b150eeR6

This part must remain a type error, no?:

t0764.scala:16: error: type mismatch;
found : Node{type T = _1.type} where val _1: Node{type T = NextType}
required: Node{type T = Main.this.AType}

Reply to this email directly or view it on GitHubhttps://github.com//pull/3516#issuecomment-35004080
.

[paulp]

@retronym look at this variation.

package p1 {
  object t0764 {
    type NodeAlias[A] = Node { type T = A }
    trait Node { outer =>
      type T <: Node
      def prepend: Node { type T = outer.type } = ???
    }

    class Main1[A <: Node](val v: NodeAlias[A]) {
      private[this] def f1 = new Main1(null: Node { type T = Node { type T = A }})                        // fail
      private[this] def f2 = new Main1[NodeAlias[A]](null: Node { type T = Node { type T = A }})          // fail
      private[this] def f3 = new Main1[Node { type T = A }](null: Node { type T = Node { type T = A }})   // fail
      // private[this] def f4 = new Main1[v.type](null: Node { type T = Node { type T = A }})                // ok
    }

    class Main2[A <: Node](val v: Node { type T = A }) {
      private[this] def f1 = new Main2(null: Node { type T = Node { type T = A }})                        // fail
      private[this] def f2 = new Main2[NodeAlias[A]](null: Node { type T = Node { type T = A }})          // fail
      private[this] def f3 = new Main2[Node { type T = A }](null: Node { type T = Node { type T = A }})   // fail
      // private[this] def f4 = new Main2[v.type](null: Node { type T = Node { type T = A }})                // ok
    }
  }
}

package p2 {
  object t0764 {
    type NodeAlias[A] = Node { type T = A }
    trait Node { outer =>
      type T <: Node
      def prepend: NodeAlias[outer.type] = ???
    }

    class Main1[A <: Node](val v: NodeAlias[A]) {
      private[this] def f1 = new Main1(null: Node { type T = Node { type T = A }})                        // ok!  <<========== WOT
      private[this] def f2 = new Main1[NodeAlias[A]](null: Node { type T = Node { type T = A }})          // fail
      private[this] def f3 = new Main1[Node { type T = A }](null: Node { type T = Node { type T = A }})   // fail
      // private[this] def f4 = new Main1[v.type](null: Node { type T = Node { type T = A }})                // ok
    }

    class Main2[A <: Node](val v: Node { type T = A }) {
      private[this] def f1 = new Main2(null: Node { type T = Node { type T = A }})                        // fail
      private[this] def f2 = new Main2[NodeAlias[A]](null: Node { type T = Node { type T = A }})          // fail
      private[this] def f3 = new Main2[Node { type T = A }](null: Node { type T = Node { type T = A }})   // fail
      // private[this] def f4 = new Main2[v.type](null: Node { type T = Node { type T = A }})                // ok
    }
  }
}

This compiles even in 2.10. But all I did was perform the type substitutions the compiler should be doing. Rather than calling prepend, I placed the return type of prepend there directly. Then I replaced outer.type (aka v.type) with v's non-singleton type Node { type T = A }. And at that point the only methods which don't compile are the ones which take v.type explicitly, which of course no longer compiles because I weakened v.

[paulp]

Actually I guess it's going to be a problem that I've replaced { type T = outer.type } with the widened type, because one could construct a similar example to the CCE above where outer.type is an incoming type and the widened type is not equivalent, even though its type member will be equivalent. However it should be compilable by sprinkling some <: where there are =s.

But I'm not even sure about any of that - this example is confusing as hell .

[adriaanm]

Hmm, even though I had another cup of coffee by now, I need to try this out before I'm sure, but my next theory would be that &1 was skolemized too soon (indicated by the "where" in the erorr message), because we should even be able to satisfy type equality, which would then turn my earlier argument into a convincing case:

 Node{type T = _1.type} where val _1: Node{type T = NextType} 
  <:< 
 Node{type T = Node{type T = NextType}}

becomes 

 Node{type T = X&} <:< Node{type T = Node{type T = NextType}}
   (where X& <: Node{type T = NextType} with Singleton)

becomes

  X& =:= Node{type T = NextType}

this would be satisfiable if X was an existential type variable and not a skolem (though I'm not sure about the with Singleton)

[adriaanm]

TBH, I'm not sure whether this is right:

scala> typeOf[X forSome { type X <: String }] =:= typeOf[String]
res1: Boolean = false

scala> typeOf[X forSome { type X <: String }] <:< typeOf[String] &&
       typeOf[String] <:< typeOf[X forSome { type X <: String }] 
res2: Boolean = true

scala> typeOf[X forSome { type X >: String <: String }] =:= typeOf[String]
res3: Boolean = false

scala> typeOf[String] <:< typeOf[X forSome { type X >: String <: String }] && 
       typeOf[X forSome { type X >: String <: String }] <:< typeOf[String]
res4: Boolean = true

[adriaanm]

(Sorry about the live comment editing.)

[paulp]

This couldn't be falser:

typeOf[String] <:< typeOf[X forSome { type X <: String }] 

[paulp]

(Well, except by actually being considered false.)

[paulp]

On consideration, fuck if I know anything. Stop enticing me to think about these things.

[adriaanm]

I always have to look up the rules to convince myself because they are so unintuitive to me, but I believe String <: Exists X. X <: String.

Rule s1-abstract deals with existentials on the right-hand side of a subtyping judgment.
It states that T is a subtype of some existential if all constraints of the existential hold after substituting T for the existentially quantified type variable.

[clhodapp]

With typeOf[String] :< typeOf[X forSome { type X <: String }], aren't we essentiality asking "Is there some type X, which must be a subtype of String, which String is a subtype of?" If so, of course the answer is yes: X can be String!

[clhodapp]

@adriaanm I think you pulled from the wrong section of the paper you linked: The ƐΧₗₘₚₗ calculus from which you took that definition and explanation only holds where existentials can only specify implementation (upper) bounds. You have to look at ƐΧᵤₚₗₒ (which renders weird in my font) to find rules that hold when existentials can specify both upper and lower bounds. I'm working on getting to the point where I can post and explain a screenshot without getting things wrong, but to prove to yourself that the substitution method of judgement won't work, consider Nothing :< (T forSome { type T >: String }), which is definitely true, but would be rejected under simple substitution.

[adriaanm]

I think the subtyping judgment holds more generally. It just talks about constraints, whether they are lower or upper bounds or even richer. The key is how you instantiate the meta-variables in the proof rules.

[adriaanm]

More concretely, applied to scala and scalac:

      T <: subst(U)    for all i: subst(Li) <: Vi /\ Vi <: subst(Hi)
 ----------------------------------------------------------------------------
         T <: U forSome {type X1 :> L1 <: H1,..., type Xn :> Ln <: Hn}

where subst(T) = T.subst(Xi, Vi) // Vi fresh type variables

T is a subtype of some existential if all constraints of the existential hold
after substituting Vi for the existentially quantified type variables Xi,
and T is a subtype of the underlying type U with the same substition applied.

[adriaanm]

which leads me to believe withTypeVars is wrong

I think it should be:

    def withTypeVars(op: Type => Boolean, depth: Depth): Boolean = {
      val quantifiedFresh = cloneSymbols(quantified)
      val tvars           = quantifiedFresh map (tparam => TypeVar(tparam))
      // fuse subst quantified -> quantifiedFresh -> tvars
      val underlying1     = underlying.instantiateTypeParams(quantified, tvars)

      isWithinBounds(NoPrefix, NoSymbol, quantifiedFresh, tvars) && // add constraints implied by bounds
      op(underlying1) &&                                            // check actual relation
      solve(tvars, quantifiedFresh, quantifiedFresh map (_ => Invariant), upper = false, depth)
    }

[paulp]

I can certainly testify that many is the bug trail which went into withTypeVars and then went dark.

[clhodapp]

I'm actually reading the through the code, trying to get acquainted with what's going on (I haven't spent much time in this part of the compiler). I'm not sure I will gain a sufficient understanding of what's going on in the typechecker in time to be of any use to anyone on this, but oh well. I do have to say that I'm kind of astounded at how many things seem to be slightly (dangerously?) misnamed (e.g. instantiateTypeParams is perfectly happy subbing things that aren't type parameters).

Anyway, in the unlikely event that anyone cares, I did work a few examples using the rule Adriaan suggested his most recent couple comments. My examples are at https://gist.github.com/clhodapp/5bb0ad993cd60ca556e8, with the final one being Paul's String <: (T forSome { type T >: String }).

[paulp]

I do have to say that I'm kind of astounded at how many things seem to be slightly (dangerously?) misnamed

Ha ha, you have no idea.

[retronym]

Would you mind submitting a pull request with that in "literate test case" form?

[clhodapp]

Sure, though it's more likely to be of the form "Here's proof that the thing should hold. Here's an implicitly[_ <:< _] showing that the compiler admits/doesn't admit the thing", rather than some kind of convoluted system to try to get the compiler to follow along with my work.

[clhodapp]

Or, better, I'll just use typeOf's, so it doesn't have to not compile.

[retronym]

I'd say a neg test would be the most straight forward way to do this.

[clhodapp]

Submitted: #3534