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


-- | Compositional Data Types
--   
--   Based on Wouter Swierstra's Functional Pearl <i>Data types à la
--   carte</i> (Journal of Functional Programming, 18(4):423-436, 2008),
--   this package provides a framework for defining recursive data types in
--   a compositional manner. The fundamental idea of compositional data
--   types is to separate the signature of a data type from the fixed point
--   construction that produces its recursive structure. By allowing to
--   compose and decompose signatures, <i>compositional data types</i>
--   enable to combine data types in a flexible way. The key point of
--   Wouter Swierstra's original work is to define functions on
--   <i>compositional data types</i> in a compositional manner as well by
--   leveraging Haskell's type class machinery.
--   
--   Building on that foundation, this library provides additional
--   extensions and (run-time) optimisations which make compositional data
--   types usable for practical implementations. In particular, it provides
--   an excellent framework for manipulating and analysing abstract syntax
--   trees in a type-safe manner. Thus, it is perfectly suited for
--   programming language implementations, especially, in an environment
--   consisting of a family of tightly interwoven <i>domain-specific
--   languages</i>.
--   
--   In concrete terms, this package provides the following features:
--   
--   <ul>
--   <li>Compositional data types in the style of Wouter Swierstra's
--   Functional Pearl <i>Data types à la carte</i>.</li>
--   <li>Modular definition of functions on compositional data types
--   through catamorphisms and anamorphisms as well as more structured
--   recursion schemes such as primitive recursion and co-recursion, and
--   course-of-value iteration and co-iteration.</li>
--   <li>Support for monadic computations via monadic variants of all
--   recursion schemes.</li>
--   <li>Support of a succinct programming style over compositional data
--   types via generic programming combinators that allow various forms of
--   generic transformations and generic queries.</li>
--   <li>Generalisation of compositional data types (terms) to
--   compositional data types "with holes" (contexts). This allows flexible
--   reuse of a wide variety of catamorphisms (called <i>term
--   homomorphisms</i>) as well as an efficient composition of them.</li>
--   <li>Operations on signatures, for example, to add and remove
--   annotations of abstract syntax trees. This includes combinators to
--   propagate annotations fully automatically through certain term
--   homomorphisms.</li>
--   <li>Optimisation of the implementation of recursion schemes. This
--   includes <i>short-cut fusion</i> style optimisation rules which yield
--   a performance boost of up to factor six.</li>
--   <li>Automatic derivation of instances of all relevant type classes for
--   using compositional data types via <i>Template Haskell</i>. This
--   includes instances of <a>Prelude.Eq</a>, <a>Prelude.Ord</a> and
--   <a>Prelude.Show</a> that are derived via instances for functorial
--   variants of them. Additionally, also <i>smart constructors</i>, which
--   allow to easily construct inhabitants of compositional data types, are
--   automatically generated.</li>
--   <li><i>Mutually recursive data types</i> and <i>generalised algebraic
--   data types (GADTs)</i>. All of the above is also lifted to families of
--   mutually recursive data types and (more generally) GADTs. This
--   extension resides in the module <a>Data.Comp.Multi</a>.</li>
--   <li><i>Parametric compositional data types</i>. All of the above is
--   also lifted to parametric data types, which enables support for
--   parametric higher-order abstract syntax (PHOAS). This extension
--   resides in the module <a>Data.Comp.Param</a>.</li>
--   <li><i>Generalised parametric compositional data types</i>. All of the
--   above is also lifted to generalised parametric data types, which
--   enables support for typed parametric higher-order abstract syntax
--   (PHOAS). This extension resides in the module
--   <a>Data.Comp.MultiParam</a>.</li>
--   </ul>
--   
--   Examples of using (generalised) (parametric) compositional data types
--   are bundled with the package in the libray <tt>examples</tt>.
@package compdata
@version 0.3


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

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

-- | Abstract notion of a variable (the constructor is hidden).
data Var i

-- | Equality on variables.
varEq :: Var i -> Var j -> Bool

-- | Ordering of variables.
varCompare :: Var i -> Var j -> Ordering

-- | Printing of variables.
varShow :: Var i -> String

-- | Generate a fresh variable.
genVar :: FreshM (Var i)

-- | Change the type of a variable.
varCoerce :: Var i -> Var j

-- | Evaluate a computation that uses fresh variables.
evalFreshM :: FreshM a -> a
instance Monad FreshM


-- | This module defines the empty data type <a>Any</a>, which is used to
--   emulate parametricity ("poor mans parametricity").
module Data.Comp.MultiParam.Any

