Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Try compiling with -O1 if you have a lot of time on your hands
{-# 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'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment