Portability  see LANGUAGE pragmas (... GHC) 

Stability  experimental 
Maintainer  nicolas.frisby@gmail.com 
Various universes determined by a data constructor type's suitability to be embedded in a data type.
 data HasTagRepU tag c t where
 HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) > HasTagRepU tag c t
 hasTagRepU :: HasTagRepU tag c t > RMI c > t
 type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))
 data ImageInDTU t fn dc where
 ImageInDTU :: (Generic dc, (Rep dc) ::: (Domain (CMap fn IdM))) => HasTagRepImageU (fn IdM) dc t > ImageInDTU t fn dc
 imageInDTU :: (forall t. fn IdM t) > ImageInDTU t fn dc > RMNI dc > t
 data ImageInDTDA t fn dc where
 ImageInDTDA :: (Generic dc, (Rep dc) ::: (DomainA (CMap fn IdM))) => HasTagRepImageU (fn IdM) dc t > ImageInDTDA t fn dc
 imageInDTAU :: Functor (Idiom (fn IdM)) => (forall t. fn IdM t) > ImageInDTDA t fn dc > RMNI dc > Idiom (fn IdM) t
Documentation
data HasTagRepU tag c t whereSource
A type t
inhabits HasTagRepU tag c
if t
is a DT
and there exists a t
constructor satisfying
.
TagRepIs
tag c
HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) > HasTagRepU tag c t 
hasTagRepU :: HasTagRepU tag c t > RMI c > tSource
Given HasTagRepU tag c t
, a triviallymediated c
value can be embedded into
t
.
type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))Source
Often times, we're interested in the universe of types accomodating a data constructor's image under some typefunction.
data ImageInDTU t fn dc whereSource
A constructor type dc
inhabits ImageHasTagRepU t fn
if

fn
can be mapped across the recursive occurrences indc
, and 
t
has a constructor isomorphic to thefn
image ofdc
ImageInDTU :: (Generic dc, (Rep dc) ::: (Domain (CMap fn IdM))) => HasTagRepImageU (fn IdM) dc t > ImageInDTU t fn dc 
imageInDTU :: (forall t. fn IdM t) > ImageInDTU t fn dc > RMNI dc > tSource
Given ImageInDTU t fn dc
, a triviallymediated dc
value can be
embedded into t
.
data ImageInDTDA t fn dc whereSource
Same as ImageInDTD
, but uses an implicitly applicative function.
ImageInDTDA :: (Generic dc, (Rep dc) ::: (DomainA (CMap fn IdM))) => HasTagRepImageU (fn IdM) dc t > ImageInDTDA t fn dc 
imageInDTAU :: Functor (Idiom (fn IdM)) => (forall t. fn IdM t) > ImageInDTDA t fn dc > RMNI dc > Idiom (fn IdM) tSource