{-# LANGUAGE GADTs, StandaloneDeriving, DataKinds #-}
{-# LANGUAGE KindSignatures, PolyKinds, RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module EffSystem
  where

import GHC.TypeLits (ErrorMessage(..),TypeError)

data Eff = EffWrite | EffRead

type EPure = '[]
type EWrite = '[EffWrite]
type ERead = '[EffRead]

data Test :: [Eff] -> * where
  A :: Test EPure                           -- No Effect
  B :: Test EWrite                          -- Write Effect
  HB :: Test e -> Test (FindE 'EffWrite e)  -- Handle Write Effect
  C :: Test ERead                           -- Read Effect
  HC :: Test e -> Test (FindE 'EffRead e)   -- Handle Read Effect
  (:>) :: Test a -> Test b -> Test (a ++ b) -- Concatenate Test Nodes

-- elem on type-level-list
type family FindE (a :: Eff) (xs :: [Eff]) :: [Eff] where
  FindE e (e : ys) = ys
  FindE e (n : ys) = n : FindE e ys
  FindE e '[] = TypeError (Text "Effect not found!")

-- Concatenate Type-Level-List
type family (++) (as :: [k]) (bs :: [k]) :: [k] where
  (++) a '[] = a
  (++) '[] b = b
  (++) (a ': as) (a ': bs) = a ': (as ++ bs)
  (++) (a ': as) bs = a ': (as ++ bs)

{-
λ> :t A
A :: Test EPure

λ> :t B
B :: Test EWrite

λ> :t HB B
HB B :: Test '[]

λ> :t C
C :: Test ERead

λ> :t HC C
HC C :: Test '[]

λ> :t A :> B :> C
A :> B :> C :: Test '[ 'EffWrite, 'EffRead]

λ> :t HC (HB (A :> B :> C))
HC (HB (A :> B :> C)) :: Test '[]

λ> HC A
<interactive>:115:1: error:
    • Effect not found!                 <--- Custom Type Error! \o/
    • When checking the inferred type
        it :: Test (TypeError ...)
-}