-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Parametric Compositional Data Types
--   
--   Based on Wouter Swierstra's Functional Pearl <i>Data types a la
--   carte</i> (Journal of Functional Programming, 18(4):423-436, 2008,
--   <a>http://dx.doi.org/10.1017/S0956796808006758</a>), this package
--   provides a framework for defining recursive data types in a
--   compositional manner with support for binders.
--   
--   This package implemements <i>parametric compositional data types</i>
--   (Workshop on Mathematically Structured Functional Programming, 3-24,
--   2012, <a>http://dx.doi.org/10.4204/EPTCS.76.3</a>), generalising
--   compositional data types (as implemented in the <i>compdata</i>
--   package) with support for parametric higher-order abstract syntax
--   (PHOAS).
--   
--   Examples of using parametric compositional data types are bundled with
--   the package in the folder <tt>examples</tt>.
@package compdata-param
@version 0.9.2


-- | This module defines difunctors (Meijer, Hutton, FPCA '95), i.e. binary
--   type constructors that are contravariant in the first argument and
--   covariant in the second argument.
module Data.Comp.Param.Difunctor
difmap :: Difunctor f => (a -> b) -> f c a -> f c b

-- | This class represents difunctors, i.e. binary type constructors that
--   are contravariant in the first argument and covariant in the second
--   argument.
class Difunctor f
dimap :: Difunctor f => (a -> b) -> (c -> d) -> f b c -> f a d
instance Data.Comp.Param.Difunctor.Difunctor (->)
instance Data.Comp.Param.Difunctor.Difunctor f => GHC.Base.Functor (f a)


-- | This module defines traversable difunctors.
module Data.Comp.Param.Ditraversable

-- | Difunctors representing data structures that can be traversed from
--   left to right.
class Difunctor f => Ditraversable f
dimapM :: (Ditraversable f, Monad m) => (b -> m c) -> f a b -> m (f a c)
disequence :: (Ditraversable f, Monad m) => f a (m b) -> m (f a b)


-- | This module defines a monad for generating fresh, abstract names,
--   useful e.g. for defining equality on terms.
module Data.Comp.Param.FreshM

-- | Monad for generating fresh (abstract) names.
data FreshM a

-- | Abstract notion of a name (the constructor is hidden).
data Name

-- | Run the given computation with the next available name.
withName :: (Name -> FreshM a) -> FreshM a

-- | Evaluate a computation that uses fresh names.
evalFreshM :: FreshM a -> a
instance GHC.Classes.Eq Data.Comp.Param.FreshM.Name
instance GHC.Base.Functor Data.Comp.Param.FreshM.FreshM
instance GHC.Base.Applicative Data.Comp.Param.FreshM.FreshM
instance GHC.Base.Monad Data.Comp.Param.FreshM.FreshM
instance GHC.Show.Show Data.Comp.Param.FreshM.Name
instance GHC.Classes.Ord Data.Comp.Param.FreshM.Name


-- | This module defines a monad for generating fresh, abstract names,
--   useful e.g. for defining equality on terms.
module Data.Comp.Param.Multi.FreshM

-- | Monad for generating fresh (abstract) names.
data FreshM a

-- | Abstract notion of a name (the constructor is hidden).
data Name i

-- | Run the given computation with the next available name.
withName :: (Name i -> FreshM a) -> FreshM a

-- | Change the type tag of a name.
nameCoerce :: Name i -> Name j

-- | Evaluate a computation that uses fresh names.
evalFreshM :: FreshM a -> a
instance GHC.Classes.Eq (Data.Comp.Param.Multi.FreshM.Name i)
instance GHC.Base.Applicative Data.Comp.Param.Multi.FreshM.FreshM
instance GHC.Base.Functor Data.Comp.Param.Multi.FreshM.FreshM
instance GHC.Base.Monad Data.Comp.Param.Multi.FreshM.FreshM
instance GHC.Show.Show (Data.Comp.Param.Multi.FreshM.Name i)
instance GHC.Classes.Ord (Data.Comp.Param.Multi.FreshM.Name i)


-- | This module defines higher-order difunctors, a hybrid between
--   higher-order functors (Johann, Ghani, POPL '08), and difunctors
--   (Meijer, Hutton, FPCA '95). Higher-order difunctors are used to define
--   signatures for compositional parametric generalised data types.
module Data.Comp.Param.Multi.HDifunctor

-- | This class represents higher-order difunctors.
class HDifunctor f
hdimap :: HDifunctor f => (a :-> b) -> (c :-> d) -> f b c :-> f a d

-- | This class represents higher-order functors (Johann, Ghani, POPL '08)
--   which are endofunctors on the category of endofunctors.
class HFunctor (h :: * -> * -> * -> *)

-- | A higher-order functor <tt>f</tt> also maps a natural transformation
--   <tt>g :-&gt; h</tt> to a natural transformation <tt>f g :-&gt; f
--   h</tt>
hfmap :: HFunctor h => f :-> g -> h f :-> h g

-- | The identity Functor.
newtype I a
I :: a -> I a
[unI] :: I a -> a

-- | The parametrised constant functor.
newtype K a i
K :: a -> K a i
[unK] :: K a i -> a
data E (f :: * -> *)
[E] :: E f
data A (f :: * -> *)
A :: forall i. () => f i -> A
[unA] :: A -> forall i. () => f i

-- | This type represents natural transformations.
type (:->) (f :: * -> *) (g :: * -> *) = forall i. () => f i -> g i
type NatM (m :: * -> *) (f :: * -> *) (g :: * -> *) = forall i. () => f i -> m g i
instance Data.Comp.Param.Multi.HDifunctor.HDifunctor f => Data.Comp.Multi.HFunctor.HFunctor (f a)


-- | This module defines traversable higher-order difunctors.
module Data.Comp.Param.Multi.HDitraversable

-- | HDifunctors representing data structures that can be traversed from
--   left to right.
class HDifunctor f => HDitraversable f
hdimapM :: (HDitraversable f, Monad m) => NatM m b c -> NatM m (f a b) (f a c)
class HFoldable t => HTraversable (t :: * -> * -> * -> *)

-- | Map each element of a structure to a monadic action, evaluate these
--   actions from left to right, and collect the results.
--   
--   Alternative type in terms of natural transformations using functor
--   composition <tt>:.:</tt>:
--   
--   <pre>
--   hmapM :: Monad m =&gt; (a :-&gt; m :.: b) -&gt; t a :-&gt; m :.: (t b)
--   </pre>
hmapM :: (HTraversable t, Monad m) => NatM m a b -> NatM m t a t b
htraverse :: (HTraversable t, Applicative f) => NatM f a b -> NatM f t a t b


-- | This module provides operators on higher-order difunctors.
module Data.Comp.Param.Multi.Ops

-- | Formal sum of signatures (difunctors).
data ( f (:+:) g ) (a :: * -> *) (b :: * -> *) i
Inl :: (f a b i) -> (:+:) f g i
Inr :: (g a b i) -> (:+:) f g i

-- | Utility function to case on a higher-order difunctor sum, without
--   exposing the internal representation of sums.
caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c

-- | Signature containment relation for automatic injections. The left-hand
--   must be an atomic signature, where as the right-hand side must have a
--   list-like structure. Examples include <tt>f :&lt;: f :+: g</tt> and
--   <tt>g :&lt;: f :+: (g :+: h)</tt>, non-examples include <tt>f :+: g
--   :&lt;: f :+: (g :+: h)</tt> and <tt>f :&lt;: (f :+: g) :+: h</tt>.
class (sub :: (* -> *) -> (* -> *) -> * -> *) :<: sup
inj :: (:<:) sub sup => sub a b :-> sup a b
proj :: (:<:) sub sup => NatM Maybe (sup a b) (sub a b)

-- | Formal product of signatures (higher-order difunctors).
data ( f (:*:) g ) a b i
(:*:) :: f a b i -> g a b i -> (:*:) f g a b i
ffst :: (f :*: g) a b :-> f a b
fsnd :: (f :*: g) a b :-> g a b

-- | This data type adds a constant product to a signature.
data ( f (:&:) p ) (a :: * -> *) (b :: * -> *) i
(:&:) :: f a b i -> p -> (:&:) f p i

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn (s :: (* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p

-- | Inject an annotation over a signature.
injectA :: DistAnn s p s' => p -> s a b :-> s' a b

-- | Project an annotation from a signature.
projectA :: DistAnn s p s' => s' a b :-> (s a b :&: p)
class RemA (s :: (* -> *) -> (* -> *) -> * -> *) s' | s -> s'

-- | Remove annotations from a signature.
remA :: RemA s s' => s a b :-> s' a b
instance Data.Comp.Param.Multi.Ops.RemA s s' => Data.Comp.Param.Multi.Ops.RemA ((f Data.Comp.Param.Multi.Ops.:&: p) Data.Comp.Param.Multi.Ops.:+: s) (f Data.Comp.Param.Multi.Ops.:+: s')
instance Data.Comp.Param.Multi.Ops.RemA (f Data.Comp.Param.Multi.Ops.:&: p) f
instance Data.Comp.Param.Multi.Ops.DistAnn f p (f Data.Comp.Param.Multi.Ops.:&: p)
instance Data.Comp.Param.Multi.Ops.DistAnn s p s' => Data.Comp.Param.Multi.Ops.DistAnn (f Data.Comp.Param.Multi.Ops.:+: s) p ((f Data.Comp.Param.Multi.Ops.:&: p) Data.Comp.Param.Multi.Ops.:+: s')
instance Data.Comp.Param.Multi.HDifunctor.HDifunctor f => Data.Comp.Param.Multi.HDifunctor.HDifunctor (f Data.Comp.Param.Multi.Ops.:&: p)
instance Data.Comp.Param.Multi.HDitraversable.HDitraversable f => Data.Comp.Param.Multi.HDitraversable.HDitraversable (f Data.Comp.Param.Multi.Ops.:&: p)
instance f Data.Comp.Param.Multi.Ops.:<: f
instance f Data.Comp.Param.Multi.Ops.:<: (f Data.Comp.Param.Multi.Ops.:+: g)
instance (f Data.Comp.Param.Multi.Ops.:<: g) => f Data.Comp.Param.Multi.Ops.:<: (h Data.Comp.Param.Multi.Ops.:+: g)
instance (Data.Comp.Param.Multi.HDifunctor.HDifunctor f, Data.Comp.Param.Multi.HDifunctor.HDifunctor g) => Data.Comp.Param.Multi.HDifunctor.HDifunctor (f Data.Comp.Param.Multi.Ops.:+: g)
instance (Data.Comp.Param.Multi.HDitraversable.HDitraversable f, Data.Comp.Param.Multi.HDitraversable.HDitraversable g) => Data.Comp.Param.Multi.HDitraversable.HDitraversable (f Data.Comp.Param.Multi.Ops.:+: g)


-- | This module defines the central notion of <i>generalised parametrised
--   terms</i> and their generalisation to generalised parametrised
--   contexts.
module Data.Comp.Param.Multi.Term

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes, and zero or more parameters. The
--   first parameter is a phantom type indicating whether the context has
--   holes. The second paramater is the signature of the context, in the
--   form of a <a>Data.Comp.Param.Multi.HDifunctor</a>. The third parameter
--   is the type of parameters, the fourth parameter is the type of holes,
--   and the fifth parameter is the GADT type.
data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> *
[In] :: f a (Cxt h f a b) i -> Cxt h f a b i
[Hole] :: b i -> Cxt Hole f a b i
[Var] :: a i -> Cxt h f a b i

-- | Phantom type used to define <a>Context</a>.
data Hole

-- | Phantom type used to define <a>Term</a>.
data NoHole

-- | A term is a context with no holes, where all occurrences of the
--   contravariant parameter is fully parametric.
newtype Term f i
Term :: forall a. Trm f a i -> Term f i
[unTerm] :: Term f i -> forall a. Trm f a i

-- | "Preterms" |
type Trm f a = Cxt NoHole f a (K ())

-- | A context may contain holes.
type Context = Cxt Hole

-- | Convert a difunctorial value into a context.
simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b
toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b

-- | This is an instance of <a>hfmap</a> for <a>Cxt</a>.
hfmapCxt :: forall h f a b b'. HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'

-- | This is an instance of <a>hdimapM</a> for <a>Cxt</a>.
hdimapMCxt :: forall h f a b b' m. (HDitraversable f, Monad m) => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')

-- | Monads for which embedded <tt>Trm</tt> values, which are parametric at
--   top level, can be made into monadic <tt>Term</tt> values, i.e.
--   "pushing the parametricity inwards".
class ParamFunctor m
termM :: ParamFunctor m => (forall a. m (Trm f a i)) -> m (Term f i)
instance Data.Comp.Param.Multi.Term.ParamFunctor GHC.Base.Maybe
instance Data.Comp.Param.Multi.Term.ParamFunctor (Data.Either.Either a)
instance Data.Comp.Param.Multi.Term.ParamFunctor []


-- | This module defines the notion of algebras and catamorphisms, and
--   their generalizations to e.g. monadic versions and other (co)recursion
--   schemes.
module Data.Comp.Param.Multi.Algebra

-- | This type represents an algebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>.
type Alg f a = f a a :-> a

-- | Construct a catamorphism for contexts over <tt>f</tt> with holes of
--   type <tt>b</tt>, from the given algebra.
free :: forall h f a b. HDifunctor f => Alg f a -> (b :-> a) -> Cxt h f a b :-> a

-- | Construct a catamorphism from the given algebra.
cata :: forall f a. HDifunctor f => Alg f a -> Term f :-> a

-- | A generalisation of <a>cata</a> from terms over <tt>f</tt> to contexts
--   over <tt>f</tt>, where the holes have the type of the algebra carrier.
cata' :: HDifunctor f => Alg f a -> Cxt h f a a :-> a

-- | This function applies a whole context into another context.
appCxt :: HDifunctor f => Cxt Hole f a (Cxt h f a b) :-> Cxt h f a b

-- | This type represents a monadic algebra. It is similar to <a>Alg</a>
--   but the return type is monadic.
type AlgM m f a = NatM m (f a a) a

-- | Construct a monadic catamorphism for contexts over <tt>f</tt> with
--   holes of type <tt>b</tt>, from the given monadic algebra.
freeM :: forall m h f a b. (HDitraversable f, Monad m) => AlgM m f a -> NatM m b a -> NatM m (Cxt h f a b) a

-- | Construct a monadic catamorphism from the given monadic algebra.
cataM :: forall m f a. (HDitraversable f, Monad m) => AlgM m f a -> NatM m (Term f) a

-- | This type represents a monadic algebra, but where the covariant
--   argument is also a monadic computation.
type AlgM' m f a = NatM m (f a (Compose m a)) a

-- | Right-to-left composition of functors. The composition of applicative
--   functors is always applicative, but the composition of monads is not
--   always a monad.
newtype Compose (f :: k -> *) (g :: k1 -> k) (a :: k1) :: forall k k1. () => k -> * -> k1 -> k -> k1 -> *
Compose :: f g a -> Compose
[getCompose] :: Compose -> f g a

-- | Construct a monadic catamorphism for contexts over <tt>f</tt> with
--   holes of type <tt>b</tt>, from the given monadic algebra.
freeM' :: forall m h f a b. (HDifunctor f, Monad m) => AlgM' m f a -> NatM m b a -> NatM m (Cxt h f a b) a

-- | Construct a monadic catamorphism from the given monadic algebra.
cataM' :: forall m f a. (HDifunctor f, Monad m) => AlgM' m f a -> NatM m (Term f) a

-- | This type represents a context function.
type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)

-- | This type represents a signature function.
type SigFun f g = forall (a :: * -> *) (b :: * -> *). f a b :-> g a b

-- | This type represents a term homomorphism.
type Hom f g = SigFun f (Context g)

-- | Apply a term homomorphism recursively to a term/context.
appHom :: forall f g. (HDifunctor f, HDifunctor g) => Hom f g -> CxtFun f g

-- | Apply a term homomorphism recursively to a term/context. This is a
--   top-down variant of <a>appHom</a>.
appHom' :: forall f g. (HDifunctor g) => Hom f g -> CxtFun f g

-- | Compose two term homomorphisms.
compHom :: (HDifunctor g, HDifunctor h) => Hom g h -> Hom f g -> Hom f h

-- | This function applies a signature function to the given context.
appSigFun :: forall f g. (HDifunctor f) => SigFun f g -> CxtFun f g

-- | This function applies a signature function to the given context.
appSigFun' :: forall f g. (HDifunctor g) => SigFun f g -> CxtFun f g

-- | This function composes two signature functions.
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h

-- | Lifts the given signature function to the canonical term homomorphism.
hom :: HDifunctor g => SigFun f g -> Hom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> Hom f g -> Alg f a

-- | This type represents a monadic context function.
type CxtFunM m f g = forall h. SigFunM m (Cxt h f) (Cxt h g)

-- | This type represents a monadic signature function.
type SigFunM m f g = forall (a :: * -> *) (b :: * -> *). NatM m (f a b) (g a b)

-- | This type represents a monadic term homomorphism.
type HomM m f g = SigFunM m f (Cxt Hole g)

-- | Lift the given signature function to a monadic signature function.
--   Note that term homomorphisms are instances of signature functions.
--   Hence this function also applies to term homomorphisms.
sigFunM :: Monad m => SigFun f g -> SigFunM m f g

-- | Lift the give monadic signature function to a monadic term
--   homomorphism.
hom' :: (HDifunctor f, HDifunctor g, Monad m) => SigFunM m f g -> HomM m f g

-- | Apply a monadic term homomorphism recursively to a term/context.
appHomM :: forall f g m. (HDitraversable f, Monad m, HDifunctor g) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM| which only works for terms.
appTHomM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g) => HomM m f g -> Term f i -> m (Term g i)

-- | Apply a monadic term homomorphism recursively to a term/context. This
--   is a top-down variant of <a>appHomM</a>.
appHomM' :: forall f g m. (HDitraversable g, Monad m) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM'| which only works for terms.
appTHomM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g) => HomM m f g -> Term f i -> m (Term g i)

-- | Lift the given signature function to a monadic term homomorphism.
homM :: (HDifunctor g, Monad m) => SigFun f g -> HomM m f g

-- | This function applies a monadic signature function to the given
--   context.
appSigFunM :: forall m f g. (HDitraversable f, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunM| which only works for terms.
appTSigFunM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g) => SigFunM m f g -> Term f i -> m (Term g i)

-- | This function applies a monadic signature function to the given
--   context. This is a top-down variant of <a>appSigFunM</a>.
appSigFunM' :: forall m f g. (HDitraversable g, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunM'| which only works for terms.
appTSigFunM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g) => SigFunM m f g -> Term f i -> m (Term g i)

-- | Compose two monadic term homomorphisms.
compHomM :: (HDitraversable g, HDifunctor h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h

-- | This function composes two monadic signature functions.
compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h

-- | Compose a monadic algebra with a monadic term homomorphism to get a
--   new monadic algebra.
compAlgM :: (HDitraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a

-- | Compose a monadic algebra with a term homomorphism to get a new
--   monadic algebra.
compAlgM' :: (HDitraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.Param.Multi.Sum

-- | Signature containment relation for automatic injections. The left-hand
--   must be an atomic signature, where as the right-hand side must have a
--   list-like structure. Examples include <tt>f :&lt;: f :+: g</tt> and
--   <tt>g :&lt;: f :+: (g :+: h)</tt>, non-examples include <tt>f :+: g
--   :&lt;: f :+: (g :+: h)</tt> and <tt>f :&lt;: (f :+: g) :+: h</tt>.
class (sub :: (* -> *) -> (* -> *) -> * -> *) :<: sup

-- | Formal sum of signatures (difunctors).
data ( f (:+:) g ) (a :: * -> *) (b :: * -> *) i

-- | Utility function to case on a higher-order difunctor sum, without
--   exposing the internal representation of sums.
caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c
proj :: (:<:) sub sup => NatM Maybe (sup a b) (sub a b)
proj2 :: forall f a b i g1 g2. ((:<:) g1 f, (:<:) g2 f) => f a b i -> Maybe ((:+:) g2 g1 a b i)
proj3 :: forall f a b i g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => f a b i -> Maybe ((:+:) g3 ((:+:) g2 g1) a b i)
proj4 :: forall f a b i g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => f a b i -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) a b i)
proj5 :: forall f a b i g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => f a b i -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) a b i)
proj6 :: forall f a b i g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => f a b i -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) a b i)
proj7 :: forall f a b i g1 g2 g3 g4 g5 g6 g7. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => f a b i -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) a b i)
proj8 :: forall f a b 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) => f a b i -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) a b i)
proj9 :: forall f a b 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) => f a b i -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) a b i)
proj10 :: forall f a b 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) => f a b i -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) a b i)