-- | The empty data type <a>Any</a> is used to emulate parametricity ("poor
--   mans parametricity").
data Any :: * -> *


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

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

-- | Abstract notion of a variable (the constructor is hidden).
data Var

-- | Generate a fresh variable.
genVar :: FreshM Var

-- | Evaluate a computation that uses fresh variables.
evalFreshM :: FreshM a -> a
instance Monad FreshM
instance Eq Var
instance Ord Var
instance Show Var


-- | This module defines the empty data type <a>Any</a>, which is used to
--   emulate parametricity ("poor mans parametricity").
module Data.Comp.Param.Any

-- | The empty data type <a>Any</a> is used to emulate parametricity ("poor
--   mans parametricity").
data Any


-- | 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

-- | 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 Difunctor f => Functor (f a)
instance Difunctor (->)


-- | 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, Monad m) => Ditraversable f m a
dimapM :: Ditraversable f m a => (b -> m c) -> f a b -> m (f a c)
disequence :: Ditraversable f m a => f a (m b) -> m (f a b)
instance [overlap ok] (Monoid w, Ditraversable (->) m Any) => Ditraversable (->) (RWST r w s m) Any
instance [overlap ok] Ditraversable (->) m Any => Ditraversable (->) (ListT m) Any
instance [overlap ok] Ditraversable (->) [] Any
instance [overlap ok] (Monoid w, Ditraversable (->) m Any) => Ditraversable (->) (WriterT w m) Any
instance [overlap ok] Ditraversable (->) m Any => Ditraversable (->) (StateT s m) Any
instance [overlap ok] (Error e, Ditraversable (->) m Any) => Ditraversable (->) (ErrorT e m) Any
instance [overlap ok] Ditraversable (->) (Either e) Any
instance [overlap ok] Ditraversable (->) Maybe Any
instance [overlap ok] Ditraversable (->) m a => Ditraversable (->) (ReaderT r m) a
instance [overlap ok] Ditraversable (->) Identity a
instance [overlap ok] Ditraversable (->) Gen a


-- | 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

-- | 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
injectA :: DistAnn s p s' => p -> s a b -> s' a b
projectA :: DistAnn s p s' => s' a b -> (s a b, p)
class RemA s s' | s -> s'
remA :: RemA s s' => s a b -> s' a b
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [incoherent] Ditraversable f m a => Ditraversable (f :&: p) m a
instance [incoherent] Difunctor f => Difunctor (f :&: p)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (Ditraversable f m a, Ditraversable g m a) => Ditraversable (f :+: g) m a
instance [incoherent] (Difunctor f, Difunctor g) => Difunctor (f :+: g)


-- | This module defines the central notion of <i>parametrized 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 :: * -> (* -> * -> *) -> * -> * -> *
Term :: f a (Cxt h f a b) -> Cxt h f a b
Hole :: b -> Cxt Hole f a b
Place :: 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

-- | The empty data type <a>Any</a> is used to emulate parametricity ("poor
--   mans parametricity").
data Any

-- | A term is a context with no holes, where all occurrences of the
--   contravariant parameter is fully parametric. Parametricity is
--   "emulated" using the empty type <tt>Any</tt>, e.g. a function of type
--   <tt>Any -&gt; T[Any]</tt> is equivalent with <tt>forall b. b -&gt;
--   T[b]</tt>, but the former avoids the impredicative typing extension,
--   and works also in the cases where the codomain type is not a type
--   constructor, e.g. <tt>Any -&gt; (Any,Any)</tt>.
type Term f = Trm f Any
type Trm f a = Cxt NoHole f a ()

-- | A context may contain holes, but must be parametric in the bound
--   parameters. Parametricity is "emulated" using the empty type
--   <tt>Any</tt>, e.g. a function of type <tt>Any -&gt; T[Any]</tt> is
--   equivalent with <tt>forall b. b -&gt; T[b]</tt>, but the former avoids
--   the impredicative typing extension, and works also in the cases where
--   the codomain type is not a type constructor, e.g. <tt>Any -&gt;
--   (Any,Any)</tt>.
type Context = Cxt Hole
type Const f = f Any ()

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

-- | Cast a "pseudo-parametric" context over a signature to a parametric
--   context over the same signature. The usage of <a>unsafeCoerce</a> is
--   safe, because the empty type <a>Any</a> witnesses that all uses of the
--   contravariant argument are parametric.
coerceCxt :: Cxt h f Any b -> forall a. Cxt h f a b
toCxt :: Difunctor f => Trm f a -> Cxt h f a b

-- | This function converts a constant to a term. This assumes that the
--   argument is indeed a constant, i.e. does not have a value for the
--   argument type of the difunctor <tt>f</tt>.
constTerm :: Difunctor f => Const f -> Term f

-- | This is an instance of <a>fmap</a> for <a>Cxt</a>.
fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b'

-- | This is an instance of <a>disequence</a> for <a>Cxt</a>.
disequenceCxt :: Ditraversable f m a => Cxt h f a (m b) -> m (Cxt h f a b)

-- | This is an instance of <tt>dimamM</tt> for <a>Cxt</a>.
dimapMCxt :: Ditraversable f m a => (b -> m b') -> Cxt h f a b -> m (Cxt h f a b')


-- | 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 :: Difunctor f => Alg f a -> (b -> a) -> Cxt h f a b -> a

-- | Construct a catamorphism from the given algebra.
cata :: 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 m a, 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 :: (Ditraversable f m a, 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 :: (Ditraversable f m a, 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' :: (Ditraversable f m a, 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 TermHom f g = SigFun f (Context g)

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

-- | Apply a term homomorphism recursively to a term/context.
appTermHom' :: Difunctor g => TermHom f g -> CxtFun f g

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

-- | This function applies a signature function to the given context.
appSigFun :: 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' :: 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.
compTermHomSigFun :: TermHom g h -> SigFun f g -> TermHom f h

-- | This function composes a term homomorphism and a signature function.
compSigFunTermHom :: Difunctor g => SigFun g h -> TermHom f g -> TermHom f h

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

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (Difunctor f, Difunctor g) => Alg g a -> TermHom 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 TermHomM m f g = SigFunM m f (Context g)

-- | This type represents a monadic signature function. It is similar to
--   'SigFunMD 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
--   'TermHomMD but has monadic values also in the domain.
type TermHomMD 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.
appTermHomM :: (Ditraversable f m Any, Difunctor g) => TermHomM m f g -> CxtFunM m f g

-- | Apply a monadic term homomorphism recursively to a term/context. The
--   monad is sequence top-down.
appTermHomM' :: Ditraversable g m Any => TermHomM m f g -> CxtFunM m f g

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

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

-- | This function applies a monadic signature function to the given
--   context.
appSigFunM :: Ditraversable f m Any => SigFunM m f g -> CxtFunM m f g

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

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

-- | Compose two monadic term homomorphisms.
compTermHomM :: (Ditraversable g m Any, Difunctor h, Monad m) => TermHomM m g h -> TermHomM m f g -> TermHomM 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.
compSigFunTermHomM :: Ditraversable g m Any => SigFunM m g h -> TermHomM m f g -> TermHomM 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 m a, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a

-- | Compose a monadic algebra with a term homomorphism to get a new
--   monadic algebra.
compAlgM' :: (Ditraversable g m a, Monad m) => AlgM m g a -> TermHom 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 :: (Ditraversable f m Any, Monad m) => CoalgM m f a -> a -> m (Term f)

-- | 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 :: 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 :: (Ditraversable f m a, 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 :: (Ditraversable f m Any, Monad m) => RCoalgM m f a -> a -> m (Term f)

-- | 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 :: (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 :: (Ditraversable f m a, 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 :: (Ditraversable f m Any, Monad m) => CVCoalgM m f a -> a -> m (Term f)


-- | 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
inj :: :<: sub sup => sub a b -> sup a b
proj :: :<: sub sup => sup a b -> Maybe (sub a b)

-- | Formal sum of signatures (difunctors).
data (:+:) f g a b
proj2 :: (:<: g1 f, :<: g2 f) => f a b -> Maybe (:+: g2 g1 a b)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a b -> Maybe (:+: g3 (:+: g2 g1) a b)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b)
proj6 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: g1 f, :<: g2 f) => Cxt h f a b -> Maybe (:+: g2 g1 a (Cxt h f a b))
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a b -> Maybe (:+: g3 (:+: g2 g1) a (Cxt h f a b))
project4 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 Maybe Any, :<: g f) => CxtFunM Maybe f g
deepProject2 :: (Ditraversable (:+: g2 g1) Maybe Any, :<: g1 f, :<: g2 f) => CxtFunM Maybe f (:+: g2 g1)
deepProject3 :: (Ditraversable (:+: g3 (:+: g2 g1)) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
deepProject4 :: (Ditraversable (:+: g4 (:+: g3 (:+: g2 g1))) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
deepProject5 :: (Ditraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))
deepProject6 :: (Ditraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
deepProject7 :: (Ditraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) Maybe Any, :<: 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 :: (Ditraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) Maybe Any, :<: 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 :: (Ditraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) Maybe Any, :<: 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 :: (Ditraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))) Maybe Any, :<: 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)))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a b -> g a b
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a b -> g a b
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a b -> g a b
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b -> g a b
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a b -> g a b
inj7 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) -> Cxt h g a b
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a (Cxt h g a b) -> Cxt h g a b
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a (Cxt h g a b) -> Cxt h g a b
inject5 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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) => CxtFun g f
deepInject2 :: (Difunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (Difunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (Difunctor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (Difunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (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 :: (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 :: (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 :: (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 :: (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
injectConst :: (Difunctor g, :<: g f) => Const g -> Cxt h f Any a
injectConst2 :: (Difunctor f1, Difunctor f2, Difunctor g, :<: f1 g, :<: f2 g) => Const (f1 :+: f2) -> Cxt h g Any a
injectConst3 :: (Difunctor f1, Difunctor f2, Difunctor f3, Difunctor g, :<: f1 g, :<: f2 g, :<: f3 g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g Any a
projectConst :: (Difunctor g, :<: g f) => Cxt h f Any a -> Maybe (Const 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 [incoherent] (Eq (f a b), Eq (g a b)) => Eq ((:+:) f g a b)
instance [incoherent] (Ord (f a b), Ord (g a b)) => Ord ((:+:) f g a b)
instance [incoherent] (Show (f a b), Show (g a b)) => Show ((:+:) f g a b)


-- | 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
injectA :: DistAnn s p s' => p -> s a b -> s' a b
projectA :: DistAnn s p s' => s' a b -> (s a b, p)
class RemA s s' | s -> s'
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) => TermHom f g -> TermHom 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) => TermHomM m f g -> TermHomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, Difunctor f) => p -> CxtFun f g
project' :: (:<: s f, RemA s s') => Cxt h f a b -> Maybe (s' a (Cxt h f 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 Var a -> f Var a -> FreshM Bool
instance [incoherent] (Difunctor f, EqD f) => Eq (Term f)
instance [incoherent] (EqD f, PEq a) => PEq (Cxt h f Var a)
instance [incoherent] EqD f => EqD (Cxt h f)
instance [incoherent] (EqD f, EqD g) => EqD (f :+: g)
instance [incoherent] Eq a => 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 Var a -> f Var a -> FreshM Ordering
instance [incoherent] (Difunctor f, OrdD f) => Ord (Term f)
instance [incoherent] (OrdD f, POrd a) => POrd (Cxt h f Var a)
instance [incoherent] OrdD f => OrdD (Cxt h f)
instance [incoherent] (OrdD f, OrdD g) => OrdD (f :+: g)
instance [incoherent] Ord a => POrd a


-- | 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 module defines higher-order functors (Johann, Ghani, POPL '08),
--   i.e. endofunctors on the category of endofunctors.
module Data.Comp.Multi.Functor

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

-- | This type represents natural transformations.
type :-> f g = forall i. f i -> g i

-- | This type represents co-cones from <tt>f</tt> to <tt>a</tt>. <tt>f
--   :=&gt; a</tt> is isomorphic to f :-&gt; K a
type :=> f a = forall i. f i -> a
type NatM m f g = forall i. f i -> m (g i)

-- | The identity Functor.
data I a
I :: a -> I a
unI :: I a -> a

-- | The parametrised constant functor.
data K a b
K :: a -> K a b
unK :: K a b -> a
data A f
A :: f i -> A f
unA :: A f -> f i

-- | This data type denotes the composition of two functor families.
data (:.:) f g e t
Comp :: f -> (g e) -> t -> :.: f g e t
instance [incoherent] Ord a => Ord (K a i)
instance [incoherent] Eq a => Eq (K a i)
instance [incoherent] Functor (K a)


-- | This module defines higher-order foldable functors.
module Data.Comp.Multi.Foldable

-- | Higher-order functors that can be folded.
--   
--   Minimal complete definition: <a>hfoldMap</a> or <a>hfoldr</a>.
class HFunctor h => HFoldable h
hfold :: (HFoldable h, Monoid m) => h (K m) :=> m
hfoldMap :: (HFoldable h, Monoid m) => (a :=> m) -> h a :=> m
hfoldr :: HFoldable h => (a :=> (b -> b)) -> b -> h a :=> b
hfoldl :: HFoldable h => (b -> a :=> b) -> b -> h a :=> b
hfoldr1 :: HFoldable h => (a -> a -> a) -> h (K a) :=> a
hfoldl1 :: HFoldable h => (a -> a -> a) -> h (K a) :=> a
kfoldr :: HFoldable f => (a -> b -> b) -> b -> f (K a) :=> b
kfoldl :: HFoldable f => (b -> a -> b) -> b -> f (K a) :=> b
htoList :: HFoldable f => f a :=> [A a]


-- | This module defines higher-order traversable functors.
module Data.Comp.Multi.Traversable
class HFoldable t => HTraversable t
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 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.MultiParam.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
hfmap :: HFunctor h => (f :-> g) -> h f :-> h g

-- | The identity functor.
data I a
I :: a -> I a
unI :: I a -> a

-- | The parametrised constant functor.
data K a i
K :: a -> K a i
unK :: K a i -> a
data A f
A :: f i -> A f
unA :: A f -> f i

-- | This type represents natural transformations.
type :-> f g = forall i. f i -> g i

-- | This type represents monadic natural transformations.
type NatM m f g = forall i. f i -> m (g i)
instance HDifunctor f => HFunctor (f a)
instance Ord a => Ord (K a i)
instance Eq a => Eq (K a i)
instance Functor (K a)
instance Functor I


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

-- | HDifunctors representing data structures that can be traversed from
--   left to right.
class (HDifunctor f, Monad m) => HDitraversable f m a
hdimapM :: HDitraversable f m a => NatM m b c -> NatM m (f a b) (f a c)
class HFoldable t => HTraversable t
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)
instance [overlap ok] (HDifunctor f, Monad m, HTraversable (f a)) => HDitraversable f m a


-- | This module defines the central notion of <i>generalised parametrised
--   terms</i> and their generalisation to generalised parametrised
--   contexts.
module Data.Comp.MultiParam.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.MultiParam.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 :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> *
Term :: f a (Cxt h f a b) i -> Cxt h f a b i
Hole :: b i -> Cxt Hole f a b i
Place :: 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

-- | The empty data type <a>Any</a> is used to emulate parametricity ("poor
--   mans parametricity").
data Any :: * -> *

-- | A term is a context with no holes, where all occurrences of the
--   contravariant parameter is fully parametric. Parametricity is
--   "emulated" using the empty functor <tt>Any</tt>, e.g. a function of
--   type <tt>Any :-&gt; T[Any]</tt> is equivalent with <tt>forall b. b
--   :-&gt; T[b]</tt>, but the former avoids the impredicative typing
--   extension, and works also in the cases where the codomain type is not
--   a type constructor, e.g. <tt>Any i -&gt; (Any i,Any i)</tt>.
type Term f = Trm f Any
type Trm f a = Cxt NoHole f a (K ())

-- | A context may contain holes, but must be parametric in the bound
--   parameters. Parametricity is "emulated" using the empty functor
--   <tt>Any</tt>, e.g. a function of type <tt>Any :-&gt; T[Any]</tt> is
--   equivalent with <tt>forall b. b :-&gt; T[b]</tt>, but the former
--   avoids the impredicative typing extension, and works also in the cases
--   where the codomain type is not a type constructor, e.g. <tt>Any i
--   -&gt; (Any i,Any i)</tt>.
type Context = Cxt Hole
type Const f i = f Any (K ()) i

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

-- | Cast a "pseudo-parametric" context over a signature to a parametric
--   context over the same signature. The usage of <a>unsafeCoerce</a> is
--   safe, because the empty functor <a>Any</a> witnesses that all uses of
--   the contravariant argument are parametric.
coerceCxt :: Cxt h f Any b i -> forall a. Cxt h f a b i
toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b

-- | This function converts a constant to a term. This assumes that the
--   argument is indeed a constant, i.e. does not have a value for the
--   argument type of the higher-order difunctor <tt>f</tt>.
constTerm :: HDifunctor f => Const f :-> Term f

-- | This is an instance of <a>hfmap</a> for <a>Cxt</a>.
hfmapCxt :: 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 :: HDitraversable f m a => (NatM m b b') -> NatM m (Cxt h f a b) (Cxt h f a b')


-- | 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.MultiParam.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 :: HDifunctor f => Alg f a -> (b :-> a) -> Cxt h f a b :-> a

-- | Construct a catamorphism from the given algebra.
cata :: 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 :: (HDitraversable f m a, 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 :: (HDitraversable f m a, 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 :: (* -> *) g :: (* -> *) a :: (* -> *) -> (* -> *) -> * -> *
Compose :: f (g a) -> Compose a
getCompose :: Compose a -> 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' :: (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' :: (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 TermHom f g = SigFun f (Context g)

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

-- | Apply a term homomorphism recursively to a term/context. This is a
--   top-down variant of <a>appTermHom</a>.
appTermHom' :: HDifunctor g => TermHom f g -> CxtFun f g

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

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

-- | This function applies a signature function to the given context.
appSigFun' :: 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.
termHom :: HDifunctor g => SigFun f g -> TermHom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> TermHom 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 TermHomM 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.
termHom' :: (HDifunctor f, HDifunctor g, Monad m) => SigFunM m f g -> TermHomM m f g

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

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

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

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

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

-- | Compose two monadic term homomorphisms.
compTermHomM :: (HDitraversable g m Any, HDifunctor h, Monad m) => TermHomM m g h -> TermHomM m f g -> TermHomM 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 m a, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a

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


-- | This module defines the central notion of mutual recursive (or,
--   higher-order) <i>terms</i> and its generalisation to (higher-order)
--   contexts. All definitions are generalised versions of those in
--   <a>Data.Comp.Term</a>.
module Data.Comp.Multi.Term

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes. The first type parameter is
--   supposed to be one of the phantom types <a>Hole</a> and <a>NoHole</a>.
--   The second parameter is the signature of the context. The third
--   parameter is the type family of the holes. The last parameter is the
--   index/label.
data Cxt h f a i
Term :: f (Cxt h f a) i -> Cxt h f a i
Hole :: a i -> Cxt Hole f a i

-- | Phantom type that signals that a <a>Cxt</a> might contain holes.
data Hole

-- | Phantom type that signals that a <a>Cxt</a> does not contain holes.
data NoHole

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

-- | Phantom type family used to define <a>Term</a>.
data Nothing :: * -> *

-- | A (higher-order) term is a context with no holes.
type Term f = Cxt NoHole f Nothing
type Const f :: ((* -> *) -> * -> *) = f (K ())

-- | This function converts a constant to a term. This assumes that the
--   argument is indeed a constant, i.e. does not have a value for the
--   argument type of the functor f.
constTerm :: HFunctor f => Const f :-> Term f

-- | This function unravels the given term at the topmost layer.
unTerm :: Term f t -> f (Term f) t

-- | Cast a term over a signature to a context over the same signature.
toCxt :: HFunctor f => Term f :-> Context f a
simpCxt :: HFunctor f => f a i -> Context f a i
instance [incoherent] HTraversable f => HTraversable (Cxt h f)
instance [incoherent] HFoldable f => HFoldable (Cxt h f)
instance [incoherent] HFunctor f => HFunctor (Cxt h f)
instance [incoherent] Ord (Nothing i)
instance [incoherent] Eq (Nothing i)
instance [incoherent] Show (Nothing i)


-- | 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 Var a -> f Var 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 Var a -> f Var 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]

-- | Printing of parametric values.
class PShow a
pshow :: PShow a => a -> FreshM String

-- | Signature printing. An instance <tt>ShowD f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowD f
showD :: (ShowD f, PShow a) => f Var a -> 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, Monad m) => Ditraversable f m a

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

-- | Derive smart constructors for a type constructor of any parametric
--   kind taking at least two arguments. The smart constructors are similar
--   to the ordinary constructors, but an <a>inject</a> is automatically
--   inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with products for a type constructor of any
--   parametric kind taking at least two arguments. The smart constructors
--   are similar to the ordinary constructors, but an <a>injectA</a> 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]

-- | 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


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

-- | Printing of parametric values.
class PShow a
pshow :: PShow a => a -> FreshM String

-- | Signature printing. An instance <tt>ShowD f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowD f
showD :: (ShowD f, PShow a) => f Var a -> FreshM String
instance [incoherent] (ShowD f, PShow p) => ShowD (f :&: p)
instance [incoherent] (Difunctor f, ShowD f) => Show (Term f)
instance [incoherent] (ShowD f, PShow a) => PShow (Cxt h f Var a)
instance [incoherent] ShowD f => ShowD (Cxt h f)
instance [incoherent] (ShowD f, ShowD g) => ShowD (f :+: g)
instance [incoherent] Show a => PShow a


-- | 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 => TermHom 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 [overlap ok] (Difunctor f, Difunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g[aZw0], Desugar g g[aZw0]) => Desugar (f :+: g) g[aZw0]


-- | This module provides operators on functors.
module Data.Comp.Ops

-- | Formal sum of signatures (functors).
data (:+:) f g e
Inl :: (f e) -> :+: f g e
Inr :: (g e) -> :+: f g e

-- | 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 -> sup a
proj :: :<: sub sup => sup a -> Maybe (sub a)

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

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

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a -> s' a
projectA :: DistAnn s p s' => s' a -> (s a, p)
class RemA s s' | s -> s'
remA :: RemA s s' => s a -> s' a
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [incoherent] Traversable f => Traversable (f :&: a)
instance [incoherent] Foldable f => Foldable (f :&: a)
instance [incoherent] Functor f => Functor (f :&: a)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (Traversable f, Traversable g) => Traversable (f :+: g)
instance [incoherent] (Foldable f, Foldable g) => Foldable (f :+: g)
instance [incoherent] (Functor f, Functor g) => Functor (f :+: g)


-- | This module defines the notion of algebras and catamorphisms, and
--   their generalizations to e.g. monadic versions and other (co)recursion
--   schemes. All definitions are generalised versions of those in
--   <a>Data.Comp.Algebra</a>.
module Data.Comp.Multi.Algebra

-- | This type represents multisorted <tt>f</tt>-algebras with a family
--   <tt>e</tt> of carriers.
type Alg f e = f e :-> e

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

-- | Construct a catamorphism from the given algebra.
cata :: HFunctor 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' :: HFunctor f => Alg f e -> Cxt h f e :-> e

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

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

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

-- | This is a monadic version of <a>cata</a>.
cataM :: (HTraversable f, Monad m) => AlgM m f a -> NatM m (Term f) a
cataM' :: (Monad m, HTraversable f) => AlgM m f a -> NatM m (Cxt h f a) a

-- | This function lifts a many-sorted algebra to a monadic domain.
liftMAlg :: (Monad m, HTraversable f) => Alg f I -> Alg f m

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

-- | This type represents uniform signature function specification.
type SigFun f g = forall a. f a :-> g a

-- | This type represents term homomorphisms.
type TermHom f g = SigFun f (Context g)

-- | This function applies the given term homomorphism to a term/context.
appTermHom :: (HFunctor f, HFunctor g) => TermHom f g -> CxtFun f g

-- | This function applies the given term homomorphism to a term/context.
--   This is the top-down variant of <a>appTermHom</a>.
appTermHom' :: HFunctor g => TermHom f g -> CxtFun f g

-- | This function composes two term algebras.
compTermHom :: (HFunctor g, HFunctor h) => TermHom g h -> TermHom f g -> TermHom f h

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

-- | This function applies a signature function to the given context. This
--   is the top-down variant of <a>appSigFun</a>.
appSigFun' :: HFunctor 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.
termHom :: HFunctor g => SigFun f g -> TermHom f g

-- | This function composes a term algebra with an algebra.
compAlg :: HFunctor g => Alg g a -> TermHom f g -> Alg f a

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

-- | This type represents monadic signature functions.
type SigFunM m f g = forall a. NatM m (f a) (g a)

-- | This type represents monadic term algebras.
type TermHomM m f g = SigFunM m f (Context g)

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

-- | This function lifts the give monadic signature function to a monadic
--   term algebra.
termHom' :: (HFunctor f, HFunctor g, Monad m) => SigFunM m f g -> TermHomM m f g

-- | This function applies the given monadic term homomorphism to the given
--   term/context.
appTermHomM :: (HTraversable f, HFunctor g, Monad m) => TermHomM m f g -> CxtFunM m f g

-- | This function applies the given monadic term homomorphism to the given
--   term/context. This is a top-down variant of <a>appTermHomM</a>.
appTermHomM' :: (HTraversable g, Monad m) => TermHomM m f g -> CxtFunM m f g

-- | This function lifts the given signature function to a monadic term
--   algebra.
termHomM :: (HFunctor g, Monad m) => SigFun f g -> TermHomM m f g

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

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

-- | This function composes two monadic term algebras.
compTermHomM :: (HTraversable g, HFunctor h, Monad m) => TermHomM m g h -> TermHomM m f g -> TermHomM 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

-- | This function composes a monadic term algebra with a monadic algebra
compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a

-- | This function composes a monadic term algebra with a monadic algebra.
compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> TermHom f g -> AlgM m f a
type Coalg f a = a :-> f a

-- | This function unfolds the given value to a term using the given
--   unravelling function. This is the unique homomorphism <tt>a -&gt; Term
--   f</tt> from the given coalgebra of type <tt>a -&gt; f a</tt> to the
--   final coalgebra <tt>Term f</tt>.
ana :: HFunctor f => Coalg f a -> a :-> Term f
type CoalgM m f a = NatM m a (f a)

-- | This function unfolds the given value to a term using the given
--   monadic unravelling function. This is the unique homomorphism <tt>a
--   -&gt; Term f</tt> from the given coalgebra of type <tt>a -&gt; f
--   a</tt> to the final coalgebra <tt>Term f</tt>.
anaM :: (HTraversable f, Monad m) => CoalgM m f a -> NatM m a (Term f)

-- | This type represents r-algebras over functor <tt>f</tt> and with
--   domain <tt>a</tt>.
type RAlg f a = f (Term f :*: a) :-> a

-- | This function constructs a paramorphism from the given r-algebra
para :: HFunctor f => RAlg f a -> Term f :-> a

-- | This type represents monadic r-algebras over monad <tt>m</tt> and
--   functor <tt>f</tt> and with domain <tt>a</tt>.
type RAlgM m f a = NatM m (f (Term f :*: a)) a

-- | This function constructs a monadic paramorphism from the given monadic
--   r-algebra
paraM :: (HTraversable f, Monad m) => RAlgM m f a -> NatM m (Term f) a

-- | This type represents r-coalgebras over functor <tt>f</tt> and with
--   domain <tt>a</tt>.
type RCoalg f a = a :-> f (Term f :+: a)

-- | This function constructs an apomorphism from the given r-coalgebra.
apo :: HFunctor f => RCoalg f a -> a :-> Term f

-- | This type represents monadic r-coalgebras over monad <tt>m</tt> and
--   functor <tt>f</tt> with domain <tt>a</tt>.
type RCoalgM m f a = NatM m a (f (Term f :+: a))

-- | This function constructs a monadic apomorphism from the given monadic
--   r-coalgebra.
apoM :: (HTraversable f, Monad m) => RCoalgM m f a -> NatM m a (Term f)

-- | This type represents cv-coalgebras over functor <tt>f</tt> and with
--   domain <tt>a</tt>.
type CVCoalg f a = a :-> f (Context f a)

-- | This function constructs the unique futumorphism from the given
--   cv-coalgebra to the term algebra.
futu :: HFunctor f => CVCoalg f a -> a :-> Term f

-- | This type represents monadic cv-coalgebras over monad <tt>m</tt> and
--   functor <tt>f</tt>, and with domain <tt>a</tt>.
type CVCoalgM m f a = NatM m a (f (Context f a))

-- | This function constructs the unique monadic futumorphism from the
--   given monadic cv-coalgebra to the term algebra.
futuM :: (HTraversable f, Monad m) => CVCoalgM m f a -> NatM m a (Term f)


-- | This module provides operators on higher-order functors. All
--   definitions are generalised versions of those in <a>Data.Comp.Ops</a>.
module Data.Comp.Multi.Ops

-- | Data type defining coproducts.
data (:+:) f g h :: (* -> *) e
Inl :: (f h e) -> :+: f g e
Inr :: (g h e) -> :+: f g e

-- | The subsumption relation.
class :<: sub :: ((* -> *) -> * -> *) sup
inj :: :<: sub sup => sub a :-> sup a
proj :: :<: sub sup => NatM Maybe (sup a) (sub a)
data (:*:) f g a
(:*:) :: f a -> g a -> :*: f g a
fst :: (f :*: g) a -> f a
snd :: (f :*: g) a -> g a

-- | This data type adds a constant product to a signature. Alternatively,
--   this could have also been defined as
--   
--   <pre>
--   data (f :&amp;: a) (g ::  * -&gt; *) e = f g e :&amp;: a e
--   </pre>
--   
--   This is too general, however, for example for
--   <tt>productHTermHom</tt>.
data (:&:) f a g :: (* -> *) e
(:&:) :: f g e -> a -> :&: f a e

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s :: ((* -> *) -> * -> *) p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a :-> s' a
projectA :: DistAnn s p s' => s' a :-> (s a :&: p)
class RemA s :: ((* -> *) -> * -> *) s' | s -> s'
remA :: RemA s s' => s a :-> s' a
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [incoherent] HTraversable f => HTraversable (f :&: a)
instance [incoherent] HFoldable f => HFoldable (f :&: a)
instance [incoherent] HFunctor f => HFunctor (f :&: a)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (HTraversable f, HTraversable g) => HTraversable (f :+: g)
instance [incoherent] (HFoldable f, HFoldable g) => HFoldable (f :+: g)
instance [incoherent] (HFunctor f, HFunctor g) => HFunctor (f :+: g)


-- | This module defines sums on signatures. All definitions are
--   generalised versions of those in <a>Data.Comp.Sum</a>.
module Data.Comp.Multi.Sum

-- | The subsumption relation.
class :<: sub :: ((* -> *) -> * -> *) sup
inj :: :<: sub sup => sub a :-> sup a
proj :: :<: sub sup => NatM Maybe (sup a) (sub a)

-- | Data type defining coproducts.
data (:+:) f g h :: (* -> *) e
proj2 :: (:<: g1 f, :<: g2 f) => f a i -> Maybe (:+: g2 g1 a i)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a i -> Maybe (:+: g3 (:+: g2 g1) a i)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a i)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a i)
proj6 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 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) (g (Cxt h f a))
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a i -> Maybe (:+: g2 g1 (Cxt h f a) i)
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a i -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a) i)
project4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a) i)
project5 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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)

-- | 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 :: (HTraversable g, :<: g f) => CxtFunM Maybe f g
deepProject2 :: (HTraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => CxtFunM Maybe f (:+: g2 g1)
deepProject3 :: (HTraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
deepProject4 :: (HTraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
deepProject5 :: (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 :: (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 :: (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 :: (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 :: (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 :: (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)))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a i -> g a i
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a i -> g a i
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a i -> g a i
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a i -> g a i
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a i -> g a i
inj7 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 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 (Cxt h f a) :-> Cxt h f a
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 (Cxt h g a) i -> Cxt h g a i
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) (Cxt h g a) i -> Cxt h g a i
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) i -> Cxt h g a i
inject5 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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

-- | 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 :: (HFunctor g, :<: g f) => CxtFun g f
deepInject2 :: (HFunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (HFunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (HFunctor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (HFunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (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 :: (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 :: (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 :: (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 :: (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
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)

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

-- | This function lifts the given functor to a context.
liftCxt :: (HFunctor f, :<: g f) => g a :-> Context f a

-- | This function applies the given context with hole type <tt>a</tt> to a
--   family <tt>f</tt> of contexts (possibly terms) indexed by <tt>a</tt>.
--   That is, each hole <tt>h</tt> is replaced by the context <tt>f h</tt>.
substHoles :: (HFunctor f, HFunctor g, :<: f g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a


-- | This module defines annotations on signatures. All definitions are
--   generalised versions of those in <a>Data.Comp.Annotation</a>.
module Data.Comp.Multi.Annotation

-- | This data type adds a constant product to a signature. Alternatively,
--   this could have also been defined as
--   
--   <pre>
--   data (f :&amp;: a) (g ::  * -&gt; *) e = f g e :&amp;: a e
--   </pre>
--   
--   This is too general, however, for example for
--   <tt>productHTermHom</tt>.
data (:&:) f a g :: (* -> *) e
(:&:) :: f g e -> a -> :&: f a e

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

-- | This function transforms 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 :-> t) -> s a :-> t

-- | This function annotates each sub term of the given term with the given
--   value (of type a).
ann :: (DistAnn f p g, HFunctor f) => p -> CxtFun f g

-- | This function transforms 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, HFunctor s') => (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a

-- | This function strips the annotations from a term over a functor with
--   annotations.
stripA :: (RemA g f, HFunctor g) => CxtFun g f
propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g) => TermHom f g -> TermHom f' g'
project' :: (:<: s f, RemA s s') => Cxt h f a i -> Maybe (s' (Cxt h f a) i)


-- | This module defines type generic functions and recursive schemes along
--   the lines of the Uniplate library. All definitions are generalised
--   versions of those in <a>Data.Comp.Generic</a>.
module Data.Comp.Multi.Generic

-- | This function returns a list of all subterms of the given term. This
--   function is similar to Uniplate's <tt>universe</tt> function.
subterms :: HFoldable f => Term f :=> [A (Term f)]

-- | This function returns a list of all subterms of the given term that
--   are constructed from a particular functor.
subterms' :: (HFoldable f, :<: g f) => Term f :=> [A (g (Term f))]

-- | This function transforms every subterm according to the given function
--   in a bottom-up manner. This function is similar to Uniplate's
--   <tt>transform</tt> function.
transform :: HFunctor f => (Term f :-> Term f) -> Term f :-> Term f

-- | Monadic version of <a>transform</a>.
transformM :: (HTraversable f, Monad m) => NatM m (Term f) (Term f) -> NatM m (Term f) (Term f)
query :: HFoldable f => (Term f :=> r) -> (r -> r -> r) -> Term f :=> r
subs :: HFoldable f => Term f :=> [A (Term f)]
subs' :: (HFoldable f, :<: g f) => Term f :=> [A (g (Term f))]

-- | This function computes the generic size of the given term, i.e. the
--   its number of subterm occurrences.
size :: HFoldable f => Cxt h f a :=> Int

-- | This function computes the generic depth of the given term.
depth :: HFoldable f => Cxt h f a :=> Int


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>HFunctor</a>, <a>HFoldable</a>, and <a>HTraversable</a>.
module Data.Comp.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 printing. An instance <tt>HShowF f</tt> gives rise to an
--   instance <tt>KShow (HTerm f)</tt>.
class HShowF f
hshowF :: HShowF f => Alg f (K String)
hshowF' :: HShowF f => f (K String) :=> String
class KShow a
kshow :: KShow a => a i -> K String i

-- | Derive an instance of <a>HShowF</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
makeHShowF :: Name -> Q [Dec]

-- | Signature equality. An instance <tt>HEqF f</tt> gives rise to an
--   instance <tt>KEq (HTerm f)</tt>.
class HEqF f
heqF :: (HEqF f, KEq g) => f g i -> f g j -> Bool
class KEq f
keq :: KEq f => f i -> f j -> Bool

-- | Derive an instance of <a>HEqF</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
makeHEqF :: Name -> Q [Dec]

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

-- | Derive an instance of <a>HFunctor</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
makeHFunctor :: Name -> Q [Dec]

-- | Higher-order functors that can be folded.
--   
--   Minimal complete definition: <a>hfoldMap</a> or <a>hfoldr</a>.
class HFunctor h => HFoldable h

-- | Derive an instance of <a>HFoldable</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
makeHFoldable :: Name -> Q [Dec]
class HFoldable t => HTraversable t

-- | Derive an instance of <a>HTraversable</a> for a type constructor of
--   any higher-order kind taking at least two arguments.
makeHTraversable :: Name -> Q [Dec]

-- | Derive smart constructors for a type constructor of any higher-order
--   kind taking at least two arguments. The smart constructors are similar
--   to the ordinary constructors, but an <a>inject</a> is automatically
--   inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with products for a type constructor of any
--   parametric kind taking at least two arguments. The smart constructors
--   are similar to the ordinary constructors, but an <a>injectA</a> is
--   automatically inserted.
smartAConstructors :: Name -> Q [Dec]

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

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


-- | This module defines equality for (higher-order) signatures, which
--   lifts to equality for (higher-order) terms and contexts. All
--   definitions are generalised versions of those in
--   <a>Data.Comp.Equality</a>.
module Data.Comp.Multi.Equality

-- | Signature equality. An instance <tt>HEqF f</tt> gives rise to an
--   instance <tt>KEq (HTerm f)</tt>.
class HEqF f
heqF :: (HEqF f, KEq g) => f g i -> f g j -> Bool
class KEq f
keq :: KEq f => f i -> f j -> Bool

-- | This function implements equality of values of type <tt>f a</tt>
--   modulo the equality of <tt>a</tt> itself. If two functorial values are
--   equal in this sense, <tt>eqMod</tt> returns a <a>Just</a> value
--   containing a list of pairs consisting of corresponding components of
--   the two functorial values.
heqMod :: (HEqF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]
instance KEq Nothing
instance (HEqF f, KEq a) => KEq (Cxt h f a)
instance HEqF f => HEqF (Cxt h f)
instance (HEqF f, HEqF g) => HEqF (f :+: g)


-- | This module defines the infrastructure necessary to use <i>Generalised
--   Compositional Data Types</i>. Generalised Compositional Data Types is
--   an extension of Compositional Data Types with mutually recursive data
--   types, and more generally GADTs. Examples of usage are bundled with
--   the package in the library <tt>examples/Examples/Multi</tt>.
module Data.Comp.Multi


-- | This module defines showing of (higher-order) signatures, which lifts
--   to showing of (higher-order) terms and contexts. All definitions are
--   generalised versions of those in <a>Data.Comp.Show</a>.
module Data.Comp.Multi.Show

-- | Signature printing. An instance <tt>HShowF f</tt> gives rise to an
--   instance <tt>KShow (HTerm f)</tt>.
class HShowF f
hshowF :: HShowF f => Alg f (K String)
hshowF' :: HShowF f => f (K String) :=> String
instance (HShowF f, HShowF g) => HShowF (f :+: g)
instance (HShowF f, Show p) => HShowF (f :&: p)
instance KShow f => Show (f i)
instance (HShowF f, HFunctor f, KShow a) => KShow (Cxt h f a)
instance (HShowF f, HFunctor f) => HShowF (Cxt h f)
instance KShow (K String)
instance KShow Nothing


-- | This module defines an abstract notion of (bound) variables in
--   compositional data types, and scoped substitution. Capture-avoidance
--   is <i>not</i> taken into account. All definitions are generalised
--   versions of those in <a>Data.Comp.Variables</a>.
module Data.Comp.Multi.Variables

-- | This multiparameter class defines functors with variables. An instance
--   <tt>HasVar f v</tt> denotes that values over <tt>f</tt> might contain
--   and bind variables of type <tt>v</tt>.
class HasVars f :: ((* -> *) -> * -> *) v
isVar :: HasVars f v => f a :=> Maybe v
bindsVars :: HasVars f v => f a :=> [v]
type GSubst v a = NatM Maybe (K v) a
type CxtSubst h a f v = GSubst v (Cxt h f a)
type Subst f v = CxtSubst NoHole Nothing f v
varsToHoles :: (HFunctor f, HasVars f v, Eq v) => Term f :-> Context f (K v)

-- | This function checks whether a variable is contained in a context.
containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f) => v -> Cxt h f a :=> Bool

-- | This function computes the set of variables occurring in a context.
variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => Cxt h f a :=> Set v

-- | This function computes the list of variables occurring in a context.
variableList :: (HasVars f v, HFoldable f, HFunctor f, Eq v) => Cxt h f a :=> [v]

-- | This function computes the set of variables occurring in a context.
variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => Const f :=> Set v
substVars :: SubstVars v t a => GSubst v t -> a :-> a
appSubst :: SubstVars v t a => GSubst v t -> a :-> a

-- | This function composes two substitutions <tt>s1</tt> and <tt>s2</tt>.
--   That is, applying the resulting substitution is equivalent to first
--   applying <tt>s2</tt> and then <tt>s1</tt>.
compSubst :: (Ord v, HasVars f v, HFunctor f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
instance [overlap ok] (SubstVars v t a, HFunctor f) => SubstVars v t (f a)
instance [overlap ok] (Ord v, HasVars f v, HFunctor f) => SubstVars v (Cxt h f a) (Cxt h f a)
instance [overlap ok] HasVars f v => HasVars (Cxt h f) v
instance [overlap ok] (HasVars f v[a1ldN], HasVars g v[a1ldN]) => HasVars (f :+: g) v[a1ldN]


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

-- | The desugaring term homomorphism.
class (HFunctor f, HFunctor g) => Desugar f g
desugHom :: Desugar f g => TermHom f g
desugHom' :: Desugar f g => Alg f (Context g a)

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

-- | Lift desugaring to annotated terms.
desugarA :: (HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' :-> Term g'
instance [overlap ok] (HFunctor f, HFunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g[a1mbH], Desugar g g[a1mbH]) => Desugar (f :+: g) g[a1mbH]


-- | This module provides operators on higher-order difunctors.
module Data.Comp.MultiParam.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

-- | 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
(:*:) :: 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 :: (* -> *) 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
injectA :: DistAnn s p s' => p -> s a b :-> s' a b
projectA :: DistAnn s p s' => s' a b :-> (s a b :&: p)
class RemA s :: ((* -> *) -> (* -> *) -> * -> *) s' | s -> s'
remA :: RemA s s' => s a b :-> s' a b
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [incoherent] HDitraversable f m a => HDitraversable (f :&: p) m a
instance [incoherent] HDifunctor f => HDifunctor (f :&: p)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (HDitraversable f m a, HDitraversable g m a) => HDitraversable (f :+: g) m a
instance [incoherent] (HDifunctor f, HDifunctor g) => HDifunctor (f :+: g)


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.MultiParam.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
inj :: :<: sub sup => sub a b :-> sup a b
proj :: :<: sub sup => NatM Maybe (sup a b) (sub a b)

-- | Formal sum of signatures (difunctors).
data (:+:) f g a :: (* -> *) b :: (* -> *) i
proj2 :: (:<: g1 f, :<: g2 f) => f a b i -> Maybe (:+: g2 g1 a b i)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a b i -> Maybe (:+: g3 (:+: g2 g1) a b i)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a b i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b i)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a b i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b i)
proj6 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: g1 f, :<: g2 f) => Cxt h f a b i -> Maybe (:+: g2 g1 a (Cxt h f a b) i)
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a b i -> Maybe (:+: g3 (:+: g2 g1) a (Cxt h f a b) i)
project4 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 Maybe Any, :<: g f) => CxtFunM Maybe f g
deepProject2 :: (HDitraversable (:+: g2 g1) Maybe Any, :<: g1 f, :<: g2 f) => CxtFunM Maybe f (:+: g2 g1)
deepProject3 :: (HDitraversable (:+: g3 (:+: g2 g1)) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
deepProject4 :: (HDitraversable (:+: g4 (:+: g3 (:+: g2 g1))) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
deepProject5 :: (HDitraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))
deepProject6 :: (HDitraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) Maybe Any, :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
deepProject7 :: (HDitraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) Maybe Any, :<: 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 :: (HDitraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) Maybe Any, :<: 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 :: (HDitraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) Maybe Any, :<: 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 :: (HDitraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))) Maybe Any, :<: 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)))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a b i -> g a b i
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a b i -> g a b i
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a b i -> g a b i
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b i -> g a b i
inj6 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) i -> Cxt h g a b i
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a (Cxt h g a b) i -> Cxt h g a b i
inject4 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (:<: 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 :: (HDifunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (HDifunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (HDifunctor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (HDifunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (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 :: (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 :: (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 :: (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 :: (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
injectConst :: (HDifunctor g, :<: g f) => Const g :-> Cxt h f Any a
injectConst2 :: (HDifunctor f1, HDifunctor f2, HDifunctor g, :<: f1 g, :<: f2 g) => Const (f1 :+: f2) :-> Cxt h g Any a
injectConst3 :: (HDifunctor f1, HDifunctor f2, HDifunctor f3, HDifunctor g, :<: f1 g, :<: f2 g, :<: f3 g) => Const (f1 :+: (f2 :+: f3)) :-> Cxt h g Any a
projectConst :: (HDifunctor g, :<: g f) => NatM Maybe (Cxt h f Any a) (Const 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 [incoherent] (Eq (f a b i), Eq (g a b i)) => Eq ((:+:) f g a b i)
instance [incoherent] (Ord (f a b i), Ord (g a b i)) => Ord ((:+:) f g a b i)
instance [incoherent] (Show (f a b i), Show (g a b i)) => Show ((:+:) f g a b i)


-- | This module defines annotations on signatures.
module Data.Comp.MultiParam.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
(:*:) :: 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
injectA :: DistAnn s p s' => p -> s a b :-> s' a b
projectA :: DistAnn s p s' => s' a b :-> (s a b :&: p)
class RemA s :: ((* -> *) -> (* -> *) -> * -> *) s' | s -> s'
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) => TermHom f g -> TermHom 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) => TermHomM m f g -> TermHomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, HDifunctor f) => p -> CxtFun f g
project' :: (:<: s f, RemA s s') => Cxt h f a b i -> Maybe (s' a (Cxt h f a b) i)


-- | This module defines equality for signatures, which lifts to equality
--   for terms.
module Data.Comp.MultiParam.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 Var a i -> f Var a j -> FreshM Bool
instance [incoherent] (HDifunctor f, EqHD f) => Eq (Term f i)
instance [incoherent] (EqHD f, PEq a) => PEq (Cxt h f Var a)
instance [incoherent] EqHD f => EqHD (Cxt h f)
instance [incoherent] PEq Var
instance [incoherent] (EqHD f, EqHD g) => EqHD (f :+: g)
instance [incoherent] Eq a => PEq (K a)


-- | 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/MultiParam</tt>.
module Data.Comp.MultiParam


-- | This module defines ordering of signatures, which lifts to ordering of
--   terms and contexts.
module Data.Comp.MultiParam.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 Var a i -> f Var a j -> FreshM Ordering
instance [incoherent] (HDifunctor f, OrdHD f) => Ord (Term f i)
instance [incoherent] (OrdHD f, POrd a) => POrd (Cxt h f Var a)
instance [incoherent] POrd Var
instance [incoherent] OrdHD f => OrdHD (Cxt h f)
instance [incoherent] (OrdHD f, OrdHD g) => OrdHD (f :+: g)
instance [incoherent] Ord a => POrd (K a)


-- | 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.MultiParam.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 Var a i -> f Var 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 Var a i -> f Var 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]

-- | Printing of parametric values.
class PShow a
pshow :: PShow a => a i -> FreshM String

-- | 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, PShow a) => f Var a 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]

-- | Higher-order functors that can be folded.
--   
--   Minimal complete definition: <a>hfoldMap</a> or <a>hfoldr</a>.
class HFunctor h => HFoldable h

-- | Derive an instance of <a>HFoldable</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
makeHFoldable :: Name -> Q [Dec]
class HFoldable t => HTraversable t

-- | Derive an instance of <a>HTraversable</a> for a type constructor of
--   any higher-order kind taking at least two arguments.
makeHTraversable :: Name -> Q [Dec]

-- | Derive smart constructors for a type constructor of any parametric
--   kind taking at least three arguments. The smart constructors are
--   similar to the ordinary constructors, but an <a>inject</a> is
--   automatically inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with products for a type constructor of any
--   parametric kind taking at least three arguments. The smart
--   constructors are similar to the ordinary constructors, but an
--   <a>injectA</a> 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]

-- | 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


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

-- | Printing of parametric values.
class PShow a
pshow :: PShow a => a i -> FreshM String

-- | 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, PShow a) => f Var a i -> FreshM String
instance [incoherent] (ShowHD f, PShow (K p)) => ShowHD (f :&: p)
instance [incoherent] (HDifunctor f, ShowHD f) => Show (Term f i)
instance [incoherent] (ShowHD f, PShow a) => PShow (Cxt h f Var a)
instance [incoherent] PShow Var
instance [incoherent] (ShowHD f, ShowHD g) => ShowHD (f :+: g)
instance [incoherent] Show a => PShow (K a)


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

-- | The desugaring term homomorphism.
class (HDifunctor f, HDifunctor g) => Desugar f g
desugHom :: Desugar f g => TermHom 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 [overlap ok] (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g[a1EGf], Desugar g g[a1EGf]) => Desugar (f :+: g) g[a1EGf]


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

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes. The first type parameter is
--   supposed to be one of the phantom types <a>Hole</a> and <a>NoHole</a>.
--   The second parameter is the signature of the context. The third
--   parameter is the type of the holes.
data Cxt :: * -> (* -> *) -> * -> *
Term :: f (Cxt h f a) -> Cxt h f a
Hole :: a -> Cxt Hole f a

-- | Phantom type that signals that a <a>Cxt</a> might contain holes.
data Hole

-- | Phantom type that signals that a <a>Cxt</a> does not contain holes.
data NoHole
type Context = Cxt Hole

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

-- | A term is a context with no holes.
type Term f = Cxt NoHole f Nothing

-- | Polymorphic definition of a term. This formulation is more natural
--   than <a>Term</a>, it leads to impredicative types in some cases,
--   though.
type PTerm f = forall h a. Cxt h f a
type Const f = f ()

-- | This function unravels the given term at the topmost layer.
unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)

-- | Convert a functorial value into a context.
simpCxt :: Functor f => f a -> Context f a

-- | Cast a term over a signature to a context over the same signature.
toCxt :: Functor f => Term f -> Cxt h f a

-- | This function converts a constant to a term. This assumes that the
--   argument is indeed a constant, i.e. does not have a value for the
--   argument type of the functor <tt>f</tt>.
constTerm :: Functor f => Const f -> Term f
instance Traversable f => Traversable (Cxt h f)
instance Foldable f => Foldable (Cxt h f)
instance Functor f => Functor (Cxt h f)
instance Show Nothing
instance Ord Nothing
instance Eq Nothing


-- | 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.Algebra

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

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

-- | Construct a catamorphism from the given algebra.
cata :: Functor 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' :: Functor f => Alg f a -> Cxt h f a -> a

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

-- | 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 -> m a

-- | Convert a monadic algebra into an ordinary algebra with a monadic
--   carrier.
algM :: (Traversable 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>a</tt>, from the given monadic algebra.
freeM :: (Traversable f, Monad m) => AlgM m f b -> (a -> m b) -> Cxt h f a -> m b

-- | Construct a monadic catamorphism from the given monadic algebra.
cataM :: (Traversable 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' :: (Traversable f, Monad m) => AlgM m f a -> Cxt h f a -> m a

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

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

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

-- | This function applies the given term homomorphism to a term/context.
appTermHom :: (Functor f, Functor g) => TermHom f g -> CxtFun f g

-- | Apply a term homomorphism recursively to a term/context. This is a
--   top-down variant of <a>appTermHom</a>.
appTermHom' :: Functor g => TermHom f g -> CxtFun f g

-- | Compose two term homomorphisms.
compTermHom :: (Functor g, Functor h) => TermHom g h -> TermHom f g -> TermHom f h

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

-- | This function applies a signature function to the given context. This
--   is a top-down variant of <a>appSigFun</a>.
appSigFun' :: Functor 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 signature function with a term homomorphism.
compSigFunTermHom :: Functor g => SigFun g h -> TermHom f g -> TermHom f h

-- | This function composes a term homomorphism with a signature function.
compTermHomSigFun :: TermHom g h -> SigFun f g -> TermHom f h

-- | This function composes an algebra with a signature function.
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a

-- | Lifts the given signature function to the canonical term homomorphism.
termHom :: Functor g => SigFun f g -> TermHom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: Functor g => Alg g a -> TermHom f g -> Alg f a

-- | Compose a term homomorphism with a coalgebra to get a cv-coalgebra.
compCoalg :: TermHom f g -> Coalg f a -> CVCoalg' g a

-- | Compose a term homomorphism with a cv-coalgebra to get a new
--   cv-coalgebra.
compCVCoalg :: (Functor f, Functor g) => TermHom f g -> CVCoalg' f a -> CVCoalg' g a

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

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

-- | This type represents a monadic term homomorphism.
type TermHomM 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. f (m a) -> m (g a)

-- | This type represents a monadic term homomorphism. It is similar to
--   <a>TermHomM</a> but has monadic values also in the domain.
type TermHomMD 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

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

-- | Apply a monadic term homomorphism recursively to a term/context.
appTermHomM :: (Traversable f, Functor g, Monad m) => TermHomM m f g -> CxtFunM m f g

-- | Apply a monadic term homomorphism recursively to a term/context. This
--   a top-down variant of <a>appTermHomM</a>.
appTermHomM' :: (Traversable g, Monad m) => TermHomM m f g -> CxtFunM m f g

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

-- | This function constructs the unique monadic homomorphism from the
--   initial term algebra to the given term algebra.
termHomMD :: (Traversable f, Functor g, Monad m) => TermHomMD m f g -> CxtFunM m f g

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

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

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

-- | Compose two monadic term homomorphisms.
compTermHomM :: (Traversable g, Functor h, Monad m) => TermHomM m g h -> TermHomM m f g -> TermHomM 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
compSigFunTermHomM :: (Traversable g, Functor h, Monad m) => SigFunM m g h -> TermHomM m f g -> TermHomM m f h

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

-- | This function composes two monadic signature functions.
compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a

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

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

-- | This type represents a coalgebra over a functor <tt>f</tt> and carrier
--   <tt>a</tt>.
type Coalg f a = a -> f a

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

-- | Shortcut fusion variant of <a>ana</a>.
ana' :: Functor f => Coalg f a -> a -> Term f

-- | This type represents a monadic coalgebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type CoalgM m f a = a -> m (f a)

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

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

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

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

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

-- | This type represents an r-coalgebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RCoalg f a = a -> f (Either (Term f) a)

-- | Construct an apomorphism from the given r-coalgebra.
apo :: Functor 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 = a -> m (f (Either (Term f) a))

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

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

-- | Construct a histomorphism from the given cv-algebra.
histo :: (Functor 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 (Term f') -> m a

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

-- | This type represents a cv-coalgebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type CVCoalg f a = a -> f (Context f a)

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

-- | This type represents a generalised cv-coalgebra over a functor
--   <tt>f</tt> and carrier <tt>a</tt>.
type CVCoalg' f a = a -> Context f a

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

-- | This type represents a monadic cv-coalgebra over a functor <tt>f</tt>
--   and carrier <tt>a</tt>.
type CVCoalgM m f a = a -> m (f (Context f a))

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


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.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
inj :: :<: sub sup => sub a -> sup a
proj :: :<: sub sup => sup a -> Maybe (sub a)

-- | Formal sum of signatures (functors).
data (:+:) f g e
proj2 :: (:<: g1 f, :<: g2 f) => f a -> Maybe (:+: g2 g1 a)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a -> Maybe (:+: g3 (:+: g2 g1) a)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a)
proj6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a)
proj7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a)
proj8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a)
proj9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a)
proj10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a)

-- | 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 -> Maybe (g (Cxt h f a))
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a -> Maybe (:+: g2 g1 (Cxt h f a))
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a))
project4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a))
project5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) (Cxt h f a))
project6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) (Cxt h f a))
project7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Cxt h f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) (Cxt h f a))
project8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Cxt h f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) (Cxt h f a))
project9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Cxt h f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) (Cxt h f a))
project10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Cxt h f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) (Cxt h f a))

