Доказательства того, что нет никаких доказательств

Question

Существует ли тип Not[Ev] или способ его реализации, который я могу использовать следующим образом

def someMethod[X,Y](implicit ev:Not[X <:< Option[Y])= ???

То есть тип X не является типом Option [_]? (и с этим можно было бы сделать больше)

Answer 1

Документы implicitAmbiguous предполагают следующую реализацию неравенства типов

trait =!=[C, D]

implicit def neq[E, F] : E =!= F = null

@annotation.implicitAmbiguous("Could not prove ${J} =!= ${J}")
implicit def neqAmbig1[G, H, J] : J =!= J = null
implicit def neqAmbig2[I] : I =!= I = null

, где

def someMethod[X,Y](implicit ev: X =!= Option[Y])= ???

someMethod[Int, String]       // ok
someMethod[Option[Int], Int]  // error