Proving equality of type constructors in Scala via an "arbitrary object" encoding of universal quantification.

gistfile1.scala

// Universal quantification is encoded in terms of quantifier-free
// assertions about an "abitrary" type (cp. "all swans are white" vs.
// "the arbitrary swan is white". Inspired by Kit Fine's 1985 "Reasoning
// with Arbitrary Objects", http://philosophy.fas.nyu.edu/object/kitfine.
// 
// Possibly also related to Oleg Kiselyov's "Interpreting types as
// abstract values", http://okmij.org/ftp/Computation/index.html#teval.

// What I wouldn't give for kind-polymorphism here ...
  
trait Eq1[T[_], U[_]]
trait Eq2[T[_, _], U[_, _]]

trait Arbitrary1
trait Arbitrary2

implicit def eq1[T[_], U[_]]
  (implicit ev : T[Arbitrary1] =:= U[Arbitrary1]) = new Eq1[T, U] {}
implicit def eq2[T[_, _], U[_, _]]
  (implicit ev : T[Arbitrary1, Arbitrary2] =:= U[Arbitrary1, Arbitrary2]) = new Eq2[T, U] {}

implicitly[Eq1[Option, Option]]  // OK
implicitly[Eq1[List, List]]      // OK
implicitly[Eq1[Option, List]]    // Does not compile

implicitly[Eq2[Map, Map]]        // OK
implicitly[Eq2[Tuple2, Tuple2]]  // OK
implicitly[Eq2[Map, Tuple2]]     // Does not compile