-- | 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 :: (Traversable g, :<: g f) => CxtFunM Maybe f g
deepProject2 :: (Traversable (:+: g2 g1), :<: g1 f, :<: g2 f) => CxtFunM Maybe f (:+: g2 g1)
deepProject3 :: (Traversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
deepProject4 :: (Traversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
deepProject5 :: (Traversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))
deepProject6 :: (Traversable (:+: 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 :: (Traversable (:+: 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 :: (Traversable (:+: 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 :: (Traversable (:+: 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 :: (Traversable (:+: 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)))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a -> g a
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a -> g a
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a -> g a
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a -> g a
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a -> g a
inj7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a -> g a
inj8 :: (:<: 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 -> g a
inj9 :: (:<: 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 -> g a
inj10 :: (:<: 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 -> g a

-- | 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 (Cxt h f a) -> Cxt h f a
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 (Cxt h g a) -> Cxt h g a
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) (Cxt h g a) -> Cxt h g a
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) -> Cxt h g a
inject5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) (Cxt h g a) -> Cxt h g a
inject6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) (Cxt h g a) -> Cxt h g a
inject7 :: (:<: 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) -> Cxt h g a
inject8 :: (:<: 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) -> Cxt h g a
inject9 :: (:<: 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) -> Cxt h g a
inject10 :: (:<: 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) -> Cxt h g a

-- | 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 :: (Functor g, :<: g f) => CxtFun g f
deepInject2 :: (Functor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (Functor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (Functor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (Functor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (Functor (:+: 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 :: (Functor (:+: 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 :: (Functor (:+: 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 :: (Functor (:+: 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 :: (Functor (:+: 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
injectConst :: (Functor g, :<: g f) => Const g -> Cxt h f a
injectConst2 :: (Functor f1, Functor f2, Functor g, :<: f1 g, :<: f2 g) => Const (f1 :+: f2) -> Cxt h g a
injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, :<: f1 g, :<: f2 g, :<: f3 g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g a
projectConst :: (Functor g, :<: g f) => Cxt h f a -> Maybe (Const g)

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

-- | This function lifts the given functor to a context.
liftCxt :: (Functor f, :<: g f) => g a -> Context f a

-- | This function applies the given context with hole type <tt>a</tt> to a
--   family <tt>f</tt> of contexts (possibly terms) indexed by <tt>a</tt>.
--   That is, each hole <tt>h</tt> is replaced by the context <tt>f h</tt>.
substHoles :: (Functor f, Functor g, :<: f g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles' :: (Functor f, Functor g, :<: f g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
instance [incoherent] (Eq (f a), Eq (g a)) => Eq ((:+:) f g a)
instance [incoherent] (Ord (f a), Ord (g a)) => Ord ((:+:) f g a)
instance [incoherent] (Show (f a), Show (g a)) => Show ((:+:) f g a)
instance [incoherent] Functor f => Monad (Context f)


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

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

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

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

-- | 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 -> t) -> s a -> 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, Functor s') => (s' a -> Cxt h s' a) -> s a -> Cxt h s a

-- | Strip the annotations from a term over a functor with annotations.
stripA :: (RemA g f, Functor 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', Functor g) => TermHom f g -> TermHom 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', Functor g, Monad m) => TermHomM m f g -> TermHomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, Functor f) => p -> CxtFun f g
project' :: (:<: s f, RemA s s') => Cxt h f a -> Maybe (s' (Cxt h f a))


-- | This module defines type generic functions and recursive schemes along
--   the lines of the Uniplate library.
module Data.Comp.Generic

-- | This function returns a list of all subterms of the given term. This
--   function is similar to Uniplate's <tt>universe</tt> function.
subterms :: Foldable f => Term f -> [Term f]

-- | This function returns a list of all subterms of the given term that
--   are constructed from a particular functor.
subterms' :: (Foldable f, :<: g f) => Term f -> [g (Term f)]

-- | This function transforms every subterm according to the given function
--   in a bottom-up manner. This function is similar to Uniplate's
--   <tt>transform</tt> function.
transform :: Functor f => (Term f -> Term f) -> Term f -> Term f
transform' :: Functor f => (Term f -> Maybe (Term f)) -> Term f -> Term f

-- | Monadic version of <a>transform</a>.
transformM :: (Traversable f, Monad m) => (Term f -> m (Term f)) -> Term f -> m (Term f)
query :: Foldable f => (Term f -> r) -> (r -> r -> r) -> Term f -> r
gsize :: Foldable f => Term f -> Int

-- | This function computes the generic size of the given term, i.e. the
--   its number of subterm occurrences.
size :: Foldable f => Cxt h f a -> Int

-- | This function computes the generic depth of the given term.
depth :: Foldable f => Cxt h f a -> Int


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>Functor</a>, <a>Foldable</a>, and <a>Traversable</a>.
module Data.Comp.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 printing. An instance <tt>ShowF f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowF f
showF :: ShowF f => f String -> String

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

-- | Signature equality. An instance <tt>EqF f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>.
class EqF f
eqF :: (EqF f, Eq a) => f a -> f a -> Bool

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

-- | Signature ordering. An instance <tt>OrdF f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqF f => OrdF f
compareF :: (OrdF f, Ord a) => f a -> f a -> Ordering

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

-- | The <a>Functor</a> class is used for types that can be mapped over.
--   Instances of <a>Functor</a> should satisfy the following laws:
--   
--   <pre>
--   fmap id  ==  id
--   fmap (f . g)  ==  fmap f . fmap g
--   </pre>
--   
--   The instances of <a>Functor</a> for lists, <tt>Data.Maybe.Maybe</tt>
--   and <tt>System.IO.IO</tt> satisfy these laws.
class Functor f :: (* -> *)

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

-- | Data structures that can be folded.
--   
--   Minimal complete definition: <a>foldMap</a> or <a>foldr</a>.
--   
--   For example, given a data type
--   
--   <pre>
--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--   </pre>
--   
--   a suitable instance would be
--   
--   <pre>
--   instance Foldable Tree where
--      foldMap f Empty = mempty
--      foldMap f (Leaf x) = f x
--      foldMap f (Node l k r) = foldMap f l `mappend` f k `mappend` foldMap f r
--   </pre>
--   
--   This is suitable even for abstract types, as the monoid is assumed to
--   satisfy the monoid laws. Alternatively, one could define
--   <tt>foldr</tt>:
--   
--   <pre>
--   instance Foldable Tree where
--      foldr f z Empty = z
--      foldr f z (Leaf x) = f x z
--      foldr f z (Node l k r) = foldr f (f k (foldr f z r)) l
--   </pre>
class Foldable t :: (* -> *)

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

-- | Functors representing data structures that can be traversed from left
--   to right.
--   
--   Minimal complete definition: <a>traverse</a> or <a>sequenceA</a>.
--   
--   Instances are similar to <a>Functor</a>, e.g. given a data type
--   
--   <pre>
--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--   </pre>
--   
--   a suitable instance would be
--   
--   <pre>
--   instance Traversable Tree where
--      traverse f Empty = pure Empty
--      traverse f (Leaf x) = Leaf &lt;$&gt; f x
--      traverse f (Node l k r) = Node &lt;$&gt; traverse f l &lt;*&gt; f k &lt;*&gt; traverse f r
--   </pre>
--   
--   This is suitable even for abstract types, as the laws for
--   <a>&lt;*&gt;</a> imply a form of associativity.
--   
--   The superclass instances should satisfy the following:
--   
--   <ul>
--   <li>In the <a>Functor</a> instance, <a>fmap</a> should be equivalent
--   to traversal with the identity applicative functor
--   (<a>fmapDefault</a>).</li>
--   <li>In the <a>Foldable</a> instance, <tt>Data.Foldable.foldMap</tt>
--   should be equivalent to traversal with a constant applicative functor
--   (<a>foldMapDefault</a>).</li>
--   </ul>
class (Functor t, Foldable t) => Traversable t :: (* -> *)

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

-- | Signature arbitration. An instance <tt>ArbitraryF f</tt> gives rise to
--   an instance <tt>Arbitrary (Term f)</tt>.
class ArbitraryF f
arbitraryF' :: (ArbitraryF f, Arbitrary v) => [(Int, Gen (f v))]
arbitraryF :: (ArbitraryF f, Arbitrary v) => Gen (f v)
shrinkF :: (ArbitraryF f, Arbitrary v) => f v -> [f v]

-- | Derive an instance of <a>ArbitraryF</a> for a type constructor of any
--   first-order kind taking at least one argument. It is necessary that
--   all types that are used by the data type definition are themselves
--   instances of <a>Arbitrary</a>.
makeArbitraryF :: Name -> Q [Dec]

-- | Random generation and shrinking of values.
class Arbitrary a
arbitrary :: Arbitrary a => Gen a
shrink :: Arbitrary a => a -> [a]

-- | Derive an instance of <a>Arbitrary</a> for a type constructor.
makeArbitrary :: Name -> Q [Dec]

-- | A class of types that can be fully evaluated.
class NFData a
rnf :: NFData a => a -> ()

-- | Derive an instance of <a>NFData</a> for a type constructor.
makeNFData :: Name -> Q [Dec]

-- | Signature normal form. An instance <tt>NFDataF f</tt> gives rise to an
--   instance <tt>NFData (Term f)</tt>.
class NFDataF f
rnfF :: (NFDataF f, NFData a) => f a -> ()

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

-- | Derive smart constructors for a type constructor of any first-order
--   kind taking at least one argument. The smart constructors are similar
--   to the ordinary constructors, but an <a>inject</a> is automatically
--   inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with products for a type constructor of any
--   parametric kind taking at least one argument. The smart constructors
--   are similar to the ordinary constructors, but an <a>injectA</a> is
--   automatically inserted.
smartAConstructors :: Name -> Q [Dec]

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

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


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

-- | Signature equality. An instance <tt>EqF f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>.
class EqF f
eqF :: (EqF f, Eq a) => f a -> f a -> Bool

-- | This function implements equality of values of type <tt>f a</tt>
--   modulo the equality of <tt>a</tt> itself. If two functorial values are
--   equal in this sense, <a>eqMod</a> returns a <a>Just</a> value
--   containing a list of pairs consisting of corresponding components of
--   the two functorial values.
eqMod :: (EqF f, Functor f, Foldable f) => f a -> f b -> Maybe [(a, b)]
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18], Eq h[19], Eq i[1a]) => EqF ((,,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18], Eq h[19]) => EqF ((,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18]) => EqF ((,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17]) => EqF ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16]) => EqF ((,,,,,) a[12] b[13] c[14] d[15] e[16])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15]) => EqF ((,,,,) a[12] b[13] c[14] d[15])
instance (Eq a[12], Eq b[13], Eq c[14]) => EqF ((,,,) a[12] b[13] c[14])
instance (Eq a[12], Eq b[13]) => EqF ((,,) a[12] b[13])
instance Eq a[12] => EqF ((,) a[12])
instance EqF Maybe
instance EqF []
instance (EqF f, Eq a) => Eq (Cxt h f a)
instance EqF f => EqF (Cxt h f)
instance (EqF f, EqF g) => EqF (f :+: g)


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

-- | Signature ordering. An instance <tt>OrdF f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqF f => OrdF f
compareF :: (OrdF f, Ord a) => f a -> f a -> Ordering
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18], Ord h[19], Ord i[1a]) => OrdF ((,,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18], Ord h[19]) => OrdF ((,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18]) => OrdF ((,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17]) => OrdF ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16]) => OrdF ((,,,,,) a[12] b[13] c[14] d[15] e[16])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15]) => OrdF ((,,,,) a[12] b[13] c[14] d[15])
instance (Ord a[12], Ord b[13], Ord c[14]) => OrdF ((,,,) a[12] b[13] c[14])
instance (Ord a[12], Ord b[13]) => OrdF ((,,) a[12] b[13])
instance Ord a[12] => OrdF ((,) a[12])
instance OrdF []
instance OrdF Maybe
instance (OrdF f, OrdF g) => OrdF (f :+: g)
instance OrdF f => OrdF (Cxt h f)
instance (OrdF f, Ord a) => Ord (Cxt h f a)


-- | This module defines full evaluation of signatures, which lifts to full
--   evaluation of terms and contexts.
module Data.Comp.DeepSeq

-- | Signature normal form. An instance <tt>NFDataF f</tt> gives rise to an
--   instance <tt>NFData (Term f)</tt>.
class NFDataF f
rnfF :: (NFDataF f, NFData a) => f a -> ()

-- | Fully evaluate a value over a foldable signature.
rnfF' :: (Foldable f, NFDataF f, NFData a) => f a -> ()
instance NFData a[12] => NFDataF ((,) a[12])
instance NFDataF []
instance NFDataF Maybe
instance (NFDataF f, NFDataF g) => NFDataF (f :+: g)
instance NFData Nothing
instance (NFDataF f, NFData a) => NFData (Cxt h f a)


-- | This module defines generation of arbitrary values for signatures,
--   which lifts to generating arbitrary terms.
module Data.Comp.Arbitrary

-- | Signature arbitration. An instance <tt>ArbitraryF f</tt> gives rise to
--   an instance <tt>Arbitrary (Term f)</tt>.
class ArbitraryF f
arbitraryF' :: (ArbitraryF f, Arbitrary v) => [(Int, Gen (f v))]
arbitraryF :: (ArbitraryF f, Arbitrary v) => Gen (f v)
shrinkF :: (ArbitraryF f, Arbitrary v) => f v -> [f v]
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18], Arbitrary h[19], Arbitrary i[1a], Arbitrary j[1b]) => ArbitraryF ((,,,,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a] j[1b])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18], Arbitrary h[19], Arbitrary i[1a]) => ArbitraryF ((,,,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18], Arbitrary h[19]) => ArbitraryF ((,,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18] h[19])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18]) => ArbitraryF ((,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17]) => ArbitraryF ((,,,,,) b[13] c[14] d[15] e[16] f[17])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16]) => ArbitraryF ((,,,,) b[13] c[14] d[15] e[16])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15]) => ArbitraryF ((,,,) b[13] c[14] d[15])
instance (Arbitrary b[13], Arbitrary c[14]) => ArbitraryF ((,,) b[13] c[14])
instance Arbitrary b[13] => ArbitraryF ((,) b[13])
instance ArbitraryF []
instance ArbitraryF Maybe
instance (ArbitraryF f, ArbitraryF g) => ArbitraryF (f :+: g)
instance (ArbitraryF f, Arbitrary a) => Arbitrary (Context f a)
instance ArbitraryF f => ArbitraryF (Context f)
instance (ArbitraryF f, Arbitrary p) => ArbitraryF (f :&: p)
instance ArbitraryF f => Arbitrary (Term f)


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

