module Data.Yoko.InDT where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.Reflect
data HasTagRepU tag c t where
HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->
HasTagRepU tag c t
instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)
) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits
hasTagRepU :: HasTagRepU tag c t -> RMI c -> t
hasTagRepU (HasTagRepU d) = w d where
w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t
w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj
w (OnLeft u) = w u; w (OnRight u) = w u
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
instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc
) => dc ::: ImageInDTU t fn where
inhabits = ImageInDTU inhabits
imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t
imageInDTU fn (ImageInDTU d) = hasTagRepU d . apply (CMap fn) . rep
data ImageInDTDA t fn dc where
ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)
) => HasTagRepImageU (fn IdM) dc t -> ImageInDTDA t fn dc
instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc
) => dc ::: ImageInDTDA t fn where
inhabits = ImageInDTDA inhabits
imageInDTAU :: Functor (Idiom (fn IdM)) =>
(forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t
imageInDTAU fn (ImageInDTDA d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep