ended up having to use the vague OverlappingInstance. That's not
quite what I hope. I'm not even sure whether the instance `Member t (t :> r)`
{-# LANGUAGE KindSignatures, TypeOperators, GADTs, FlexibleInstances,
FlexibleContexts, MultiParamTypeClasses, OverlappingInstances #-}
-- FlexibleContexts is for Show instance of Union
import Data.Functor
import Control.Applicative -- for several functor instances
-- open union
infixr 2 :>
data (a :: * -> *) :> b
data Union r v where
Elsewhere :: Functor t' => Union r v -> Union (t' :> r) v
Here :: Functor t => t v -> Union (t :> r) v
class Member t r where
inj :: Functor t => t v -> Union r v
prj :: Functor t => Union r v -> Maybe (t v)
instance Member t (t :> r) where
inj tv = Here tv
prj (Here tv) = Just tv
prj (Elsewhere _) = Nothing
-- Note: overlapped by letting t' = t
instance (Functor t', Member t r) => Member t (t' :> r) where
inj tv = Elsewhere (inj tv)
prj (Here _) = Nothing
prj (Elsewhere u) = prj u
decomp :: Functor t => Union (t :> r) v -> Either (Union r v) (t v)
decomp (Here tv) = Right tv
decomp (Elsewhere u) = Left u
-- Auxiliary definitions for tests
data Void
newtype Func a = Func a
instance Show (Union Void a) where
show _ = undefined
instance (Show (t v), Show (Union r v)) => Show (Union (t :> r) v) where
show (Here tv) = "Here " ++ show tv
show (Elsewhere u) = "Elsewhere " ++ show u
instance Functor Func where
fmap f (Func x) = Func (f x)
instance Show a => Show (Func a) where
show (Func a) = show a
type Stk = Maybe :> Either Char :> Func :> Void
type Stk' = Either Char :> Func :> Void -- used in `deTrue`, `deFalse`
unTrue :: Union Stk Bool
unTrue = inj (Func True)
unFalse :: Union Stk Bool
unFalse = inj (Just False)
-- `Func` is repeated
un5 :: Union (Maybe :> Func :> Either Char :> Func :> Void) Int
un5 = inj (Func 5)
maybe2 :: Maybe (Func Int)
maybe2 = prj un5
maybeTrue :: Maybe (Func Bool)
maybeTrue = prj unTrue
maybeFalse1 :: Maybe (Func Bool)
maybeFalse1 = prj unFalse
maybeFalse2 :: Maybe (Maybe Bool)
maybeFalse2 = prj unFalse
deTrue :: Either (Union Stk' Bool) (Maybe Bool)
deTrue = decomp unTrue
deFalse :: Either (Union Stk' Bool) (Maybe Bool)
deFalse = decomp unFalse