Why type equality check with implicitly fails?

I'd like to do some calculation on type level during runtime. So I define wrapper classes and implicit definitions for them. But I could not understand why type information is lost during computation

sealed trait Solve[In] {
  type Out
}

implicit def idSolve[I] = new Solve[I] {
  override type Out = I
}

type X = Int
val y = implicitly[Solve[X]]

val e = implicitly[X =:= y.Out]
val l = implicitly[X <:< y.Out]
val g = implicitly[y.Out <:< X]

The compiler accepts neither of e, l, g:

TypeSolution.scala:15: error: Cannot prove that test.Test.X =:= test.Test.y.Out.
  val e = implicitly[X =:= y.Out]
                    ^
TypeSolution.scala:16: error: Cannot prove that test.Test.X <:< test.Test.y.Out.
  val l = implicitly[X <:< y.Out]
                    ^
TypeSolution.scala:17: error: Cannot prove that test.Test.y.Out <:< test.Test.X.
  val g = implicitly[y.Out <:< X]
                    ^
three errors found

What is going on and why compiler refuses to admit that X and y.Out are the same types. Is it possible to rephrase the example so it would compile?

Solution

implicitly "forgets" type information, as per it's definition (+ inferred types % renaming):

def implicitly[A](implicit a: A): A = a

Note that it returns something of type A, not a.type. Therefore, your code looks like:

val y = implicitly[Solve[Int]]
// ===
val y: Solve[Int] /* per return type of implicitly */ = implicitly[Solve[Int]]

y's type is inferred to Solve[Int], not Solve[Int] { type Out = Int }, so y.Out is unknown.

You can define a custom implicitly without this restriction:

import Predef.{ implicitly => _, _ } // Begone, failure!

import language.experimental.macros
import reflect.macros.whitebox.Context

def implicitly[T](implicit found: T): T = macro implicitly_impl[T]

def implicitly_impl[T: c.WeakTypeTag](c: Context)(found: c.Tree) = found
// We just return the exact same tree that we got, eliding the implicitly completely and dropping it's type-erasing touch.

Which works as a drop-in replacement:

scala> :paste
// Entering paste mode (ctrl-D to finish)

import Predef.{ implicitly => _, _ }

import language.experimental.macros
import reflect.macros.whitebox.Context

def implicitly[T](implicit found: T): T = macro implicitly_impl[T]

def implicitly_impl[T: c.WeakTypeTag](c: Context)(found: c.Tree) = found

// Exiting paste mode, now interpreting.

import Predef.{implicitly=>_, _}
import language.experimental.macros
import reflect.macros.whitebox.Context
defined term macro implicitly: [T](implicit found: T)T
implicitly_impl: [T](c: scala.reflect.macros.whitebox.Context)(found: c.Tree)(implicit evidence$1: c.WeakTypeTag[T])c.Tree

scala> :paste
// Entering paste mode (ctrl-D to finish)

sealed trait Solve[In] {
  type Out
}

implicit def idSolve[I] = new Solve[I] {
  override type Out = I
}

type X = Int
val y = implicitly[Solve[X]]

val e = implicitly[X =:= y.Out]
val l = implicitly[X <:< y.Out]
val g = implicitly[y.Out <:< X]

// Exiting paste mode, now interpreting.

defined trait Solve
idSolve: [I]=> Solve[I]{type Out = I}
defined type alias X
y: Solve[X]{type Out = X} = $anon$1@611f28f5
e: y.Out =:= y.Out = <function1>
l: X <:< X = <function1>
g: y.Out <:< y.Out = <function1>

Sidenote:

def implicitly[A](implicit a: A): a.type = a

Won't work, because Scala doesn't like it when you use singleton types without an AnyRef upper bound.

def implicitly[A <: AnyRef](implicit a: A): a.type = a

Works in this case, but it won't allow AnyVal subclasses or the like. However, the macro solution is not very complicated and works for everything, which is a fair trade.