--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Type.Dummies
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------






{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

module Type.Dummies where
    
#include "../Defs.hs"
         
-- | \"Kind-cast\" @ SET @ to @*@
data Lower (a :: SET)
    
-- | \"Kind-cast\" @ SET1 @ to @ SET @. Also lower elements using 'Lower'.
data Lower1 (a :: SET1) :: SET where
    LowerElement :: u x -> Lower1 u (Lower x)
    
-- | \"Kind-cast\" @ SET2 @ to @ SET1 @. Also lower elements using 'Lower1'.
data Lower2 (a :: SET2) :: SET1 where
    Lower1Element :: u x -> Lower2 u (Lower1 x)
    
-- | \"Kind-cast\" @ SET3 @ to @ SET2 @. Also lower elements using 'Lower2'.
data Lower3 (a :: SET3) :: SET2 where
    Lower2Element :: u x -> Lower3 u (Lower2 x)

-- | Pair of types of kind @ SET @
data PAIR (a :: SET) (b :: SET) x
-- | Pair of types of kind @ SET1 @
data PAIR1 (a :: SET1) (b :: SET1) (x :: SET) 
-- | Pair of types of kind @ SET2 @
data PAIR2 (a :: SET2) (b :: SET2) (x :: SET1)
-- | Pair of types of kind @ SET3 @
data PAIR3 (a :: SET3) (b :: SET3) (x :: SET2)
    
data Bool0
data Bool1
    
data BOOL :: SET where
    Bool0 :: BOOL Bool0
    Bool1 :: BOOL Bool1
            
elimBOOL :: BOOL a -> r Bool0 -> r Bool1 -> r a
elimBOOL Bool0 x _ = x
elimBOOL Bool1 _ x = x
                      
kelimBOOL :: BOOL a -> r -> r -> r
kelimBOOL Bool0 x _ = x
kelimBOOL Bool1 _ x = x


-- data ΣPair (a :: SET) (b :: *)
    
-- type DependentPair = ΣPair

-- type Curry f a b = f (a,b)
    
-- type family Uncurry (f :: * -> * -> *) (ab :: *) :: *
-- type instance Uncurry g (a,b) = g a b


-- type Curry2 f a b = f (Pair2 a b)
    
-- type family Uncurry2 (g :: SET -> SET -> *) (ab :: SET) :: *
-- type instance Uncurry2 g (Pair2 a b) = g a b

    
-- type Curry3 f a b = f (Pair3 a b)
    
-- type family Uncurry3 (g :: SET1 -> SET1 -> *) (ab :: SET1) :: *
-- type instance Uncurry3 g (Pair3 a b) = g a b

    
-- type Curry4 f a b = f (Pair4 a b)
    
-- type family Uncurry4 (g :: SET2 -> SET2 -> *) (ab :: SET2) :: *
-- type instance Uncurry4 g (Pair4 a b) = g a b