-- | Signature printing. An instance <tt>ShowF f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowF f
showF :: ShowF f => f String -> String
instance Show a[12] => ShowF ((,) a[12])
instance ShowF []
instance ShowF Maybe
instance (ShowF f, ShowF g) => ShowF (f :+: g)
instance (ShowF f, Show p) => ShowF (f :&: p)
instance (Functor f, ShowF f, Show a) => Show (Cxt h f a)
instance (Functor f, ShowF f) => ShowF (Cxt h f)


-- | This module defines an abstract notion of (bound) variables in
--   compositional data types, and scoped substitution. Capture-avoidance
--   is <i>not</i> taken into account.
module Data.Comp.Variables

-- | This multiparameter class defines functors with variables. An instance
--   <tt>HasVar f v</tt> denotes that values over <tt>f</tt> might contain
--   and bind variables of type <tt>v</tt>.
class HasVars f v
isVar :: HasVars f v => f a -> Maybe v
bindsVars :: HasVars f v => f a -> [v]
type Subst f v = CxtSubst NoHole Nothing f v
type CxtSubst h a f v = Map v (Cxt h f a)

-- | Convert variables to holes, except those that are bound.
varsToHoles :: (Functor f, HasVars f v, Eq v) => Term f -> Context f v

-- | This function checks whether a variable is contained in a context.
containsVar :: (Eq v, HasVars f v, Foldable f, Functor f) => v -> Cxt h f a -> Bool

