UnapplyMT.scala

trait UnapplyMT[TC[_[_[_], _]], N[_], MTNA] {
  /** the type constructor */
  type MT[_[_], _]

  /** The type that MT is applied to */
  type A

  /** The instance of the type class */
  def TC: TC[MT]

  /** Evidence that MA =:= M[A] */
  def leibniz: MTNA === MT[N,A]

  /** Compatibility. */
  @inline final def apply(ma: MTNA): MT[N, A] = leibniz.subst[Id](ma)
}

trait UnapplyMT_0 {
  implicit def unapplyMTMA[TC[_[_[_], _]], M0[_[_], _], N[_], A0](implicit TC0: TC[M0]): UnapplyMT[TC, N, M0[N,A0]] {
    type MT[X[_],Y] = M0[X,Y]
    type A = A0

  } = new UnapplyMT[TC, N, M0[N,A0]] {
    type MT[X[_],Y] = M0[X,Y]
    type A = A0
    def TC = TC0
    def leibniz = refl
  }
}

object UnapplyMT extends UnapplyMT_0{
  implicit def unapplyMTMAB1[TC[_[_[_], _]], M0[_[_], _, _], N[_], A0, B0](implicit TC0: TC[({type λ[α[_], β] = M0[α, β, B0]})#λ]): UnapplyMT[TC,N, M0[N,A0,B0]] {
    type MT[X[_],Y] = M0[X,Y,B0]
    type A = A0
  } = new UnapplyMT[TC, N, M0[N,A0,B0]] {
    type MT[X[_],Y] = M0[X,Y,B0]
    type A = A0
    def TC = TC0
    def leibniz = refl
  }
  implicit def unapplyMTMAB2[TC[_[_[_], _]], M0[_[_], _, _], N[_], A0, B0](implicit TC0: TC[({type λ[α[_], β] = M0[α, A0, β]})#λ]): UnapplyMT[TC,N, M0[N,A0,B0]] {
    type MT[X[_],Y] = M0[X,A0,Y]
    type A = B0
  } = new UnapplyMT[TC, N, M0[N,A0,B0]] {
    type MT[X[_],Y] = M0[X,A0,Y]
    type A = B0
    def TC = TC0
    def leibniz = refl
  }
}