```package scalaz

import Scalaz.{⊥, ⊤}

/**
* Leibnizian equality: A better =:=
*
* This technique was first used in
* <a href="http://portal.acm.org/citation.cfm?id=583852.581494">Typing Dynamic Typing</a> (Baars and Swierstra, ICFP 2002).
*
* It is generalized here to handle subtyping so that it can be used with constrained type constructors.
*
* Leibniz[L,H,A,B] says that A = B, and that both of its types are between L and H. Subtyping lets you
* loosen the bounds on L and H.
*
* If you just need a witness that A = B, then you can use A===B which is a supertype of any Leibniz[L,H,A,B]
*
* The more refined types are useful if you need to be able to substitute into restricted contexts.
*/
trait Leibniz[-L, +H >: L, A >: L <: H, B >: L <: H] {
def subst[F[_ >: L <: H]](p: F[A]): F[B]
def compose[L2 <: L, H2 >: H, C >: L2 <: H2](that: Leibniz[L2, H2, C, A]): Leibniz[L2, H2, C, B] =
Leibniz.trans[L2, H2, C, A, B](this, that)
def andThen[L2 <: L, H2 >: H, C >: L2 <: H2](that: Leibniz[L2, H2, B, C]): Leibniz[L2, H2, A, C] =
Leibniz.trans[L2, H2, A, B, C](that, this)
}

object Leibniz {

/** (A === B) is a supertype of Leibniz[L,H,A,B] */
type ===[A,B] = Leibniz[⊥, ⊤, A, B]

/** Equality is reflexive -- we rely on subtyping to expand this type */
implicit def refl[A]: Leibniz[A, A, A, A] = new Leibniz[A, A, A, A] {
def subst[F[_ >: A <: A]](p: F[A]): F[A] = p
}

/** We can witness equality by using it to convert between types
* We rely on subtyping to enable this to work for any Leibniz arrow
*/
implicit def witness[A, B](f: A === B): A => B =
f.subst[({type λ[X] = A => X})#λ](identity)

/** Equality is transitive */
def trans[L, H >: L, A >: L <: H, B >: L <: H, C >: L <: H](
f: Leibniz[L, H, B, C],
g: Leibniz[L, H, A, B]
): Leibniz[L, H, A, C] =
f.subst[({type λ[X >: L <: H] = Leibniz[L, H, A, X]})#λ](g)

/** Equality is symmetric */
def symm[L, H >: L, A >: L <: H, B >: L <: H](
f: Leibniz[L, H, A, B]
)  : Leibniz[L, H, B, A] =
f.subst[({type λ[X>:L<:H]=Leibniz[L, H, X, A]})#λ](refl)

sealed class LeibnizGroupoid[L_, H_ >: L_] extends GeneralizedGroupoid with Hom {
type L = L_
type H = H_
type C[A >: L <: H, B >: L <: H] = Leibniz[L, H, A, B]
type U = LeibnizGroupoid[L, H]

def id[A >: L <: H]: Leibniz[A, A, A, A] = refl[A]

def compose[A >: L <: H, B >: L <: H, C >: L <: H](
bc: Leibniz[L, H, B, C],
ab: Leibniz[L, H, A, B]
): Leibniz[L, H, A, C] = trans[L, H, A, B, C](bc, ab)

def invert[A >: L <: H, B >: L <: H](
ab: Leibniz[L, H, A, B]
): Leibniz[L, H, B, A] = symm(ab)
}

implicit def leibnizGroupoid[L, H >: L]: LeibnizGroupoid[L, H] = new LeibnizGroupoid[L, H]

/** We can lift equality into any type constructor */
def lift[
LA, LT,
HA >: LA, HT >: LT,
T[_ >: LA <: HA] >: LT <: HT,
A >: LA <: HA, A2 >: LA <: HA
](
a: Leibniz[LA, HA, A, A2]
): Leibniz[LT, HT, T[A], T[A2]] =
a.subst[({type λ[X >: LA <: HA] = Leibniz[LT, HT, T[A], T[X]]})#λ](refl)

/** We can lift equality into any type constructor */
def lift2[
LA, LB, LT,
HA >: LA, HB >: LB, HT >: LT,
T[_ >: LA <: HA, _ >: LB <: HB] >: LT <: HT,
A >: LA <: HA, A2 >: LA <: HA,
B >: LB <: HB, B2 >: LB <: HB
](
a: Leibniz[LA, HA, A, A2],
b: Leibniz[LB, HB, B, B2]
) : Leibniz[LT, HT, T[A, B], T[A2, B2]] =
b.subst[({type λ[X >: LB <: HB] = Leibniz[LT, HT, T[A, B], T[A2, X]]})#λ](
a.subst[({type λ[X >: LA <: HA] = Leibniz[LT, HT, T[A, B], T[X, B]]})#λ](
refl))

/** We can lift equality into any type constructor */
def lift3[
LA, LB, LC, LT,
HA >: LA, HB >: LB, HC >: LC, HT >: LT,
T[_ >: LA <: HA, _ >: LB <: HB, _ >: LC <: HC] >: LT <: HT,
A >: LA <: HA, A2 >: LA <: HA,
B >: LB <: HB, B2 >: LB <: HB,
C >: LC <: HC, C2 >: LC <: HC
](
a: Leibniz[LA, HA, A, A2],
b: Leibniz[LB, HB, B, B2],
c: Leibniz[LC, HC, C, C2]
): Leibniz[LT, HT, T[A, B, C], T[A2, B2, C2]] =
c.subst[({type λ[X >: LC <: HC] = Leibniz[LT, HT, T[A, B, C], T[A2, B2, X]]})#λ](
b.subst[({type λ[X >: LB <: HB] = Leibniz[LT, HT, T[A, B, C], T[A2, X, C]]})#λ](
a.subst[({type λ[X >: LA <: HA] = Leibniz[LT, HT, T[A, B, C], T[X, B, C]]})#λ](
refl)))

/**
* Unsafe coercion between types. force abuses asInstanceOf to explicitly coerce types.
* It is unsafe, but needed where Leibnizian equality isn't sufficient
*/
def force[L, H >: L, A >: L <: H, B >: L <: H]: Leibniz[L, H, A, B] = new Leibniz[L, H, A, B] {
def subst[F[_ >: L <: H]](fa: F[A]): F[B] = fa.asInstanceOf[F[B]]
}

/**
* Emir Pasalic's PhD thesis mentions that it is unknown whether or not <code>((A,B) === (C,D)) => (A === C)</code> is inhabited.
* <p>
* Haskell can work around this issue by abusing type families as noted in
* but we instead turn to force.
* </p>
*
*/

// import Injectivity._

def lower[
LA, HA >: LA,
T[_ >: LA <: HA], //:Injective,
A >: LA <: HA, A2 >: LA <: HA
](
t: T[A] === T[A2]
): Leibniz[LA, HA, A, A2] = force[LA, HA, A, A2]

def lower2[
LA, HA >: LA,
LB, HB >: LB,
T[_ >: LA <: HA, _ >: LB <: HB], // :Injective2,
A >: LA <: HA, A2 >: LA <: HA,
B >: LB <: HB, B2 >: LB <: HB
](
t: T[A, B] === T[A2, B2]
): (Leibniz[LA, HA, A, A2], Leibniz[LB, HB, B, B2]) = (force[LA, HA, A, A2], force[LB, HB, B, B2])
}

```