Try compiling with -O1 if you have a lot of time on your hands

TakesForeverToCompile.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module TakesForeverToCompile where

import Data.Kind
import Data.Type.Equality ((:~:)(..))

rebalance :: forall j (x1 :: j) (x2 :: j) (x3 :: j) (x4 :: j)
                    (a :: x1 :~: x2) (b :: x2 :~: x3) (c :: x3 :~: x4).
             Sing a -> Sing b -> Sing c
          -> Trans a (Trans b c) :~: Trans (Trans a b) c
rebalance sa sb sc = leibniz @(x1 :~: x2) @(WhyRebalanceSym2 b c)
                             @(Symmetry (Symmetry a)) @a
                             (symIdempotent sa) rebalanceHelper
  where
    rebalanceHelper :: Trans (Symmetry (Symmetry a)) (Trans b c)
                   :~: Trans (Trans (Symmetry (Symmetry a)) b) c
    rebalanceHelper = (~>:~:) @j @x2 @(WhyRebalanceHelperSym2 b c) @x1 @(Symmetry a)
                              (sSym sa) rebalanceBC

    rebalanceBC :: Trans Refl (Trans b c) :~: Trans (Trans Refl b) c
    rebalanceBC = trans (transRight (sTrans sb sc)) transRightBC

    transRightBC :: Trans b c :~: Trans (Trans Refl b) c
    transRightBC = cong @(x2 :~: x3) @(x2 :~: x4) @(FlipSym2 TransSym0 c)
                        @b @(Trans Refl b)
                        (sym (transRight sb))

type family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type f @@ x = Apply f x

data SomeSing :: Type -> Type where
  SomeSing :: Sing (a :: k) -> SomeSing k

class SingKind (k :: Type) where
  type Demote k :: Type
  toSing :: Demote k -> SomeSing k

withSomeSing :: forall k r
              . SingKind k
             => Demote k
             -> (forall (a :: k). Sing a -> r)
             -> r
withSomeSing x f =
  case toSing x of
    SomeSing x' -> f x'

data (%:~:) :: forall k (a :: k) (b :: k). a :~: b -> Type where
  SRefl :: (%:~:) Refl
type instance Sing = (%:~:)

instance SingKind (a :~: b) where
  type Demote (a :~: b) = a :~: b
  toSing Refl    = SomeSing SRefl

(~>:~:) :: forall k (a :: k)
                  (p :: forall (y :: k). a :~: y ~> Type)
                  (b :: k) (r :: a :~: b).
           Sing r
        -> p @@ Refl
        -> p @@ r
(~>:~:) SRefl pRefl = pRefl

type family Flip (f :: a ~> b ~> c) (y :: b) (x :: a) :: c where
  Flip f y x = f @@ x @@ y
data FlipSym0 :: forall a b c. (a ~> b ~> c) ~> b ~> a ~> c
data FlipSym1 :: forall a b c. (a ~> b ~> c) -> b ~> a ~> c
data FlipSym2 :: forall a b c. (a ~> b ~> c) -> b -> a ~> c
type instance Apply FlipSym0 f       = FlipSym1 f
type instance Apply (FlipSym1 f) y   = FlipSym2 f y
type instance Apply (FlipSym2 f y) x = Flip f y x

type family Symmetry (x :: (a :: k) :~: b) :: b :~: a where
  Symmetry Refl = Refl

type family Trans (x :: (a :: k) :~: b) (y :: b :~: c) :: a :~: c where
  Trans Refl Refl = Refl
data TransSym0 :: forall k (a :: k) (b :: k) (c :: k). a :~: b ~> b :~: c ~> a :~: c
data TransSym1 :: forall k (a :: k) (b :: k) (c :: k). a :~: b -> b :~: c ~> a :~: c
type instance Apply TransSym0 x     = TransSym1 x
type instance Apply (TransSym1 x) y = Trans x y

data SingSym0 :: forall k. k ~> Type
type instance Apply SingSym0 x = Sing x

newtype WrappedTrans (x :: k) (e :: x :~: y) =
  WrapTrans { unwrapTrans :: forall (z :: k). y :~: z -> x :~: z }
data WrappedTransSym1 (x :: k) :: forall (y :: k). x :~: y ~> Type
type instance Apply (WrappedTransSym1 x) e = WrappedTrans x e

newtype WrappedSTrans (x :: k) (e1 :: x :~: y) =
  WrapSTrans { unwrapSTrans :: forall (z :: k) (e2 :: y :~: z).
                               Sing e2 -> Sing (Trans e1 e2) }
data WrappedSTransSym1 (x :: k) :: forall (y :: k). x :~: y ~> Type
type instance Apply (WrappedSTransSym1 x) e = WrappedSTrans x e

type WhySym (a :: t) (e :: a :~: y) = y :~: a
data WhySymSym1 (a :: t) :: forall (y :: t). a :~: y ~> Type
type instance Apply (WhySymSym1 a) e = WhySym a e

type WhySSym (a :: t) (e :: a :~: y) = Sing (Symmetry e)
data WhySSymSym1 (a :: t) :: forall (y :: t). a :~: y ~> Type
type instance Apply (WhySSymSym1 a) e = WhySSym a e

