path: root/test/files/neg/t0764.scala

class Top[A] {
        type AType = A
}

trait Node { outer =>
        type T <: Node
        def prepend = new Node { type T = outer.type }
}

class Main[NextType <: Node](value: Node { type T = NextType })
        extends Top[Node { type T = NextType }] {

        new Main[AType]( (value: AType).prepend )
}

/* we've been back-and-forth on this one -- see PRs on SI-8177 for the reasoning
I think it should compile and that the following error is due to broken =:= on existentials
 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}}

I claim (omitting the forSome for brevity, even though the premature skolemization is probably the issue)
_1.type =:= Main.this.AType
because
(1) _1.type <:< Main.this.AType and (2) Main.this.AType  <:< _1.type
(1), because:
_1.type <:< Node{type T = NextType} (because skolemization and _1's upper bound)
(2), because:
Node{type T = NextType} <:< _1.type forSome val _1: Node{type T = NextType}
because:
Node{type T = NextType} <:< T forSome {type T <: Node{type T = NextType} with Singleton}
because 
Node{type T = NextType} <:< Node{type T = NextType} with Singleton

hmmm.. might the with Singleton be throwing a wrench in our existential house?

Behold the equivalent program which type checks without the fix for SI-8177.
(Expand type alias, convert type member to type param;
note the covariance to encode subtyping on type members.)

class Node[+T <: Node[_]] { def prepend = new Node[this.type] }
class Main[NextType <: Node[_]](value: Node[NextType]) {
  new Main(value.prepend)
}
*/