-- | This function computes the set of variables occurring in a context.
variables :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> Set v

-- | This function computes the list of variables occurring in a context.
variableList :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> [v]

-- | This function computes the set of variables occurring in a constant.
variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v
substVars :: SubstVars v t a => (v -> Maybe t) -> a -> a

-- | Apply the given substitution.
appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a

-- | This function composes two substitutions <tt>s1</tt> and <tt>s2</tt>.
--   That is, applying the resulting substitution is equivalent to first
--   applying <tt>s2</tt> and then <tt>s1</tt>.
compSubst :: (Ord v, HasVars f v, Functor f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
instance [overlap ok] (SubstVars v t a, Functor f) => SubstVars v t (f a)
instance [overlap ok] (Ord v, HasVars f v, Functor f) => SubstVars v (Cxt h f a) (Cxt h f a)
instance [overlap ok] HasVars f v => HasVars (Cxt h f) v
instance [overlap ok] (HasVars f v[a27mn], HasVars g v[a27mn]) => HasVars (f :+: g) v[a27mn]


-- | This module implements matching of contexts or terms with variables
--   againts terms
module Data.Comp.Matching

-- | This function takes a context <tt>c</tt> as the first argument and
--   tries to match it against the term <tt>t</tt> (or in general a context
--   with holes in <tt>a</tt>). The context <tt>c</tt> matches the term
--   <tt>t</tt> if there is a <i>matching substitution</i> <tt>s</tt> that
--   maps holes to terms (resp. contexts in general) such that if the holes
--   in the context <tt>c</tt> are replaced according to the substitution
--   <tt>s</tt>, the term <tt>t</tt> is obtained. Note that the context
--   <tt>c</tt> might be non-linear, i.e. has multiple holes that are
--   equal. According to the above definition this means that holes with
--   equal holes have to be instantiated by equal terms!
matchCxt :: (Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f) => Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)

