Data.Comp.Multi.Sum

This module defines sums on signatures. All definitions are generalised versions of those in Data.Comp.Sum.

Documentation

class sub :<: sup where

The subsumption relation.

Methods

inj :: sub a :-> sup a

proj :: NatM Maybe (sup a) (sub a)

Instances

f :<: f

(:<:) f g => f :<: ((:+:) h g)

f :<: ((:+:) f g)

data (f :+: g) h e infixr 5

Data type defining coproducts.

Instances

(:<:) f g => f :<: ((:+:) h g)

f :<: ((:+:) f g)

(HFunctor f, HFunctor g) => HFunctor ((:+:) f g)

(HFoldable f, HFoldable g) => HFoldable ((:+:) f g)

(HTraversable f, HTraversable g) => HTraversable ((:+:) f g)

(ShowHF f, ShowHF g) => ShowHF ((:+:) f g)

(EqHF f, EqHF g) => EqHF ((:+:) f g)

EqF is propagated through sums.

(OrdHF f, OrdHF g) => OrdHF ((:+:) f g)

OrdHF is propagated through sums.

(Desugar f h, Desugar g h) => Desugar ((:+:) f g) h

(HasVars f v0, HasVars g v0) => HasVars ((:+:) f g) v

DistAnn s p s' => DistAnn ((:+:) f s) p ((:+:) ((:&:) f p) s')

RemA s s' => RemA ((:+:) ((:&:) f p) s) ((:+:) f s')

caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c

Utility function to case on a higher-order functor sum, without exposing the internal representation of sums.

Projections for Signatures and Terms

proj2 :: forall f i a g1 g2. ((:<:) g1 f, (:<:) g2 f) => f a i -> Maybe ((:+:) g2 g1 a i)

proj3 :: forall f i a g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => f a i -> Maybe ((:+:) g3 ((:+:) g2 g1) a i)

proj4 :: forall f i a g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => f a i -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) a i)

proj5 :: forall f i a g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => f a i -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) a i)

proj6 :: forall f i a g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => f a i -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) a i)

proj7 :: forall f i a g1 g2 g3 g4 g5 g6 g7. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => f a i -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) a i)

proj8 :: forall f i a g1 g2 g3 g4 g5 g6 g7 g8. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => f a i -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) a i)

proj9 :: forall f i a g1 g2 g3 g4 g5 g6 g7 g8 g9. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f) => f a i -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) a i)

proj10 :: forall f i a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f, (:<:) g10 f) => f a i -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) a i)

project :: g :<: f => NatM Maybe (Cxt h f a) (g (Cxt h f a))

Project the outermost layer of a term to a sub signature. If the signature g is compound of n atomic signatures, use projectn instead.

project2 :: forall h f a i g1 g2. ((:<:) g1 f, (:<:) g2 f) => Cxt h f a i -> Maybe ((:+:) g2 g1 (Cxt h f a) i)

project3 :: forall h f a i g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => Cxt h f a i -> Maybe ((:+:) g3 ((:+:) g2 g1) (Cxt h f a) i)

project4 :: forall h f a i g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => Cxt h f a i -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) (Cxt h f a) i)

project5 :: forall h f a i g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => Cxt h f a i -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) (Cxt h f a) i)

project6 :: forall h f a i g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => Cxt h f a i -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) (Cxt h f a) i)

project7 :: forall h f a i g1 g2 g3 g4 g5 g6 g7. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => Cxt h f a i -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) (Cxt h f a) i)

project8 :: forall h f a i g1 g2 g3 g4 g5 g6 g7 g8. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => Cxt h f a i -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) (Cxt h f a) i)

project9 :: forall h f a i g1 g2 g3 g4 g5 g6 g7 g8 g9. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f) => Cxt h f a i -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) (Cxt h f a) i)

project10 :: forall h f a i g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f, (:<:) g10 f) => Cxt h f a i -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) (Cxt h f a) i)

deepProject :: (HTraversable g, g :<: f) => CxtFunM Maybe f g

Tries to coerce a termcontext to a termcontext over a sub-signature. If the signature g is compound of n atomic signatures, use deepProjectn instead.

deepProject2 :: forall f g1 g2. (HTraversable ((:+:) g2 g1), (:<:) g1 f, (:<:) g2 f) => CxtFunM Maybe f ((:+:) g2 g1)

deepProject3 :: forall f g1 g2 g3. (HTraversable ((:+:) g3 ((:+:) g2 g1)), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => CxtFunM Maybe f ((:+:) g3 ((:+:) g2 g1))

deepProject4 :: forall f g1 g2 g3 g4. (HTraversable ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => CxtFunM Maybe f ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))

