module Data.Extensible.Union where
import Data.Extensible.Internal
import Data.Extensible.Internal.Rig
import Data.Extensible.Sum
import Data.Extensible.Product
import Data.Typeable
newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)
newtype Union xs a = Union { getUnion :: K1 a :| xs }
reunion :: Gondola m :* xs -> Union xs a -> m a
reunion gs (Union (UnionAt pos (K1 f))) = views (sectorAt pos) runGondola gs f
newtype Gondola f g = Gondola { runGondola :: forall a. g a -> f a }
rung :: (forall x. f x -> g x) -> Gondola g :* fs -> Gondola g :* (f ': fs)
rung f = (<:) (Gondola f)
infixr 0 `rung`
runGondolas :: (x ∈ xs) => Gondola f :* xs -> x a -> f a
runGondolas = views sector runGondola