-- | Project the outermost layer of a term to a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>project</tt><i>n</i> instead.
project :: (g :<: f) => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))
project2 :: forall h f a b i g1 g2. ((:<:) g1 f, (:<:) g2 f) => Cxt h f a b i -> Maybe ((:+:) g2 g1 a (Cxt h f a b) i)
project3 :: forall h f a b i g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => Cxt h f a b i -> Maybe ((:+:) g3 ((:+:) g2 g1) a (Cxt h f a b) i)
project4 :: forall h f a b i g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => Cxt h f a b i -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) a (Cxt h f a b) i)
project5 :: forall h f a b i g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => Cxt h f a b i -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) a (Cxt h f a b) i)
project6 :: forall h f a b i g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => Cxt h f a b i -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) a (Cxt h f a b) i)
project7 :: forall h f a b 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 b i -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) a (Cxt h f a b) i)
project8 :: forall h f a b 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 b i -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) a (Cxt h f a b) i)
project9 :: forall h f a b 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 b i -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) a (Cxt h f a b) i)
project10 :: forall h f a b 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 b i -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) a (Cxt h f a b) i)

-- | Tries to coerce a term<i>context to a term</i>context over a
--   sub-signature. If the signature <tt>g</tt> is compound of <i>n</i>
--   atomic signatures, use <tt>deepProject</tt><i>n</i> instead.
deepProject :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i)
deepProject2 :: forall f i g1 g2. (HDitraversable ((:+:) g2 g1), (:<:) g1 f, (:<:) g2 f) => Term f i -> Maybe (Term ((:+:) g2 g1) i)
deepProject3 :: forall f i g1 g2 g3. (HDitraversable ((:+:) g3 ((:+:) g2 g1)), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => Term f i -> Maybe (Term ((:+:) g3 ((:+:) g2 g1)) i)
deepProject4 :: forall f i g1 g2 g3 g4. (HDitraversable ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => Term f i -> Maybe (Term ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) i)
deepProject5 :: forall f i g1 g2 g3 g4 g5. (HDitraversable ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => Term f i -> Maybe (Term ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) i)
deepProject6 :: forall f i g1 g2 g3 g4 g5 g6. (HDitraversable ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => Term f i -> Maybe (Term ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) i)
deepProject7 :: forall f i g1 g2 g3 g4 g5 g6 g7. (HDitraversable ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => Term f i -> Maybe (Term ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) i)
deepProject8 :: forall f i g1 g2 g3 g4 g5 g6 g7 g8. (HDitraversable ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => Term f i -> Maybe (Term ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) i)
deepProject9 :: forall f i g1 g2 g3 g4 g5 g6 g7 g8 g9. (HDitraversable ((:+:) 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) => Term f i -> Maybe (Term ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) i)
deepProject10 :: forall f i g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (HDitraversable ((:+:) 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) => Term f i -> Maybe (Term ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))) i)
inj :: (:<:) sub sup => sub a b :-> sup a b
inj2 :: forall g a b i f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 a b i -> g a b i
inj3 :: forall g a b i f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) a b i -> g a b i
inj4 :: forall g a b i f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) a b i -> g a b i
inj5 :: forall g a b i f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) a b i -> g a b i
inj6 :: forall g a b 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 b i -> g a b i
inj7 :: forall g a b 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 b i -> g a b i
inj8 :: forall g a b 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 b i -> g a b i
inj9 :: forall g a b 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 b i -> g a b i
inj10 :: forall g a b 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 b i -> g a b i

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject :: (g :<: f) => g a (Cxt h f a b) :-> Cxt h f a b
inject2 :: forall h g a b i f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 a (Cxt h g a b) i -> Cxt h g a b i
inject3 :: forall h g a b i f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) a (Cxt h g a b) i -> Cxt h g a b i
inject4 :: forall h g a b i f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) a (Cxt h g a b) i -> Cxt h g a b i
inject5 :: forall h g a b i f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) a (Cxt h g a b) i -> Cxt h g a b i
inject6 :: forall h g a b 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 (Cxt h g a b) i -> Cxt h g a b i
inject7 :: forall h g a b 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 (Cxt h g a b) i -> Cxt h g a b i
inject8 :: forall h g a b 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 (Cxt h g a b) i -> Cxt h g a b i
inject9 :: forall h g a b 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 (Cxt h g a b) i -> Cxt h g a b i
inject10 :: forall h g a b 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 (Cxt h g a b) i -> Cxt h g a b i