deepProject5 :: forall f g1 g2 g3 g4 g5. (HTraversable ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => CxtFunM Maybe f ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))

deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (HTraversable ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => CxtFunM Maybe f ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))

deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (HTraversable ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => CxtFunM Maybe f ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))

deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (HTraversable ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => CxtFunM Maybe f ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))

deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (HTraversable ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f) => CxtFunM Maybe f ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))

deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (HTraversable ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f, (:<:) g10 f) => CxtFunM Maybe f ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))))

Injections for Signatures and Terms

inj2 :: forall g a i f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 a i -> g a i

inj3 :: forall g a i f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) a i -> g a i

inj4 :: forall g a i f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) a i -> g a i

inj5 :: forall g a i f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) a i -> g a i

inj6 :: forall g a i f1 f2 f3 f4 f5 f6. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g) => (:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))) a i -> g a i

inj7 :: forall g a i f1 f2 f3 f4 f5 f6 f7. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g) => (:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))) a i -> g a i

inj8 :: forall g a i f1 f2 f3 f4 f5 f6 f7 f8. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g) => (:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))) a i -> g a i

inj9 :: forall g a i f1 f2 f3 f4 f5 f6 f7 f8 f9. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g) => (:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))) a i -> g a i

inj10 :: forall g a i f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g, (:<:) f10 g) => (:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))) a i -> g a i

inject :: g :<: f => g (Cxt h f a) :-> Cxt h f a

Inject a term where the outermost layer is a sub signature. If the signature g is compound of n atomic signatures, use injectn instead.

inject2 :: forall h g a i f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 (Cxt h g a) i -> Cxt h g a i

inject3 :: forall h g a i f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) (Cxt h g a) i -> Cxt h g a i

inject4 :: forall h g a i f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) (Cxt h g a) i -> Cxt h g a i

inject5 :: forall h g a i f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) (Cxt h g a) i -> Cxt h g a i

inject6 :: forall h g a i f1 f2 f3 f4 f5 f6. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g) => (:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))) (Cxt h g a) i -> Cxt h g a i

inject7 :: forall h g a i f1 f2 f3 f4 f5 f6 f7. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g) => (:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))) (Cxt h g a) i -> Cxt h g a i

inject8 :: forall h g a i f1 f2 f3 f4 f5 f6 f7 f8. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g) => (:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))) (Cxt h g a) i -> Cxt h g a i

inject9 :: forall h g a i f1 f2 f3 f4 f5 f6 f7 f8 f9. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g) => (:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))) (Cxt h g a) i -> Cxt h g a i

inject10 :: forall h g a i f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g, (:<:) f10 g) => (:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))) (Cxt h g a) i -> Cxt h g a i

deepInject :: (HFunctor g, g :<: f) => CxtFun g f

Inject a term over a sub signature to a term over larger signature. If the signature g is compound of n atomic signatures, use deepInjectn instead.

deepInject2 :: forall g f1 f2. (HFunctor ((:+:) f2 f1), (:<:) f1 g, (:<:) f2 g) => CxtFun ((:+:) f2 f1) g

deepInject3 :: forall g f1 f2 f3. (HFunctor ((:+:) f3 ((:+:) f2 f1)), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => CxtFun ((:+:) f3 ((:+:) f2 f1)) g

deepInject4 :: forall g f1 f2 f3 f4. (HFunctor ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => CxtFun ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) g

deepInject5 :: forall g f1 f2 f3 f4 f5. (HFunctor ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => CxtFun ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))) g

deepInject6 :: forall g f1 f2 f3 f4 f5 f6. (HFunctor ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g) => CxtFun ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))) g

deepInject7 :: forall g f1 f2 f3 f4 f5 f6 f7. (HFunctor ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g) => CxtFun ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))) g

deepInject8 :: forall g f1 f2 f3 f4 f5 f6 f7 f8. (HFunctor ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g) => CxtFun ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))) g

deepInject9 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9. (HFunctor ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g) => CxtFun ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))) g

deepInject10 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (HFunctor ((:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g, (:<:) f10 g) => CxtFun ((:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))))) g

Injections and Projections for Constants

injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a

injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g) => Const (f1 :+: f2) :-> Cxt h g a

injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) :-> Cxt h g a

projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)

injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a

This function injects a whole context into another context.

liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a

This function lifts the given functor to a context.

substHoles :: (HFunctor f, HFunctor g, f :<: g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a

This function applies the given context with hole type a to a family f of contexts (possibly terms) indexed by a. That is, each hole h is replaced by the context f h.