GrandChild (2)

grandchild.scala

trait John
trait Carl
trait Tom
trait Child[T,U]
trait GrandChild {
  type Left
  type Right
}
object GrandChild {
  type Left[T] = GrandChild { type Left = T }
  type Right[U] = GrandChild { type Right = U }
  type Aux[T,U] = GrandChild { type Left = T; type Right = U }
}

implicit val john_carl = new Child[John,Carl]{}
implicit val carl_tom  = new Child[Carl,Tom ]{}

implicit def grandChild[X,Y,Z](
	implicit 
		xy: Child[X,Y],
		yz: Child[Y,Z]
	) = new GrandChild { type Left = X; type Right = U }

output.scala

scala> implicitly [ GrandChild[John] ]
res0: GrandChild[John] = $anon$1@7193666c

scala> implicitly [ GrandChild[John]{type Nephew = Tom} ]
res1: GrandChild[John]{type Nephew = Tom} = $anon$1@38c6f217

scala> implicitly [ GrandChild.Aux[John, Tom] ]
res2: GrandChild.Aux[John,Tom] = $anon$1@4b2bac3f

scala> implicitly [ GrandChild.Aux[John, Tom] =:= GrandChild[John] {type Nephew = Tom} ]
res3: =:=[GrandChild.Aux[John,Tom],GrandChild[John]{type Nephew = Tom}] = <function1>

// why is this not compiling ?
scala> implicitly [ GrandChild.Aux[John, Tom] =:= GrandChild[John] ]
<console>:20: error: Cannot prove that GrandChild.Aux[John,Tom] =:= GrandChild[John].
       implicitly [ GrandChild.Aux[John, Tom] =:= GrandChild[John] ]
                  ^