{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, StandaloneDeriving, ScopedTypeVariables
           , GADTs, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, InstanceSigs
           , TypeFamilies, Rank2Types, ConstraintKinds, FlexibleContexts #-}
-- | You probably want to use the "Control.Monad.Signal.Class" module. This module contains
--   internals.
module Data.Union (Union(..), absurd, Elem(..), Subset(..), All(..)) where

import GHC.Base
import Data.Proxy

-- | An open union type. A @Union xs@ type holds a value of type @x@ where @x@ is some type from
--   xs.
data Union (types :: [*]) where
    Union :: Either (Union types) a -> Union (a ': types)

instance Show (Union '[]) where
    show _ = "Union '[]"
deriving instance (Show a, Show (Union as)) => Show (Union (a ': as))

deriving instance (Eq a, Eq (Union as)) => Eq (Union (a ': as))

deriving instance (Ord a, Ord (Union as)) => Ord (Union (a ': as))

instance Read (Union '[]) where
    readsPrec _ _ = []
deriving instance (Read a, Read (Union as)) => Read (Union (a ': as))

-- | An empty union can't be constructed so we can get any value from it.
absurd :: Union '[] -> a
absurd _ = undefined

-- -- There's no real reason for this functionality for now.
-- data HList (types :: [*]) where
--     HNil :: HList '[]
--     (:-) :: a -> HList as -> HList (a ': as)
--
-- infixr 5 :-
--
-- class Deconstruct ts fs a | ts a -> fs, fs a -> ts where
--     deconstruct' :: Either (Union ts) a -> HList fs -> a
--
-- instance Deconstruct '[] '[] a where
--     deconstruct' (Left u) _ = absurd u
--     deconstruct' (Right a) _ = a
--
-- instance Deconstruct xs fs a => Deconstruct (x ': xs) ((x -> a) ': fs) a where
--     deconstruct' :: Either (Union (x ': xs)) a -> HList ((x -> a) ': fs) -> a
--     deconstruct' (Right a) (_ :- (fs :: HList fs)) = deconstruct' (Right a :: Either (Union xs) a) (fs :: HList fs)
--     deconstruct' (Left (Union (Right x))) (f :- fs) = deconstruct' (Right (f x) :: Either (Union xs) a) fs
--     deconstruct' (Left (Union (Left u))) (_ :- fs) = deconstruct' (Left u) fs
--
-- deconstruct :: Deconstruct ts fs a => Union ts -> HList fs -> a
-- deconstruct u = deconstruct' (Left u)


-- | @Elem types@ is a class of types from @types@. If @a@ is from @types@ it can be lifted
--   into a @Union types@
class Elem types a where
    liftSingle :: a -> Union types

instance Elem (a ': as) a where
    liftSingle = Union . Right

instance {-# OVERLAPPABLE #-} Elem as a => Elem (b ': as) a where
    liftSingle = Union . Left . liftSingle

-- | If @as@ is a subset of @bs@ we can take the value of @Union as@ and lift it into @Union bs@.
class Subset (as :: [*]) (bs :: [*]) where
    liftUnion :: Union as -> Union bs

instance (Elem bs a, Subset as bs) => Subset (a ': as) bs where
    liftUnion (Union (Left u)) = liftUnion u
    liftUnion (Union (Right a)) = liftSingle a

instance Subset '[] bs where
    liftUnion = absurd

-- | If all the elements of @xs@ satisfy the @c@ constraint then, given a function that only cares
--   about that constraint type, we can colapse the union into a concrete type.
--
--   For example, if all the types in @xs@ satisfy the @Show@ class, then we can use the @show@
--   function to turn a @Union xs@ into a @String@.
class All (c :: * -> Constraint) (xs :: [*]) where
    deconstructAll :: proxy c -> Union xs -> (forall x. c x => x -> a) -> a

instance All c '[] where
    deconstructAll _ u _ = absurd u

instance (c x, All c xs) => All c (x ': xs) where
    deconstructAll _ (Union (Right x)) f = f x
    deconstructAll p (Union (Left u))  f = deconstructAll p u f