-- | This function is similar to <a>matchCxt</a> but instead of a context
--   it matches a term with variables against a context.
matchTerm :: (Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f, HasVars f v) => Term f -> Cxt h f a -> Maybe (CxtSubst h a f v)


-- | This module defines term rewriting systems (TRSs) using compositional
--   data types.
module Data.Comp.TermRewriting

-- | This type represents <i>recursive program schemes</i>.
type RPS f g = TermHom f g
type Var = Int

-- | This type represents term rewrite rules from signature <tt>f</tt> to
--   signature <tt>g</tt> over variables of type <tt>v</tt>
type Rule f g v = (Context f v, Context g v)

-- | This type represents term rewriting systems (TRSs) from signature
--   <tt>f</tt> to signature <tt>g</tt> over variables of type <tt>v</tt>.
type TRS f g v = [Rule f g v]
type Step t = t -> Maybe t
type BStep t = t -> (t, Bool)

-- | This function tries to match the given rule against the given term
--   (resp. context in general) at the root. If successful, the function
--   returns the right hand side of the rule and the matching substitution.
matchRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRules :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))

-- | This function tries to apply the given rule at the root of the given
--   term (resp. context in general). If successful, the function returns
--   the result term of the rewrite step; otherwise <tt>Nothing</tt>.
appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f f v -> Step (Cxt h f a)