-- | Inject a term over a sub signature to a term over larger signature. If
--   the signature <tt>g</tt> is compound of <i>n</i> atomic signatures,
--   use <tt>deepInject</tt><i>n</i> instead.
deepInject :: (HDifunctor g, g :<: f) => CxtFun g f
deepInject2 :: forall g f1 f2. (HDifunctor ((:+:) f2 f1), (:<:) f1 g, (:<:) f2 g) => CxtFun ((:+:) f2 f1) g
deepInject3 :: forall g f1 f2 f3. (HDifunctor ((:+:) f3 ((:+:) f2 f1)), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => CxtFun ((:+:) f3 ((:+:) f2 f1)) g
deepInject4 :: forall g f1 f2 f3 f4. (HDifunctor ((:+:) 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. (HDifunctor ((:+:) 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. (HDifunctor ((:+:) 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. (HDifunctor ((:+:) 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. (HDifunctor ((:+:) 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. (HDifunctor ((:+:) 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. (HDifunctor ((:+:) 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

-- | This function injects a whole context into another context.
injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b

-- | This function lifts the given functor to a context.
liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b
instance (GHC.Show.Show (f a b i), GHC.Show.Show (g a b i)) => GHC.Show.Show ((Data.Comp.Param.Multi.Ops.:+:) f g a b i)
instance (GHC.Classes.Ord (f a b i), GHC.Classes.Ord (g a b i)) => GHC.Classes.Ord ((Data.Comp.Param.Multi.Ops.:+:) f g a b i)
instance (GHC.Classes.Eq (f a b i), GHC.Classes.Eq (g a b i)) => GHC.Classes.Eq ((Data.Comp.Param.Multi.Ops.:+:) f g a b i)


-- | This module defines equality for signatures, which lifts to equality
--   for terms.
module Data.Comp.Param.Multi.Equality

-- | Equality on parametric values. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class PEq a
peq :: PEq a => a i -> a j -> FreshM Bool

-- | Signature equality. An instance <tt>EqHD f</tt> gives rise to an
--   instance <tt>Eq (Term f i)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqHD f
eqHD :: (EqHD f, PEq a) => f Name a i -> f Name a j -> FreshM Bool
instance (Data.Comp.Param.Multi.Equality.EqHD f, Data.Comp.Param.Multi.Equality.EqHD g) => Data.Comp.Param.Multi.Equality.EqHD (f Data.Comp.Param.Multi.Ops.:+: g)
instance Data.Comp.Param.Multi.Equality.EqHD f => Data.Comp.Param.Multi.Equality.EqHD (Data.Comp.Param.Multi.Term.Cxt h f)
instance (Data.Comp.Param.Multi.Equality.EqHD f, Data.Comp.Param.Multi.Equality.PEq a) => Data.Comp.Param.Multi.Equality.PEq (Data.Comp.Param.Multi.Term.Cxt h f Data.Comp.Param.Multi.FreshM.Name a)
instance (Data.Comp.Param.Multi.HDifunctor.HDifunctor f, Data.Comp.Param.Multi.Equality.EqHD f) => GHC.Classes.Eq (Data.Comp.Param.Multi.Term.Term f i)
instance GHC.Classes.Eq a => Data.Comp.Param.Multi.Equality.PEq (Data.Comp.Multi.HFunctor.K a)
instance Data.Comp.Param.Multi.Equality.PEq Data.Comp.Param.Multi.FreshM.Name


-- | This module defines ordering of signatures, which lifts to ordering of
--   terms and contexts.
module Data.Comp.Param.Multi.Ordering

-- | Ordering of parametric values.
class PEq a => POrd a
pcompare :: POrd a => a i -> a j -> FreshM Ordering

-- | Signature ordering. An instance <tt>OrdHD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqHD f => OrdHD f
compareHD :: (OrdHD f, POrd a) => f Name a i -> f Name a j -> FreshM Ordering
instance (Data.Comp.Param.Multi.Ordering.OrdHD f, Data.Comp.Param.Multi.Ordering.OrdHD g) => Data.Comp.Param.Multi.Ordering.OrdHD (f Data.Comp.Param.Multi.Ops.:+: g)
instance Data.Comp.Param.Multi.Ordering.OrdHD f => Data.Comp.Param.Multi.Ordering.OrdHD (Data.Comp.Param.Multi.Term.Cxt h f)
instance (Data.Comp.Param.Multi.Ordering.OrdHD f, Data.Comp.Param.Multi.Ordering.POrd a) => Data.Comp.Param.Multi.Ordering.POrd (Data.Comp.Param.Multi.Term.Cxt h f Data.Comp.Param.Multi.FreshM.Name a)
instance (Data.Comp.Param.Multi.HDifunctor.HDifunctor f, Data.Comp.Param.Multi.Ordering.OrdHD f) => GHC.Classes.Ord (Data.Comp.Param.Multi.Term.Term f i)
instance GHC.Classes.Ord a => Data.Comp.Param.Multi.Ordering.POrd (Data.Comp.Multi.HFunctor.K a)
instance Data.Comp.Param.Multi.Ordering.POrd Data.Comp.Param.Multi.FreshM.Name


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>HDifunctor</a>, <a>ShowHD</a>, and <a>EqHD</a>.
module Data.Comp.Param.Multi.Derive

-- | Helper function for generating a list of instances for a list of named
--   signatures. For example, in order to derive instances <a>Functor</a>
--   and <tt>ShowF</tt> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [makeFunctor, makeShowF] [''Exp])
--   </pre>
derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]

-- | Signature equality. An instance <tt>EqHD f</tt> gives rise to an
--   instance <tt>Eq (Term f i)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqHD f
eqHD :: (EqHD f, PEq a) => f Name a i -> f Name a j -> FreshM Bool

-- | Derive an instance of <a>EqHD</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeEqHD :: Name -> Q [Dec]

-- | Signature ordering. An instance <tt>OrdHD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqHD f => OrdHD f
compareHD :: (OrdHD f, POrd a) => f Name a i -> f Name a j -> FreshM Ordering

-- | Derive an instance of <a>OrdHD</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeOrdHD :: Name -> Q [Dec]

-- | Signature printing. An instance <tt>ShowHD f</tt> gives rise to an
--   instance <tt>Show (Term f i)</tt>.
class ShowHD f
showHD :: ShowHD f => f Name (K (FreshM String)) i -> FreshM String

-- | Derive an instance of <a>ShowHD</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeShowHD :: Name -> Q [Dec]

-- | This class represents higher-order difunctors.
class HDifunctor f

-- | Derive an instance of <a>HDifunctor</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeHDifunctor :: Name -> Q [Dec]

-- | Derive smart constructors for a higher-order difunctor. The smart
--   constructors are similar to the ordinary constructors, but a 'inject .
--   hdimap Var id' is automatically inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with annotations for a higher-order
--   difunctor. The smart constructors are similar to the ordinary
--   constructors, but a 'injectA . hdimap Var id' is automatically
--   inserted.
smartAConstructors :: Name -> Q [Dec]

-- | Given the name of a type class, where the first parameter is a
--   higher-order difunctor, lift it to sums of higher-order difunctors.
--   Example: <tt>class ShowHD f where ...</tt> is lifted as <tt>instance
--   (ShowHD f, ShowHD g) =&gt; ShowHD (f :+: g) where ... </tt>.
liftSum :: Name -> Q [Dec]


-- | This module defines showing of signatures, which lifts to showing of
--   terms.
module Data.Comp.Param.Multi.Show

-- | Signature printing. An instance <tt>ShowHD f</tt> gives rise to an
--   instance <tt>Show (Term f i)</tt>.
class ShowHD f
showHD :: ShowHD f => f Name (K (FreshM String)) i -> FreshM String
instance (Data.Comp.Param.Multi.Derive.Show.ShowHD f, Data.Comp.Param.Multi.Derive.Show.ShowHD g) => Data.Comp.Param.Multi.Derive.Show.ShowHD (f Data.Comp.Param.Multi.Ops.:+: g)
instance (Data.Comp.Param.Multi.HDifunctor.HDifunctor f, Data.Comp.Param.Multi.Derive.Show.ShowHD f) => Data.Comp.Param.Multi.Derive.Show.ShowHD (Data.Comp.Param.Multi.Term.Cxt h f)
instance (Data.Comp.Param.Multi.HDifunctor.HDifunctor f, Data.Comp.Param.Multi.Derive.Show.ShowHD f) => GHC.Show.Show (Data.Comp.Param.Multi.Term.Term f i)
instance (Data.Comp.Param.Multi.Derive.Show.ShowHD f, GHC.Show.Show p) => Data.Comp.Param.Multi.Derive.Show.ShowHD (f Data.Comp.Param.Multi.Ops.:&: p)


-- | This module defines annotations on signatures.
module Data.Comp.Param.Multi.Annotation

-- | This data type adds a constant product to a signature.
data ( f (:&:) p ) (a :: * -> *) (b :: * -> *) i
(:&:) :: f a b i -> p -> (:&:) f p i

-- | Formal product of signatures (higher-order difunctors).
data ( f (:*:) g ) a b i
(:*:) :: f a b i -> g a b i -> (:*:) f g a b i

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn (s :: (* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p

-- | Inject an annotation over a signature.
injectA :: DistAnn s p s' => p -> s a b :-> s' a b

-- | Project an annotation from a signature.
projectA :: DistAnn s p s' => s' a b :-> (s a b :&: p)
class RemA (s :: (* -> *) -> (* -> *) -> * -> *) s' | s -> s'

-- | Remove annotations from a signature.
remA :: RemA s s' => s a b :-> s' a b

-- | Transform a function with a domain constructed from a higher-order
--   difunctor to a function with a domain constructed with the same
--   higher-order difunctor, but with an additional annotation.
liftA :: (RemA s s') => (s' a b :-> t) -> s a b :-> t

-- | Transform a function with a domain constructed from a higher-order
--   difunctor to a function with a domain constructed with the same
--   higher-order difunctor, but with an additional annotation.
liftA' :: (DistAnn s' p s, HDifunctor s') => (s' a b :-> Cxt h s' c d) -> s a b :-> Cxt h s c d

-- | Strip the annotations from a term over a higher-order difunctor with
--   annotations.
stripA :: (RemA g f, HDifunctor g) => CxtFun g f

-- | Lift a term homomorphism over signatures <tt>f</tt> and <tt>g</tt> to
--   a term homomorphism over the same signatures, but extended with
--   annotations.
propAnn :: (DistAnn f p f', DistAnn g p g', HDifunctor g) => Hom f g -> Hom f' g'

-- | Lift a monadic term homomorphism over signatures <tt>f</tt> and
--   <tt>g</tt> to a monadic term homomorphism over the same signatures,
--   but extended with annotations.
propAnnM :: (DistAnn f p f', DistAnn g p g', HDifunctor g, Monad m) => HomM m f g -> HomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, HDifunctor f) => p -> CxtFun f g

-- | This function is similar to <a>project</a> but applies to signatures
--   with an annotation which is then ignored.
project' :: (RemA f f', s :<: f') => Cxt h f a b i -> Maybe (s a (Cxt h f a b) i)


-- | This module defines the infrastructure necessary to use <i>Generalised
--   Parametric Compositional Data Types</i>. Generalised Parametric
--   Compositional Data Types is an extension of Compositional Data Types
--   with parametric higher-order abstract syntax (PHOAS) for usage with
--   binders, and GADTs. Generalised Parametric Compositional Data Types
--   combines Generalised Compositional Data Types (<a>Data.Comp.Multi</a>)
--   and Parametric Compositional Data Types (<a>Data.Comp.Param</a>).
--   Examples of usage are bundled with the package in the library
--   <tt>examples/Examples/Param.Multi</tt>.
module Data.Comp.Param.Multi


-- | This modules defines the <a>Desugar</a> type class for desugaring of
--   terms.
module Data.Comp.Param.Multi.Desugar

-- | The desugaring term homomorphism.
class (HDifunctor f, HDifunctor g) => Desugar f g
desugHom :: Desugar f g => Hom f g
desugHom' :: Desugar f g => f a (Cxt h g a b) :-> Cxt h g a b

-- | Desugar a term.
desugar :: Desugar f g => Term f :-> Term g

-- | Lift desugaring to annotated terms.
desugarA :: (HDifunctor f', HDifunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' :-> Term g'
instance (Data.Comp.Param.Multi.Desugar.Desugar f h, Data.Comp.Param.Multi.Desugar.Desugar g h) => Data.Comp.Param.Multi.Desugar.Desugar (f Data.Comp.Param.Multi.Ops.:+: g) h
instance (Data.Comp.Param.Multi.HDifunctor.HDifunctor f, Data.Comp.Param.Multi.HDifunctor.HDifunctor g, f Data.Comp.Param.Multi.Ops.:<: g) => Data.Comp.Param.Multi.Desugar.Desugar f g


-- | This module provides operators on difunctors.
module Data.Comp.Param.Ops

-- | Formal sum of signatures (difunctors).
data ( f (:+:) g ) a b
Inl :: (f a b) -> (:+:) f g a b
Inr :: (g a b) -> (:+:) f g a b

-- | Utility function to case on a difunctor sum, without exposing the
--   internal representation of sums.
caseD :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c

-- | Signature containment relation for automatic injections. The left-hand
--   must be an atomic signature, where as the right-hand side must have a
--   list-like structure. Examples include <tt>f :&lt;: f :+: g</tt> and
--   <tt>g :&lt;: f :+: (g :+: h)</tt>, non-examples include <tt>f :+: g
--   :&lt;: f :+: (g :+: h)</tt> and <tt>f :&lt;: (f :+: g) :+: h</tt>.
class sub :<: sup
inj :: (:<:) sub sup => sub a b -> sup a b
proj :: (:<:) sub sup => sup a b -> Maybe (sub a b)

-- | Formal product of signatures (difunctors).
data ( f (:*:) g ) a b
(:*:) :: f a b -> g a b -> (:*:) f g a b
ffst :: (f :*: g) a b -> f a b
fsnd :: (f :*: g) a b -> g a b

-- | This data type adds a constant product to a signature.
data ( f (:&:) p ) a b
(:&:) :: f a b -> p -> (:&:) f p a b

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p

-- | Inject an annotation over a signature.
injectA :: DistAnn s p s' => p -> s a b -> s' a b

-- | Project an annotation from a signature.
projectA :: DistAnn s p s' => s' a b -> (s a b, p)
class RemA s s' | s -> s'

-- | Remove annotations from a signature.
remA :: RemA s s' => s a b -> s' a b
instance Data.Comp.Param.Ops.RemA s s' => Data.Comp.Param.Ops.RemA ((f Data.Comp.Param.Ops.:&: p) Data.Comp.Param.Ops.:+: s) (f Data.Comp.Param.Ops.:+: s')
instance Data.Comp.Param.Ops.RemA (f Data.Comp.Param.Ops.:&: p) f
instance Data.Comp.Param.Ops.DistAnn f p (f Data.Comp.Param.Ops.:&: p)
instance Data.Comp.Param.Ops.DistAnn s p s' => Data.Comp.Param.Ops.DistAnn (f Data.Comp.Param.Ops.:+: s) p ((f Data.Comp.Param.Ops.:&: p) Data.Comp.Param.Ops.:+: s')
instance Data.Comp.Param.Difunctor.Difunctor f => Data.Comp.Param.Difunctor.Difunctor (f Data.Comp.Param.Ops.:&: p)
instance Data.Comp.Param.Ditraversable.Ditraversable f => Data.Comp.Param.Ditraversable.Ditraversable (f Data.Comp.Param.Ops.:&: p)
instance f Data.Comp.Param.Ops.:<: f
instance f Data.Comp.Param.Ops.:<: (f Data.Comp.Param.Ops.:+: g)
instance (f Data.Comp.Param.Ops.:<: g) => f Data.Comp.Param.Ops.:<: (h Data.Comp.Param.Ops.:+: g)
instance (Data.Comp.Param.Difunctor.Difunctor f, Data.Comp.Param.Difunctor.Difunctor g) => Data.Comp.Param.Difunctor.Difunctor (f Data.Comp.Param.Ops.:+: g)
instance (Data.Comp.Param.Ditraversable.Ditraversable f, Data.Comp.Param.Ditraversable.Ditraversable g) => Data.Comp.Param.Ditraversable.Ditraversable (f Data.Comp.Param.Ops.:+: g)


-- | This module defines the central notion of <i>parametrised terms</i>
--   and their generalisation to parametrised contexts.
module Data.Comp.Param.Term

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes, and zero or more parameters. The
--   first parameter is a phantom type indicating whether the context has
--   holes. The second paramater is the signature of the context, in the
--   form of a <a>Data.Comp.Param.Difunctor</a>. The third parameter is the
--   type of parameters, and the fourth parameter is the type of holes.
data Cxt :: * -> (* -> * -> *) -> * -> * -> *
[In] :: f a (Cxt h f a b) -> Cxt h f a b
[Hole] :: b -> Cxt Hole f a b
[Var] :: a -> Cxt h f a b

-- | Phantom type used to define <a>Context</a>.
data Hole

-- | Phantom type used to define <a>Term</a>.
data NoHole

-- | A term is a context with no holes, where all occurrences of the
--   contravariant parameter is fully parametric.
newtype Term f
Term :: forall a. Trm f a -> Term f
[unTerm] :: Term f -> forall a. Trm f a

-- | "Preterms"
type Trm f a = Cxt NoHole f a ()

-- | A context may contain holes.
type Context = Cxt Hole

-- | Convert a difunctorial value into a context.
simpCxt :: Difunctor f => f a b -> Cxt Hole f a b
toCxt :: Difunctor f => Trm f a -> Cxt h f a b

-- | This combinator maps a function over a context by applying the
--   function to each hole.
cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c

-- | Monads for which embedded <tt>Trm</tt> values, which are parametric at
--   top level, can be made into monadic <tt>Term</tt> values, i.e.
--   "pushing the parametricity inwards".
class ParamFunctor m
termM :: ParamFunctor m => (forall a. m (Trm f a)) -> m (Term f)
instance Data.Comp.Param.Term.ParamFunctor GHC.Base.Maybe
instance Data.Comp.Param.Term.ParamFunctor (Data.Either.Either a)
instance Data.Comp.Param.Term.ParamFunctor []


-- | This module defines the notion of algebras and catamorphisms, and
--   their generalizations to e.g. monadic versions and other (co)recursion
--   schemes.
module Data.Comp.Param.Algebra

-- | This type represents an algebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>.
type Alg f a = f a a -> a

-- | Construct a catamorphism for contexts over <tt>f</tt> with holes of
--   type <tt>b</tt>, from the given algebra.
free :: forall h f a b. Difunctor f => Alg f a -> (b -> a) -> Cxt h f a b -> a

-- | Construct a catamorphism from the given algebra.
cata :: forall f a. Difunctor f => Alg f a -> Term f -> a

-- | A generalisation of <a>cata</a> from terms over <tt>f</tt> to contexts
--   over <tt>f</tt>, where the holes have the type of the algebra carrier.
cata' :: Difunctor f => Alg f a -> Cxt h f a a -> a

-- | This function applies a whole context into another context.
appCxt :: Difunctor f => Context f a (Cxt h f a b) -> Cxt h f a b

-- | This type represents a monadic algebra. It is similar to <a>Alg</a>
--   but the return type is monadic.
type AlgM m f a = f a a -> m a

-- | Convert a monadic algebra into an ordinary algebra with a monadic
--   carrier.
algM :: (Ditraversable f, Monad m) => AlgM m f a -> Alg f (m a)

-- | Construct a monadic catamorphism for contexts over <tt>f</tt> with
--   holes of type <tt>b</tt>, from the given monadic algebra.
freeM :: forall m h f a b. (Ditraversable f, Monad m) => AlgM m f a -> (b -> m a) -> Cxt h f a b -> m a

-- | Construct a monadic catamorphism from the given monadic algebra.
cataM :: forall m f a. (Ditraversable f, Monad m) => AlgM m f a -> Term f -> m a

-- | A generalisation of <a>cataM</a> from terms over <tt>f</tt> to
--   contexts over <tt>f</tt>, where the holes have the type of the monadic
--   algebra carrier.
cataM' :: forall m h f a. (Ditraversable f, Monad m) => AlgM m f a -> Cxt h f a (m a) -> m a

-- | This type represents a context function.
type CxtFun f g = forall h a b. Cxt h f a b -> Cxt h g a b

-- | This type represents a signature function.
type SigFun f g = forall a b. f a b -> g a b

-- | This type represents a term homomorphism.
type Hom f g = SigFun f (Context g)

-- | Apply a term homomorphism recursively to a term/context.
appHom :: forall f g. (Difunctor f, Difunctor g) => Hom f g -> CxtFun f g

-- | Apply a term homomorphism recursively to a term/context.
appHom' :: forall f g. (Difunctor g) => Hom f g -> CxtFun f g

-- | Compose two term homomorphisms.
compHom :: (Difunctor g, Difunctor h) => Hom g h -> Hom f g -> Hom f h

-- | This function applies a signature function to the given context.
appSigFun :: forall f g. (Difunctor f) => SigFun f g -> CxtFun f g

-- | This function applies a signature function to the given context. This
--   is a top-bottom variant of <a>appSigFun</a>.
appSigFun' :: forall f g. (Difunctor g) => SigFun f g -> CxtFun f g

-- | This function composes two signature functions.
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h

-- | This function composes a term homomorphism and a signature function.
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h

-- | This function composes a term homomorphism and a signature function.
compSigFunHom :: (Difunctor g) => SigFun g h -> Hom f g -> Hom f h

-- | Lifts the given signature function to the canonical term homomorphism.
hom :: Difunctor g => SigFun f g -> Hom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (Difunctor f, Difunctor g) => Alg g a -> Hom f g -> Alg f a
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a

-- | This type represents a monadic context function.
type CxtFunM m f g = forall h. SigFunM m (Cxt h f) (Cxt h g)

-- | This type represents a monadic signature function.
type SigFunM m f g = forall a b. f a b -> m (g a b)

-- | This type represents a monadic term homomorphism.
type HomM m f g = SigFunM m f (Context g)

-- | This type represents a monadic signature function. It is similar to
--   <a>SigFunM</a> but has monadic values also in the domain.
type SigFunMD m f g = forall a b. f a (m b) -> m (g a b)

-- | This type represents a monadic term homomorphism. It is similar to
--   <a>HomM</a> but has monadic values also in the domain.
type HomMD m f g = SigFunMD m f (Context g)

-- | Lift the given signature function to a monadic signature function.
--   Note that term homomorphisms are instances of signature functions.
--   Hence this function also applies to term homomorphisms.
sigFunM :: Monad m => SigFun f g -> SigFunM m f g

-- | Apply a monadic term homomorphism recursively to a term/context. The
--   monad is sequenced bottom-up.
appHomM :: forall f g m. (Ditraversable f, Difunctor g, Monad m) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM| which only works for terms.
appTHomM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g) => HomM m f g -> Term f -> m (Term g)

-- | Apply a monadic term homomorphism recursively to a term/context. The
--   monad is sequence top-down.
appHomM' :: forall f g m. (Ditraversable g, Monad m) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM'| which only works for terms.
appTHomM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g) => HomM m f g -> Term f -> m (Term g)

-- | Lift the given signature function to a monadic term homomorphism.
homM :: (Difunctor g, Monad m) => SigFunM m f g -> HomM m f g

-- | This function constructs the unique monadic homomorphism from the
--   initial term algebra to the given term algebra.
homMD :: forall f g m. (Difunctor f, Difunctor g, Monad m) => HomMD m f g -> CxtFunM m f g

-- | This function applies a monadic signature function to the given
--   context.
appSigFunM :: forall m f g. (Ditraversable f, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunM| which only works for terms.
appTSigFunM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g) => SigFunM m f g -> Term f -> m (Term g)

-- | This function applies a monadic signature function to the given
--   context. This is a 'top-down variant of <a>appSigFunM</a>.
appSigFunM' :: forall m f g. (Ditraversable g, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunM'| which only works for terms.
appTSigFunM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g) => SigFunM m f g -> Term f -> m (Term g)

-- | This function applies a signature function to the given context.
appSigFunMD :: forall f g m. (Ditraversable f, Difunctor g, Monad m) => SigFunMD m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunMD| which only works for terms.
appTSigFunMD :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g) => SigFunMD m f g -> Term f -> m (Term g)

-- | Compose two monadic term homomorphisms.
compHomM :: (Ditraversable g, Difunctor h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h

-- | Compose two monadic term homomorphisms.
compHomM' :: (Ditraversable h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h

-- | This function composes two monadic signature functions.
compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h

-- | Compose two monadic term homomorphisms.
compSigFunHomM :: (Ditraversable g, Monad m) => SigFunM m g h -> HomM m f g -> HomM m f h

-- | Compose two monadic term homomorphisms.
compSigFunHomM' :: (Ditraversable h, Monad m) => SigFunM m g h -> HomM m f g -> HomM m f h

-- | Compose a monadic algebra with a monadic signature function to get a
--   new monadic algebra.
compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a

-- | Compose a monadic algebra with a signature function to get a new
--   monadic algebra.
compAlgSigFunM' :: AlgM m g a -> SigFun f g -> AlgM m f a

-- | Compose a monadic algebra with a monadic term homomorphism to get a
--   new monadic algebra.
compAlgM :: (Ditraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a

-- | Compose a monadic algebra with a term homomorphism to get a new
--   monadic algebra.
compAlgM' :: (Ditraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a

-- | This type represents a coalgebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>. The list of <tt>(a,b)</tt>s represent the
--   parameters that may occur in the constructed value. The first
--   component represents the seed of the parameter, and the second
--   component is the (polymorphic) parameter itself. If <tt>f</tt> is
--   itself a binder, then the parameters bound by <tt>f</tt> can be passed
--   to the covariant argument, thereby making them available to sub terms.
type Coalg f a = forall b. a -> [(a, b)] -> Either b (f b (a, [(a, b)]))

-- | Construct an anamorphism from the given coalgebra.
ana :: Difunctor f => Coalg f a -> a -> Term f

-- | This type represents a monadic coalgebra over a difunctor <tt>f</tt>
--   and carrier <tt>a</tt>.
type CoalgM m f a = forall b. a -> [(a, b)] -> m (Either b (f b (a, [(a, b)])))

-- | Construct a monadic anamorphism from the given monadic coalgebra.
anaM :: forall a m f. (Ditraversable f, Monad m) => CoalgM m f a -> a -> forall a. m (Trm f a)

-- | This type represents an r-algebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RAlg f a = f a (Trm f a, a) -> a

-- | Construct a paramorphism from the given r-algebra.
para :: forall f a. Difunctor f => RAlg f a -> Term f -> a

-- | This type represents a monadic r-algebra over a difunctor <tt>f</tt>
--   and carrier <tt>a</tt>.
type RAlgM m f a = f a (Trm f a, a) -> m a

-- | Construct a monadic paramorphism from the given monadic r-algebra.
paraM :: forall m f a. (Ditraversable f, Monad m) => RAlgM m f a -> Term f -> m a

-- | This type represents an r-coalgebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RCoalg f a = forall b. a -> [(a, b)] -> Either b (f b (Either (Trm f b) (a, [(a, b)])))

-- | Construct an apomorphism from the given r-coalgebra.
apo :: Difunctor f => RCoalg f a -> a -> Term f

-- | This type represents a monadic r-coalgebra over a functor <tt>f</tt>
--   and carrier <tt>a</tt>.
type RCoalgM m f a = forall b. a -> [(a, b)] -> m (Either b (f b (Either (Trm f b) (a, [(a, b)]))))

-- | Construct a monadic apomorphism from the given monadic r-coalgebra.
apoM :: forall f m a. (Ditraversable f, Monad m) => RCoalgM m f a -> a -> forall a. m (Trm f a)

-- | This type represents a cv-algebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>.
type CVAlg f a f' = f a (Trm f' a) -> a

-- | Construct a histomorphism from the given cv-algebra.
histo :: forall f f' a. (Difunctor f, DistAnn f a f') => CVAlg f a f' -> Term f -> a

-- | This type represents a monadic cv-algebra over a functor <tt>f</tt>
--   and carrier <tt>a</tt>.
type CVAlgM m f a f' = f a (Trm f' a) -> m a

-- | Construct a monadic histomorphism from the given monadic cv-algebra.
histoM :: forall f f' m a. (Ditraversable f, Monad m, DistAnn f a f') => CVAlgM m f a f' -> Term f -> m a

-- | This type represents a cv-coalgebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>. The list of <tt>(a,b)</tt>s represent the
--   parameters that may occur in the constructed value. The first
--   component represents the seed of the parameter, and the second
--   component is the (polymorphic) parameter itself. If <tt>f</tt> is
--   itself a binder, then the parameters bound by <tt>f</tt> can be passed
--   to the covariant argument, thereby making them available to sub terms.
type CVCoalg f a = forall b. a -> [(a, b)] -> Either b (f b (Context f b (a, [(a, b)])))

-- | Construct a futumorphism from the given cv-coalgebra.
futu :: Difunctor f => CVCoalg f a -> a -> Term f

-- | This type represents a generalised cv-coalgebra over a difunctor
--   <tt>f</tt> and carrier <tt>a</tt>.
type CVCoalg' f a = forall b. a -> [(a, b)] -> Context f b (a, [(a, b)])

-- | Construct a futumorphism from the given generalised cv-coalgebra.
futu' :: Difunctor f => CVCoalg' f a -> a -> Term f

-- | This type represents a monadic cv-coalgebra over a difunctor
--   <tt>f</tt> and carrier <tt>a</tt>.
type CVCoalgM m f a = forall b. a -> [(a, b)] -> m (Either b (f b (Context f b (a, [(a, b)]))))

-- | Construct a monadic futumorphism from the given monadic cv-coalgebra.
futuM :: forall f a m. (Ditraversable f, Monad m) => CVCoalgM m f a -> a -> forall a. m (Trm f a)


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.Param.Sum

-- | Signature containment relation for automatic injections. The left-hand
--   must be an atomic signature, where as the right-hand side must have a
--   list-like structure. Examples include <tt>f :&lt;: f :+: g</tt> and
--   <tt>g :&lt;: f :+: (g :+: h)</tt>, non-examples include <tt>f :+: g
--   :&lt;: f :+: (g :+: h)</tt> and <tt>f :&lt;: (f :+: g) :+: h</tt>.
class sub :<: sup

-- | Formal sum of signatures (difunctors).
data ( f (:+:) g ) a b

-- | Utility function to case on a difunctor sum, without exposing the
--   internal representation of sums.
caseD :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
proj :: (:<:) sub sup => sup a b -> Maybe (sub a b)
proj2 :: forall f a b g1 g2. ((:<:) g1 f, (:<:) g2 f) => f a b -> Maybe ((:+:) g2 g1 a b)
proj3 :: forall f a b g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => f a b -> Maybe ((:+:) g3 ((:+:) g2 g1) a b)
proj4 :: forall f a b g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => f a b -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) a b)
proj5 :: forall f a b g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => f a b -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) a b)
proj6 :: forall f a b g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => f a b -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) a b)
proj7 :: forall f a b g1 g2 g3 g4 g5 g6 g7. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => f a b -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) a b)
proj8 :: forall f a b 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 b -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) a b)
proj9 :: forall f a b 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 b -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) a b)
proj10 :: forall f a b 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 b -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) a b)

