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


-- | Support for programming with names and binders using kind-generics
--   
--   Specify the binding structure of your data type with an expressive set
--   of type combinators, and unbound-generics handles the rest!
--   Automatically derives alpha-equivalence, free variable calculation,
--   capture-avoiding substitution, and more. See
--   <tt>Unbound.Generics.LocallyNameless.Kind.Derive</tt> to get started.
--   
--   This is an independent re-implementation of <a>unbound-generics</a>
--   but using <a>kind-generics</a> instead of <a>GHC Generics</a>.
@package unbound-kind-generics
@version 0.2.1.1

module Unbound.Generics.LocallyNameless.Kind.Derive
newtype AutoAlpha a
AutoAlpha :: a -> AutoAlpha a
[unAutoAlpha] :: AutoAlpha a -> a
aeqDefK :: forall a. GenericAlpha a => AlphaCtx -> a -> a -> Bool
fvAnyDefK :: forall g a. (GenericAlpha a, Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> a -> g a
closeDefK :: forall a. GenericAlpha a => AlphaCtx -> NamePatFind -> a -> a
openDefK :: forall a. GenericAlpha a => AlphaCtx -> NthPatFind -> a -> a
isPatDefK :: forall a. GenericAlpha a => a -> DisjointSet AnyName
isTermDefK :: forall a. GenericAlpha a => a -> All
isEmbedDefK :: a -> Bool
nthPatFindDefK :: forall a. GenericAlpha a => a -> NthPatFind
namePatFindDefK :: forall a. GenericAlpha a => a -> NamePatFind
swapsDefK :: forall a. GenericAlpha a => AlphaCtx -> Perm AnyName -> a -> a
lfreshenDefK :: forall m a b. (LFresh m, GenericAlpha a) => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
freshenDefK :: forall m a. (Fresh m, GenericAlpha a) => AlphaCtx -> a -> m (a, Perm AnyName)
acompareDefK :: forall a. GenericAlpha a => AlphaCtx -> a -> a -> Ordering
buildSubstName :: forall a b. (Typeable a, Typeable b) => Name a -> Maybe (SubstName a b)
gsubstDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) => Name b -> b -> a -> a
gsubstsDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) => [(Name b, b)] -> a -> a
gsubstBvsDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) => AlphaCtx -> [b] -> a -> a
instance GHC.Show.Show a => GHC.Show.Show (Unbound.Generics.LocallyNameless.Kind.Derive.AutoAlpha a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Unbound.Generics.LocallyNameless.Kind.Derive.AutoAlpha a)
instance forall k b (t :: Data.PolyKinded.Atom.Atom k (*)) (a :: Data.PolyKinded.LoT k). Unbound.Generics.LocallyNameless.Subst.Subst b (Data.PolyKinded.Atom.Interpret t a) => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b (Generics.Kind.Field t) a
instance forall k b (f :: Data.PolyKinded.LoT k -> *) (a :: Data.PolyKinded.LoT k) i (c :: GHC.Generics.Meta). Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b f a => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b (GHC.Generics.M1 i c f) a
instance forall k b (a :: Data.PolyKinded.LoT k). Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b GHC.Generics.U1 a
instance forall k b (f :: Data.PolyKinded.LoT k -> *) (a :: Data.PolyKinded.LoT k) (g :: Data.PolyKinded.LoT k -> *). (Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b f a, Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b g a) => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b (f GHC.Generics.:*: g) a
instance forall k b (f :: Data.PolyKinded.LoT k -> *) (a :: Data.PolyKinded.LoT k) (g :: Data.PolyKinded.LoT k -> *). (Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b f a, Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b g a) => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b (f GHC.Generics.:+: g) a
instance forall k (c :: Data.PolyKinded.Atom.Atom k GHC.Types.Constraint) (a :: Data.PolyKinded.LoT k) b (f :: Data.PolyKinded.LoT k -> *). (Data.PolyKinded.Atom.Interpret c a => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b f a) => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b (c Generics.Kind.:=>: f) a
instance forall k1 k2 b (f :: Data.PolyKinded.LoT (k2 -> k1) -> *) (a :: Data.PolyKinded.LoT k1). (forall (t :: k2). Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b f (t 'Data.PolyKinded.:&&: a)) => Unbound.Generics.LocallyNameless.Kind.Derive.GSubstK b (Generics.Kind.Exists k2 f) a
instance (Data.Typeable.Internal.Typeable a, Unbound.Generics.LocallyNameless.Kind.Derive.GenericAlpha a, GHC.Show.Show a) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Kind.Derive.AutoAlpha a)
instance forall k (t :: Data.PolyKinded.Atom.Atom k (*)) (a :: Data.PolyKinded.LoT k) (b :: Data.PolyKinded.LoT k). (Unbound.Generics.LocallyNameless.Alpha.Alpha (Data.PolyKinded.Atom.Interpret t a), Unbound.Generics.LocallyNameless.Alpha.Alpha (Data.PolyKinded.Atom.Interpret t b), Data.Typeable.Internal.Typeable (Data.PolyKinded.Atom.Interpret t a), Data.Typeable.Internal.Typeable (Data.PolyKinded.Atom.Interpret t b)) => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK (Generics.Kind.Field t) a b
instance forall k (f :: Data.PolyKinded.LoT k -> *) (a :: Data.PolyKinded.LoT k) (b :: Data.PolyKinded.LoT k) i (d :: GHC.Generics.Meta). Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK f a b => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK (GHC.Generics.M1 i d f) a b
instance forall k (a :: Data.PolyKinded.LoT k) (b :: Data.PolyKinded.LoT k). Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK GHC.Generics.U1 a b
instance forall k (f :: Data.PolyKinded.LoT k -> *) (a :: Data.PolyKinded.LoT k) (b :: Data.PolyKinded.LoT k) (g :: Data.PolyKinded.LoT k -> *). (Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK f a b, Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK g a b) => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK (f GHC.Generics.:*: g) a b
instance forall k (f :: Data.PolyKinded.LoT k -> *) (a :: Data.PolyKinded.LoT k) (b :: Data.PolyKinded.LoT k) (g :: Data.PolyKinded.LoT k -> *). (Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK f a b, Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK g a b) => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK (f GHC.Generics.:+: g) a b
instance forall k (c :: Data.PolyKinded.Atom.Atom k GHC.Types.Constraint) (a :: Data.PolyKinded.LoT k) (b :: Data.PolyKinded.LoT k) (f :: Data.PolyKinded.LoT k -> *). ((Data.PolyKinded.Atom.Interpret c a, Data.PolyKinded.Atom.Interpret c b) => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK f a b) => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK (c Generics.Kind.:=>: f) a b
instance forall k1 k2 (f :: Data.PolyKinded.LoT (k2 -> k1) -> *) (a :: Data.PolyKinded.LoT k1) (b :: Data.PolyKinded.LoT k1). (forall (t1 :: k2) (t2 :: k2). Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK f (t1 'Data.PolyKinded.:&&: a) (t2 'Data.PolyKinded.:&&: b)) => Unbound.Generics.LocallyNameless.Kind.Derive.GAlphaK (Generics.Kind.Exists k2 f) a b


-- | Example of how to use `unbound-kind-generics`
module Unbound.Generics.LocallyNameless.Kind.Example

-- | Variables stand for expressions
type Var t = Name (Expr t)

-- | Well-typed lambda expressions
data Expr t
[V] :: Var t -> Expr t
[Lam] :: (Typeable a, Typeable b) => Bind (Var a) (Expr b) -> Expr (a -> b)
[App] :: Typeable a => Expr (a -> b) -> Expr a -> Expr b
eval :: Typeable t => Expr t -> FreshM (Expr t)
example :: forall a. Typeable a => Expr (a -> a)
instance GHC.Show.Show (Unbound.Generics.LocallyNameless.Kind.Example.Expr t)
instance Generics.Kind.GenericK (Unbound.Generics.LocallyNameless.Kind.Example.Expr t)
instance Generics.Kind.GenericK Unbound.Generics.LocallyNameless.Kind.Example.Expr
instance Data.Typeable.Internal.Typeable t => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Kind.Example.Expr t)
instance (Data.Typeable.Internal.Typeable small, Data.Typeable.Internal.Typeable big) => Unbound.Generics.LocallyNameless.Subst.Subst (Unbound.Generics.LocallyNameless.Kind.Example.Expr small) (Unbound.Generics.LocallyNameless.Kind.Example.Expr big)