-- | This function tries to apply one of the rules in the given TRS at the
--   root of the given term (resp. context in general) by trying each rule
--   one by one using <a>appRule</a> until one rule is applicable. If no
--   rule is applicable <tt>Nothing</tt> is returned.
appTRS :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f f v -> Step (Cxt h f a)

-- | This is an auxiliary function that turns function <tt>f</tt> of type
--   <tt>(t -&gt; Maybe t)</tt> into functions <tt>f'</tt> of type <tt>t
--   -&gt; (t,Bool)</tt>. <tt>f' x</tt> evaluates to <tt>(y,True)</tt> if
--   <tt>f x</tt> evaluates to <tt>Just y</tt>, and to <tt>(x,False)</tt>
--   if <tt>f x</tt> evaluates to <tt>Nothing</tt>. This function is useful
--   to change the output of functions that apply rules such as
--   <a>appTRS</a>.
bStep :: Step t -> BStep t

-- | This function performs a parallel reduction step by trying to apply
--   rules of the given system to all outermost redexes. If the given term
--   contains no redexes, <tt>Nothing</tt> is returned.
parTopStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)

-- | This function performs a parallel reduction step by trying to apply
--   rules of the given system to all outermost redexes and then
--   recursively in the variable positions of the redexes. If the given
--   term does not contain any redexes, <tt>Nothing</tt> is returned.
parallelStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)

