Safe Haskell  Trustworthy 

Language  Haskell2010 
Extensions 

Open unions (typeindexed coproducts) for extensible effects All operations are constanttime, and there is no Typeable constraint
This is a variation of OpenUion5.hs, which relies on overlapping instances instead of closed type families. Closed type families have their problems: overlapping instances can resolve even for unground types, but closed type families are subject to a strict apartness condition.
This implementation is very similar to OpenUnion1.hs, but without the annoying Typeable constraint. We sort of emulate it:
Our list r of open union components is a small Universe. Therefore, we can use the Typeablelike evidence in that universe. We hence can define
data Union r v where Union :: t v > TRep t r > Union r v  t is existential
where
data TRep t r where T0 :: TRep t (t ': r) TS :: TRep t r > TRep (any ': r)
Then Member is a type class that produces TRep Taken literally it doesn't seem much better than OpenUinion41.hs. However, we can cheat and use the index of the type t in the list r as the TRep. (We will need UnsafeCoerce then).
The interface is the same as of other OpenUnion*.hs
 data Union (r :: [* > *]) v
 inj :: Member t r => t v > Union r v
 prj :: Member t r => Union r v > Maybe (t v)
 decomp :: Union (t ': r) v > Either (Union r v) (t v)
 class FindElem t r => Member (t :: * > *) r where
 class Member t r => SetMember (tag :: k > * > *) (t :: * > *) r  tag r > t
 type family (ms :: [* > *]) <:: r where ...
 weaken :: Union r w > Union (any ': r) w
Documentation
data Union (r :: [* > *]) v Source #
The data constructors of Union are not exported
Strong Sum (Existential with the evidence) is an open union t is can be a GADT and hence not necessarily a Functor. Int is the index of t in the list r; that is, the index of t in the universe r
class FindElem t r => Member (t :: * > *) r where Source #
FindElem [* > *] t r => Member t r Source #  
(~) (* > *) t s => Member t ((:) (* > *) s ([] (* > *))) Source #  Explicit typelevel equality condition is a dirty
hack to eliminate the type annotation in the trivial case,
such as There is no ambiguity when finding instances for
The only case we have to concerned about is 
class Member t r => SetMember (tag :: k > * > *) (t :: * > *) r  tag r > t Source #
This class is used for emulating monad transformers
type family (ms :: [* > *]) <:: r where ... Source #
A useful operator for reducing boilerplate.
f :: [Reader Int, Writer String] ::> r => a > Eff r b
is equal to
f :: (Member (Reader Int) r, Member (Writer String) r) => a > Eff r b
'[] <:: r = (() :: Constraint)  
(m ': ms) <:: r = (Member m r, (<::) ms r) 