-- | Project the outermost layer of a term to a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>project</tt><i>n</i> instead.
project :: (g :<: f) => Cxt h f a b -> Maybe (g a (Cxt h f a b))
project2 :: forall h f a b g1 g2. ((:<:) g1 f, (:<:) g2 f) => Cxt h f a b -> Maybe ((:+:) g2 g1 a (Cxt h f a b))
project3 :: forall h f a b g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => Cxt h f a b -> Maybe ((:+:) g3 ((:+:) g2 g1) a (Cxt h f a b))
project4 :: forall h f a b g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => Cxt h f a b -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) a (Cxt h f a b))
project5 :: forall h f a b g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => Cxt h f a b -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) a (Cxt h f a b))
project6 :: forall h f a b g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => Cxt h f a b -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) a (Cxt h f a b))
project7 :: forall h f a b 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 b -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) a (Cxt h f a b))
project8 :: forall h f a b 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 b -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) a (Cxt h f a b))
project9 :: forall h f a b 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 b -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) a (Cxt h f a b))
project10 :: forall h f a b 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 b -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) a (Cxt h f a b))

-- | Tries to coerce a term<i>context to a term</i>context over a
--   sub-signature. If the signature <tt>g</tt> is compound of <i>n</i>
--   atomic signatures, use <tt>deepProject</tt><i>n</i> instead.
deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)
deepProject2 :: forall f g1 g2. (Ditraversable ((:+:) g2 g1), (:<:) g1 f, (:<:) g2 f) => Term f -> Maybe (Term ((:+:) g2 g1))
deepProject3 :: forall f g1 g2 g3. (Ditraversable ((:+:) g3 ((:+:) g2 g1)), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => Term f -> Maybe (Term ((:+:) g3 ((:+:) g2 g1)))
deepProject4 :: forall f g1 g2 g3 g4. (Ditraversable ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => Term f -> Maybe (Term ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))
deepProject5 :: forall f g1 g2 g3 g4 g5. (Ditraversable ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => Term f -> Maybe (Term ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))
deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Ditraversable ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => Term f -> Maybe (Term ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))
deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Ditraversable ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => Term f -> Maybe (Term ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))
deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Ditraversable ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => Term f -> Maybe (Term ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))
deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Ditraversable ((:+:) 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) => Term f -> Maybe (Term ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))))
deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Ditraversable ((:+:) 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) => Term f -> Maybe (Term ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))))
inj :: (:<:) sub sup => sub a b -> sup a b
inj2 :: forall g a b f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 a b -> g a b
inj3 :: forall g a b f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) a b -> g a b
inj4 :: forall g a b f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) a b -> g a b
inj5 :: forall g a b f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) a b -> g a b
inj6 :: forall g a b 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 b -> g a b
inj7 :: forall g a b 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 b -> g a b
inj8 :: forall g a b 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 b -> g a b
inj9 :: forall g a b 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 b -> g a b
inj10 :: forall g a b 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 b -> g a b

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject :: (g :<: f) => g a (Cxt h f a b) -> Cxt h f a b

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b
inject2 :: forall h g a b f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 a (Cxt h g a b) -> Cxt h g a b
inject3 :: forall h g a b f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) a (Cxt h g a b) -> Cxt h g a b
inject4 :: forall h g a b f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) a (Cxt h g a b) -> Cxt h g a b
inject5 :: forall h g a b f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) a (Cxt h g a b) -> Cxt h g a b
inject6 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
inject7 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
inject8 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
inject9 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b
inject10 :: forall h g a b 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 (Cxt h g a b) -> Cxt h g a b

