{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

import           Data.Functor.Identity
import           Data.Typeable

-- Union

infixr 1 |>
data (a :: * -> *) |> b

-- class Member (t :: * -> *) r
-- instance Member t (t |> r)
-- instance Member t r => Member t (t' |> r)

type family t `Elem` ts :: Bool where
    _ `Elem` Void = False
    t `Elem` (t |> r) = True
    t `Elem` (t' |> r) = t `Elem` r

type Member t r = t `Elem` r ~ True

data Union r a where
    Union :: (Functor t, Typeable t) => Identity (t a) -> Union r a

instance Functor (Union r) where
    fmap f (Union (Identity x)) = Union (Identity (fmap f x))

inj :: (Functor t, Typeable t, Member t r) => t a -> Union r a
inj = Union . Identity

prj :: (Functor t, Typeable t, Member t r) => Union r a -> Maybe (t a)
prj (Union f) = runIdentity <$> gcast1 f

maybeToRight :: a -> Maybe b -> Either a b
maybeToRight d Nothing  = Left d
maybeToRight _ (Just x) = Right x

decomp :: Typeable t => Union (t |> r) a -> Either (Union r a) (t a)
decomp (Union f) = maybeToRight (Union f) (runIdentity <$> gcast1 f)


-- Eff

data Status a r = Done a | Send (Union r (Status a r))

newtype Eff r a = Eff { runEff :: forall b. (a -> Status b r) -> Status b r }

instance Functor (Eff r) where
    fmap f m = Eff $ \next ->
        runEff m (\x -> next (f x))

instance Applicative (Eff r) where
    pure x = Eff $ \next -> next x
    mf <*> mx = Eff $ \next ->
        runEff mf $ \f ->
            runEff mx $ \x ->
                next (f x)

instance Monad (Eff r) where
    m >>= f = Eff $ \next ->
        runEff m $ \x ->
            runEff (f x) next

send :: (forall b . (a -> Status b r) -> Union r (Status b r)) -> Eff r a
send f = Eff (Send . f)

handleRelay :: Typeable t
            => Union (t |> r) a
            -> (a -> Eff r b)
            -> (t a -> Eff r b)
            -> Eff r b
handleRelay u f h = case decomp u of
    Right x -> h x
    Left u  -> send (\next -> next <$> u) >>= f


-- Void

data Void

run :: forall a . Eff Void a -> a
run m = handle (runEff m Done)
  where
    handle (Done x) = x
    handle (Send _) = undefined


-- Reader

newtype Reader e a = Reader (e -> a)
    deriving (Functor, Typeable)

ask :: (Typeable e, Member (Reader e) r) => Eff r e
ask = send (inj . Reader)

runReader :: Typeable e => Eff (Reader e |> r) a -> e -> Eff r a
runReader m e = handle (runEff m Done)
  where
    handle (Done x) = return x
    handle (Send u) = handleRelay u handle (\(Reader next) -> handle (next e))

testReader :: Eff (Reader Integer |> Reader Double |> Void) Double
testReader = do
    x <- ask
    y <- ask
    pure $ fromInteger x + y

main :: IO ()
main = do
    print $ run $ runReader (runReader testReader 10) 5.5 -- 15.5
    print $ run $ pure "lol"