{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
module Data.Exists.Constrained where

import Data.Typeable

-- | Dependent sum
data E c a = ∀ k . (Typeable k, c k) => E { unE :: a k }

map :: (∀ k . c k => a k -> b k) -> E c a -> E c b
map f (E a) = E (f a)

mapF :: Functor f => (∀ k . c k => a k -> f (b k)) -> E c a -> f (E c b)
mapF f (E a) = E <$> f a