scala - Mixin type constraints still compiles

Question

following on from Enforce type difference

I've noticed this compiles and am not sure why.

trait NotFuture {

  type Out[+T]

  implicitly[Out[_] =!= scala.concurrent.Future[_]]
}

val newNotFuture = new NotFuture {
  type Out[+T] = scala.concurrent.Future[T]
}

Any idea how to make this work?

Answer 1

Unfortunately I don't think it's possible to construct the required inequality proof until Out is actually defined. The closest I can get to what you want is something like this,

scala> import shapeless._ // for =:!=
import shapeless._

scala> import scala.concurrent.Future
import scala.concurrent.Future

scala> trait NotFuture {
     |   type Out[+T]
     |   val ev: Out[_] =:!= Future[_]
     |   def prf(implicit ev: Out[_] =:!= Future[_]) = ev
     | }
defined trait NotFuture

scala> val nf = new NotFuture { type Out[+T] = List[T] ; val ev = prf }
nf: NotFuture{type Out[+T] = List[T]} = $anon$1@5723cc36

scala> val nf = new NotFuture { type Out[+T] = Future[T] ; val ev = prf }
<console>:12: error: ambiguous implicit values:
 both method neqAmbig1 in package shapeless of type [A]=> shapeless.=:!=[A,A]
 and method neqAmbig2 in package shapeless of type [A]=> shapeless.=:!=[A,A]
 match expected type shapeless.=:!=[this.Out[_],scala.concurrent.Future[_]]
       val nf = new NotFuture { type Out[+T] = Future[T] ; val ev = prf }

Notice that providing the proof is mandatory (because ev is abstract in NotFuture) and provided semi-implicitly in the subclasses (val ev = prf).