-- | Inject a term over a sub signature to a term over larger signature. If
--   the signature <tt>g</tt> is compound of <i>n</i> atomic signatures,
--   use <tt>deepInject</tt><i>n</i> instead.
deepInject :: (Difunctor g, g :<: f) => Term g -> Term f
deepInject2 :: forall g f1 f2. (Difunctor ((:+:) f2 f1), (:<:) f1 g, (:<:) f2 g) => CxtFun ((:+:) f2 f1) g
deepInject3 :: forall g f1 f2 f3. (Difunctor ((:+:) f3 ((:+:) f2 f1)), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => CxtFun ((:+:) f3 ((:+:) f2 f1)) g
deepInject4 :: forall g f1 f2 f3 f4. (Difunctor ((:+:) 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. (Difunctor ((:+:) 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. (Difunctor ((:+:) 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. (Difunctor ((:+:) 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. (Difunctor ((:+:) 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. (Difunctor ((:+:) 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. (Difunctor ((:+:) 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

-- | This function injects a whole context into another context.
injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a b

-- | This function lifts the given functor to a context.
liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a b
instance (GHC.Show.Show (f a b), GHC.Show.Show (g a b)) => GHC.Show.Show ((Data.Comp.Param.Ops.:+:) f g a b)
instance (GHC.Classes.Ord (f a b), GHC.Classes.Ord (g a b)) => GHC.Classes.Ord ((Data.Comp.Param.Ops.:+:) f g a b)
instance (GHC.Classes.Eq (f a b), GHC.Classes.Eq (g a b)) => GHC.Classes.Eq ((Data.Comp.Param.Ops.:+:) f g a b)


-- | This module defines equality for signatures, which lifts to equality
--   for terms.
module Data.Comp.Param.Equality

-- | Equality on parametric values. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class PEq a
peq :: PEq a => a -> a -> FreshM Bool

-- | Signature equality. An instance <tt>EqD f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqD f
eqD :: (EqD f, PEq a) => f Name a -> f Name a -> FreshM Bool
instance (Data.Comp.Param.Equality.EqD f, Data.Comp.Param.Equality.EqD g) => Data.Comp.Param.Equality.EqD (f Data.Comp.Param.Ops.:+: g)
instance Data.Comp.Param.Equality.EqD f => Data.Comp.Param.Equality.EqD (Data.Comp.Param.Term.Cxt h f)
instance (Data.Comp.Param.Equality.EqD f, Data.Comp.Param.Equality.PEq a) => Data.Comp.Param.Equality.PEq (Data.Comp.Param.Term.Cxt h f Data.Comp.Param.FreshM.Name a)
instance (Data.Comp.Param.Difunctor.Difunctor f, Data.Comp.Param.Equality.EqD f) => GHC.Classes.Eq (Data.Comp.Param.Term.Term f)
instance Data.Comp.Param.Equality.PEq a => Data.Comp.Param.Equality.PEq [a]
instance GHC.Classes.Eq a => Data.Comp.Param.Equality.PEq a


-- | This module defines ordering of signatures, which lifts to ordering of
--   terms and contexts.
module Data.Comp.Param.Ordering

-- | Ordering of parametric values.
class PEq a => POrd a
pcompare :: POrd a => a -> a -> FreshM Ordering

-- | Signature ordering. An instance <tt>OrdD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqD f => OrdD f
compareD :: (OrdD f, POrd a) => f Name a -> f Name a -> FreshM Ordering
compList :: [Ordering] -> Ordering
instance (Data.Comp.Param.Ordering.OrdD f, Data.Comp.Param.Ordering.OrdD g) => Data.Comp.Param.Ordering.OrdD (f Data.Comp.Param.Ops.:+: g)
instance Data.Comp.Param.Ordering.OrdD f => Data.Comp.Param.Ordering.OrdD (Data.Comp.Param.Term.Cxt h f)
instance (Data.Comp.Param.Ordering.OrdD f, Data.Comp.Param.Ordering.POrd a) => Data.Comp.Param.Ordering.POrd (Data.Comp.Param.Term.Cxt h f Data.Comp.Param.FreshM.Name a)
instance (Data.Comp.Param.Difunctor.Difunctor f, Data.Comp.Param.Ordering.OrdD f) => GHC.Classes.Ord (Data.Comp.Param.Term.Term f)
instance Data.Comp.Param.Ordering.POrd a => Data.Comp.Param.Ordering.POrd [a]
instance GHC.Classes.Ord a => Data.Comp.Param.Ordering.POrd a


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>Difunctor</a>, <tt>Difoldable</tt>, and <a>Ditraversable</a>.
module Data.Comp.Param.Derive

-- | Helper function for generating a list of instances for a list of named
--   signatures. For example, in order to derive instances <a>Functor</a>
--   and <tt>ShowF</tt> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [makeFunctor, makeShowF] [''Exp])
--   </pre>
derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]

-- | Signature equality. An instance <tt>EqD f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqD f
eqD :: (EqD f, PEq a) => f Name a -> f Name a -> FreshM Bool

-- | Derive an instance of <a>EqD</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeEqD :: Name -> Q [Dec]

-- | Signature ordering. An instance <tt>OrdD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqD f => OrdD f
compareD :: (OrdD f, POrd a) => f Name a -> f Name a -> FreshM Ordering

-- | Derive an instance of <a>OrdD</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeOrdD :: Name -> Q [Dec]

-- | Signature printing. An instance <tt>ShowD f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowD f
showD :: ShowD f => f Name (FreshM String) -> FreshM String

-- | Derive an instance of <a>ShowD</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeShowD :: Name -> Q [Dec]

-- | This class represents difunctors, i.e. binary type constructors that
--   are contravariant in the first argument and covariant in the second
--   argument.
class Difunctor f

-- | Derive an instance of <a>Difunctor</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeDifunctor :: Name -> Q [Dec]

-- | Difunctors representing data structures that can be traversed from
--   left to right.
class Difunctor f => Ditraversable f

-- | Derive an instance of <a>Traversable</a> for a type constructor of any
--   first-order kind taking at least one argument.
makeDitraversable :: Name -> Q [Dec]

-- | Derive smart constructors for a difunctor. The smart constructors are
--   similar to the ordinary constructors, but a 'inject . dimap Var id' is
--   automatically inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with annotations for a difunctor. The smart
--   constructors are similar to the ordinary constructors, but a 'injectA
--   . dimap Var id' is automatically inserted.
smartAConstructors :: Name -> Q [Dec]

-- | Given the name of a type class, where the first parameter is a
--   difunctor, lift it to sums of difunctors. Example: <tt>class ShowD f
--   where ...</tt> is lifted as <tt>instance (ShowD f, ShowD g) =&gt;
--   ShowD (f :+: g) where ... </tt>.
liftSum :: Name -> Q [Dec]


-- | This module defines showing of signatures, which lifts to showing of
--   terms.
module Data.Comp.Param.Show

-- | Signature printing. An instance <tt>ShowD f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowD f
showD :: ShowD f => f Name (FreshM String) -> FreshM String
instance (Data.Comp.Param.Derive.Show.ShowD f, Data.Comp.Param.Derive.Show.ShowD g) => Data.Comp.Param.Derive.Show.ShowD (f Data.Comp.Param.Ops.:+: g)
instance (Data.Comp.Param.Difunctor.Difunctor f, Data.Comp.Param.Derive.Show.ShowD f) => Data.Comp.Param.Derive.Show.ShowD (Data.Comp.Param.Term.Cxt h f)
instance (Data.Comp.Param.Difunctor.Difunctor f, Data.Comp.Param.Derive.Show.ShowD f) => GHC.Show.Show (Data.Comp.Param.Term.Term f)
instance (Data.Comp.Param.Derive.Show.ShowD f, GHC.Show.Show p) => Data.Comp.Param.Derive.Show.ShowD (f Data.Comp.Param.Ops.:&: p)


-- | This module defines annotations on signatures.
module Data.Comp.Param.Annotation

-- | This data type adds a constant product to a signature.
data ( f (:&:) p ) a b
(:&:) :: f a b -> p -> (:&:) f p a b

-- | Formal product of signatures (difunctors).
data ( f (:*:) g ) a b
(:*:) :: f a b -> g a b -> (:*:) f g a b

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p

-- | Inject an annotation over a signature.
injectA :: DistAnn s p s' => p -> s a b -> s' a b

-- | Project an annotation from a signature.
projectA :: DistAnn s p s' => s' a b -> (s a b, p)
class RemA s s' | s -> s'

-- | Remove annotations from a signature.
remA :: RemA s s' => s a b -> s' a b

-- | Transform a function with a domain constructed from a functor to a
--   function with a domain constructed with the same functor, but with an
--   additional annotation.
liftA :: (RemA s s') => (s' a b -> t) -> s a b -> t

-- | Transform a function with a domain constructed from a functor to a
--   function with a domain constructed with the same functor, but with an
--   additional annotation.
liftA' :: (DistAnn s' p s, Difunctor s') => (s' a b -> Cxt h s' c d) -> s a b -> Cxt h s c d

-- | Strip the annotations from a term over a functor with annotations.
stripA :: (RemA g f, Difunctor g) => CxtFun g f

-- | Lift a term homomorphism over signatures <tt>f</tt> and <tt>g</tt> to
--   a term homomorphism over the same signatures, but extended with
--   annotations.
propAnn :: (DistAnn f p f', DistAnn g p g', Difunctor g) => Hom f g -> Hom f' g'

-- | Lift a monadic term homomorphism over signatures <tt>f</tt> and
--   <tt>g</tt> to a monadic term homomorphism over the same signatures,
--   but extended with annotations.
propAnnM :: (DistAnn f p f', DistAnn g p g', Difunctor g, Monad m) => HomM m f g -> HomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, Difunctor f) => p -> CxtFun f g

-- | This function is similar to <a>project</a> but applies to signatures
--   with an annotation which is then ignored.
project' :: (RemA f f', s :<: f') => Cxt h f a b -> Maybe (s a (Cxt h f a b))


-- | This module defines the infrastructure necessary to use <i>Parametric
--   Compositional Data Types</i>. Parametric Compositional Data Types is
--   an extension of Compositional Data Types with parametric higher-order
--   abstract syntax (PHOAS) for usage with binders. Examples of usage are
--   bundled with the package in the library
--   <tt>examples/Examples/Param</tt>.
module Data.Comp.Param


-- | This modules defines the <a>Desugar</a> type class for desugaring of
--   terms.
module Data.Comp.Param.Desugar

-- | The desugaring term homomorphism.
class (Difunctor f, Difunctor g) => Desugar f g
desugHom :: Desugar f g => Hom f g
desugHom' :: Desugar f g => f a (Cxt h g a b) -> Cxt h g a b

-- | Desugar a term.
desugar :: Desugar f g => Term f -> Term g

-- | Lift desugaring to annotated terms.
desugarA :: (Difunctor f', Difunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' -> Term g'
instance (Data.Comp.Param.Desugar.Desugar f h, Data.Comp.Param.Desugar.Desugar g h) => Data.Comp.Param.Desugar.Desugar (f Data.Comp.Param.Ops.:+: g) h
instance (Data.Comp.Param.Difunctor.Difunctor f, Data.Comp.Param.Difunctor.Difunctor g, f Data.Comp.Param.Ops.:<: g) => Data.Comp.Param.Desugar.Desugar f g


-- | This modules defines terms &amp; contexts with thunks, with deferred
--   monadic computations.
module Data.Comp.Param.Thunk

-- | This type represents terms with thunks.
type TermT m f = Term (Thunk m :+: f)

-- | This type represents terms with thunks.
type TrmT m f a = Trm (Thunk m :+: f) a

-- | This type represents contexts with thunks.
type CxtT h m f a = Cxt h (Thunk m :+: f) a
data Thunk m a b

-- | This function turns a monadic computation into a thunk.
thunk :: (Thunk m :<: f) => m (Cxt h f a b) -> Cxt h f a b

-- | This function evaluates all thunks until a non-thunk node is found.
whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))
whnf' :: Monad m => TrmT m f a -> m (TrmT m f a)

-- | This function first evaluates the argument term into whnf via
--   <a>whnf</a> and then projects the top-level signature to the desired
--   subsignature. Failure to do the projection is signalled as a failure
--   in the monad.
whnfPr :: (Monad m, g :<: f) => TrmT m f a -> m (g a (TrmT m f a))

-- | This function evaluates all thunks.
nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)

-- | This function evaluates all thunks.
nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)

-- | This function evaluates all thunks while simultaneously projecting the
--   term to a smaller signature. Failure to do the projection is signalled
--   as a failure in the monad as in <a>whnfPr</a>.
nfPr :: (Monad m, Ditraversable g, g :<: f) => TrmT m f a -> m (Trm g a)

-- | This function evaluates all thunks while simultaneously projecting the
--   term to a smaller signature. Failure to do the projection is signalled
--   as a failure in the monad as in <a>whnfPr</a>.
nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, g :<: f) => TermT m f -> m (Term g)
evalStrict :: (Ditraversable g, Monad m, g :<: f) => (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a) -> g (TrmT m f a) (TrmT m f a) -> TrmT m f a

-- | This type represents algebras which have terms with thunks as carrier.
type AlgT m f g = Alg f (TermT m g)

-- | This combinator makes the evaluation of the given functor application
--   strict by evaluating all thunks of immediate subterms.
strict :: (f :<: g, Ditraversable f, Monad m) => f a (TrmT m g a) -> TrmT m g a

-- | This combinator makes the evaluation of the given functor application
--   strict by evaluating all thunks of immediate subterms.
strict' :: (f :<: g, Ditraversable f, Monad m) => f (TrmT m g a) (TrmT m g a) -> TrmT m g a