-- | This function applies the given reduction step repeatedly until a
--   normal form is reached.
reduce :: Step t -> t -> t


-- | This module implements the decomposition of terms into function
--   symbols and arguments resp. variables.
module Data.Comp.Decompose

-- | This type represents decompositions of functorial values.
data Decomp f v a
Var :: v -> Decomp f v a
Fun :: (Const f) -> [a] -> Decomp f v a

-- | This type represents decompositions of terms.
type DecompTerm f v = Decomp f v (Term f)

-- | This class specifies the decomposability of a functorial value.
class (HasVars f v, Functor f, Foldable f) => Decompose f v
decomp :: Decompose f v => f a -> Decomp f v a

-- | This function computes the structure of a functorial value.
structure :: Functor f => f a -> Const f

-- | This function computes the arguments of a functorial value.
arguments :: Foldable f => f a -> [a]

-- | This function decomposes a term.
decompose :: Decompose f v => Term f -> DecompTerm f v
instance (HasVars f v, Functor f, Foldable f) => Decompose f v


-- | This module implements a simple unification algorithm using
--   compositional data types.
module Data.Comp.Unification

-- | This type represents equations between terms over a specific
--   signature.
type Equation f = (Term f, Term f)

-- | This type represents list of equations.
type Equations f = [Equation f]

-- | This type represents errors that might occur during the unification.
data UnifError f v
FailedOccursCheck :: v -> (Term f) -> UnifError f v
HeadSymbolMismatch :: (Term f) -> (Term f) -> UnifError f v
UnifError :: String -> UnifError f v
failedOccursCheck :: MonadError (UnifError f v) m => v -> Term f -> m a
headSymbolMismatch :: MonadError (UnifError f v) m => Term f -> Term f -> m a
appSubstEq :: (Ord v, HasVars f v, Functor f) => Subst f v -> Equation f -> Equation f

-- | This function returns the most general unifier of the given equations
--   using the algorithm of Martelli and Montanari.
unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) => Equations f -> m (Subst f v)
data UnifyState f v
UnifyState :: Equations f -> Subst f v -> UnifyState f v
usEqs :: UnifyState f v -> Equations f
usSubst :: UnifyState f v -> Subst f v
type UnifyM f v m a = StateT (UnifyState f v) m a
runUnifyM :: MonadError (UnifError f v) m => UnifyM f v m a -> Equations f -> m (Subst f v)
withNextEq :: Monad m => (Equation f -> UnifyM f v m ()) -> UnifyM f v m ()
putEqs :: Monad m => Equations f -> UnifyM f v m ()
putBinding :: (Monad m, Ord v, HasVars f v, Functor f) => (v, Term f) -> UnifyM f v m ()
runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) => UnifyM f v m ()
unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) => Equation f -> UnifyM f v m ()
instance Error (UnifError f v)


-- | This module defines the infrastructure necessary to use
--   <i>Compositional Data Types</i>. Compositional Data Types is an
--   extension of Wouter Swierstra's Functional Pearl: <i>Data types a la
--   carte</i>. Examples of usage are bundled with the package in the
--   library <tt>examples/Examples</tt>.
module Data.Comp


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

-- | The desugaring term homomorphism.
class (Functor f, Functor g) => Desugar f g
desugHom :: Desugar f g => TermHom f g
desugHom' :: Desugar f g => Alg f (Context g a)

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

-- | Lift desugaring to annotated terms.
desugarA :: (Functor f', Functor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' -> Term g'
instance [overlap ok] (Functor f, Functor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g[a2ams], Desugar g g[a2ams]) => Desugar (f :+: g) g[a2ams]