type WhySymIdempotent (a :: t) (r :: a :~: z) = Symmetry (Symmetry r) :~: r
data WhySymIdempotentSym1 (a :: t) :: forall (z :: t). a :~: z ~> Type
type instance Apply (WhySymIdempotentSym1 a) r = WhySymIdempotent a r

type WhyReplace (from :: t) (p :: t ~> Type) (e :: from :~: y) = p @@ y
data WhyReplaceSym2 (from :: t) (p :: t ~> Type) :: forall (y :: t). from :~: y ~> Type
type instance Apply (WhyReplaceSym2 from p) e = WhyReplace from p e

type WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t) = f @@ a -> f @@ z
data WhyLeibnizSym2 (f :: t ~> Type) (a :: t) :: t ~> Type
type instance Apply (WhyLeibnizSym2 f a) z = WhyLeibniz f a z

type WhyCong (f :: x ~> y) (a :: x) (e :: a :~: z) = f @@ a :~: f @@ z
data WhyCongSym2 (f :: x ~> y) (a :: x) :: forall (z :: x). a :~: z ~> Type
type instance Apply (WhyCongSym2 f a) e = WhyCong f a e

type WhyTransRight (a :: k) (e :: a :~: z) = Trans Refl e :~: e
data WhyTransRightSym1 (a :: k) :: forall (z :: k). a :~: z ~> Type
type instance Apply (WhyTransRightSym1 a) e = WhyTransRight a e

type WhyRebalance (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x1 :~: x2) =
  Trans a (Trans b c) :~: Trans (Trans a b) c
data WhyRebalanceSym2 (b :: (x2 :: k) :~: x3) (c :: x3 :~: x4) :: forall (x1 :: k). x1 :~: x2 ~> Type
type instance Apply (WhyRebalanceSym2 b c) a = WhyRebalance b c a

type WhyRebalanceHelper (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x2 :~: x1) =
  Trans (Symmetry a) (Trans b c) :~: Trans (Trans (Symmetry a) b) c
data WhyRebalanceHelperSym2 (b :: (x2 :: k) :~: x3) (c :: x3 :~: x4) :: forall (x1 :: k). x2 :~: x1 ~> Type
type instance Apply (WhyRebalanceHelperSym2 b c) a = WhyRebalanceHelper b c a

sym :: forall t (a :: t) (b :: t).
       a :~: b -> b :~: a
sym eq = withSomeSing eq $ \(singEq :: Sing r) ->
           (~>:~:) @t @a @(WhySymSym1 a) @b @r singEq Refl

sSym :: forall t (a :: t) (b :: t) (e :: a :~: b).
        Sing e -> Sing (Symmetry e)
sSym se = (~>:~:) @t @a @(WhySSymSym1 a) @b @e se SRefl

symIdempotent :: forall t (a :: t) (b :: t)
                        (e :: a :~: b).
                 Sing e -> Symmetry (Symmetry e) :~: e
symIdempotent se = (~>:~:) @t @a @(WhySymIdempotentSym1 a) @b @e se Refl

trans :: forall t (a :: t) (b :: t) (c :: t).
                a :~: b -> b :~: c -> a :~: c
trans eq1 eq2 = withSomeSing eq1 $ \(singEq1 :: Sing r) ->
                  unwrapTrans ((~>:~:) @t @a @(WrappedTransSym1 a) @b @r
                                       singEq1 (WrapTrans id)) eq2

replace :: forall t (from :: t) (to :: t) (p :: t ~> Type).
           p @@ from
        -> from :~: to
        -> p @@ to
replace from eq =
  withSomeSing eq $ \(singEq :: Sing r) ->
    (~>:~:) @t @from @(WhyReplaceSym2 from p) @to @r singEq from

leibniz :: forall t (f :: t ~> Type) (a :: t) (b :: t).
           a :~: b
        -> f @@ a
        -> f @@ b
leibniz = replace @t @a @b @(WhyLeibnizSym2 f a) id

cong :: forall x y (f :: x ~> y)
               (a :: x) (b :: x).
        a :~: b
     -> f @@ a :~: f @@ b
cong eq =
  withSomeSing eq $ \(singEq :: Sing r) ->
    (~>:~:) @x @a @(WhyCongSym2 f a) @b @r singEq Refl

transRight :: forall j (a :: j) (b :: j) (e :: a :~: b).
              Sing e -> Trans Refl e :~: e
transRight se = (~>:~:) @j @a @(WhyTransRightSym1 a) @b @e se Refl

sTrans :: forall t (a :: t) (b :: t) (c :: t)
                   (e1 :: a :~: b) (e2 :: b :~: c).
          Sing e1 -> Sing e2 -> Sing (Trans e1 e2)
sTrans se1 = unwrapSTrans $ (~>:~:) @t @a @(WrappedSTransSym1 a) @b @e1
                                    se1 (WrapSTrans sTransHelper)
  where
    sTransHelper :: forall (z :: t) (e' :: a :~: z).
                    Sing e' -> Sing (Trans Refl e')
    sTransHelper se' = leibniz @(a :~: z) @SingSym0 @e' @(Trans Refl e')
                               (sym (transRight se')) se'