Leibniz.scala

abstract class Foo {
  trait BarT { this: Bar => def zomg: String }
  type Bar <: BarT

  def newBar: Bar
}

// Or not sealed if you reject axiom K? :)
sealed abstract class FooEqual[X <: Foo, Y <: Foo] {
  val x: X
  val y: Y

  def subst[F[_]](fx: F[x.Bar]): F[y.Bar]

  private type Id[A] = A
  def apply(fx: x.Bar): y.Bar = subst[Id](fx)
}

class Refl[F <: Foo with Singleton](val z: F) extends FooEqual[F, F] {
  val x: z.type = z
  val y: z.type = z

  def subst[F[_]](fx: F[z.Bar]): F[z.Bar] = fx
}

object Leibniz {
  def equate(x: Foo)(y: x.type): Option[FooEqual[x.type, y.type]] = Some(new Refl[x.type](x))

  case class FooA(x: Int) extends Foo {
    case class Bar() extends BarT { def zomg = s"zomgA $x" }
    def newBar: Bar = Bar()
  }

  case class FooB(x: String) extends Foo {
    case class Bar(i: Int) extends BarT { def zomg = s"zomgB $i $x" }
    def newBar: Bar = Bar(5)
  }


  def main(args: Array[String]) {
    val x = FooA(5)
    val y = FooB("ahaha")
    val z = FooA(5)

    val a = x.newBar
    val b = x.newBar
    val c = y.newBar

    // With a type ascription we get this lovely error message:
    // ./a.scala:55: error: type mismatch;
    //  found   : Option[FooEqual[x.type,z.type]]
    //  required: Option[FooEqual[x.type,z.type]]
    //       case z: x.type => equate(x)(z)
    //                               ^
    // one error found
    val compared = z match {
      case z: x.type => equate(x)(z)
      case _         => None
    }
    val Some(foo) = compared
    val bar = foo(a)
    println(a.zomg)
    println(bar.zomg)
    println(c.zomg)
  }
}