#include "macros.h"
LANGUAGE_TRUSTWORTHY
module Type.Eq.Higher (module Type.Eq, module Type.Eq.Higher) where
#if __GLASGOW_HASKELL__ >= 707
import Data.OldTypeable hiding (cast)
#else
import Data.Typeable hiding (cast)
#endif
import Type.Eq
import Type.Eq.Higher.Unsafe
import Unsafe.Coerce
constructorEq :: f a :~: g b -> f ::~:: g
constructorEq Eq = BUG_5591(Eq1)
sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: g
sameOuterEq OuterEq OuterEq = BUG_5591(Eq1)
data (f :: * -> *) ::~:: (g :: * -> *) where
Eq1 :: (f ~ g) => f ::~:: g
withEq1 :: (f ~ g => r) -> (f ::~:: g) -> r
withEq1 x Eq1 = x
idEq1 :: f ::~:: f
idEq1 = Eq1
composeEq1, (|.|) :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h)
composeEq1 Eq1 Eq1 = Eq1
(|.|) = composeEq1
flipEq1 :: (f ::~:: g) -> (g ::~:: f)
flipEq1 Eq1 = Eq1
applyEq1, (|$|) :: f ::~:: g -> a :~: b -> f a :~: g b
applyEq1 Eq1 Eq = Eq
(|$|) = applyEq1
constructorEq1 :: m a ::~:: n b -> m :::~::: n
constructorEq1 Eq1 = BUG_5591(Eq2)
argumentEq1 :: m a ::~:: n b -> a :~: b
argumentEq1 Eq1 = BUG_5591(Eq)
DYNAMIC_EQ(1,1,::~::,f,g,())
data OuterEq1 (m :: * -> * -> *) (f :: * -> *) where
OuterEq1 :: m a ~ f => OuterEq1 m f
data InnerEq1 (a :: *) (f :: * -> *) where
InnerEq1 :: m a ~ f => InnerEq1 a f
withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> r
withOuterEq1 a OuterEq1 = a
withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> r
withInnerEq1 a InnerEq1 = a
outerEq1 :: m a ::~:: f -> OuterEq1 m f
outerEq1 Eq1 = OuterEq1
innerEq1 :: m a ::~:: f -> InnerEq1 a f
innerEq1 Eq1 = InnerEq1
assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: f
assembleEq1 OuterEq1 InnerEq1 = BUG_5591(Eq1)
sameOuterEq1 :: OuterEq1 m f -> OuterEq1 n f -> m :::~::: n
sameOuterEq1 OuterEq1 OuterEq1 = BUG_5591(Eq2)
sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: b
sameInnerEq1 InnerEq1 InnerEq1 = BUG_5591(Eq)
data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where
Eq2 :: (m ~ n) => m :::~::: n
withEq2 :: (m ~ n => r) -> (m :::~::: n) -> r
withEq2 x Eq2 = x
idEq2 :: m :::~::: m
idEq2 = Eq2
composeEq2, (||.||) :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o)
composeEq2 Eq2 Eq2 = Eq2
(||.||) = composeEq2
flipEq2 :: (m :::~::: n) -> (n :::~::: m)
flipEq2 Eq2 = Eq2
applyEq2, (||$||) :: m :::~:::n -> a :~: b -> m a ::~:: n b
applyEq2 Eq2 Eq = Eq1
(||$||) = applyEq2
DYNAMIC_EQ(2,2,:::~:::,n,m,() ())