{-# language ConstraintKinds       #-}
{-# language DataKinds             #-}
{-# language FlexibleContexts      #-}
{-# language FlexibleInstances     #-}
{-# language GADTs                 #-}
{-# language MultiParamTypeClasses #-}
{-# language PolyKinds             #-}
{-# language QuantifiedConstraints #-}
{-# language ScopedTypeVariables   #-}
{-# language TypeApplications      #-}
{-# language TypeOperators         #-}
{-# language UndecidableInstances  #-}
module Unbound.Generics.LocallyNameless.Kind.Derive (
  -- For use with DerivingVia
  AutoAlpha(..)
  -- Default definitions for 'Alpha'
, aeqDefK
, fvAnyDefK
, closeDefK
, openDefK
, isPatDefK
, isTermDefK
, isEmbedDefK
, nthPatFindDefK
, namePatFindDefK
, swapsDefK
, lfreshenDefK
, freshenDefK
, acompareDefK
  -- Default definitions for 'Subst'
, buildSubstName
, gsubstDefK
, gsubstsDefK
, gsubstBvsDefK
) where

import           Control.Arrow                           (first)
import           Data.Function                           (on)
import           Data.Functor.Contravariant              (Contravariant (..))
import           Data.Kind                               (Type)
import           Data.List                               (find)
import           Data.Maybe                              (fromMaybe)
import           Data.Monoid                             (All (..))
import           Type.Reflection

import           Generics.Kind
import           Unbound.Generics.LocallyNameless.Alpha
import           Unbound.Generics.LocallyNameless.Fresh
import           Unbound.Generics.LocallyNameless.LFresh
import           Unbound.Generics.LocallyNameless.Name
import           Unbound.Generics.LocallyNameless.Subst
import           Unbound.Generics.PermM

type GenericAlpha a = (GenericK a, GAlphaK (RepK a) 'LoT0 'LoT0)

newtype AutoAlpha a = AutoAlpha { forall a. AutoAlpha a -> a
unAutoAlpha :: a }
                    deriving (AutoAlpha a -> AutoAlpha a -> Bool
forall a. Eq a => AutoAlpha a -> AutoAlpha a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AutoAlpha a -> AutoAlpha a -> Bool
$c/= :: forall a. Eq a => AutoAlpha a -> AutoAlpha a -> Bool
== :: AutoAlpha a -> AutoAlpha a -> Bool
$c== :: forall a. Eq a => AutoAlpha a -> AutoAlpha a -> Bool
Eq, Int -> AutoAlpha a -> ShowS
forall a. Show a => Int -> AutoAlpha a -> ShowS
forall a. Show a => [AutoAlpha a] -> ShowS
forall a. Show a => AutoAlpha a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AutoAlpha a] -> ShowS
$cshowList :: forall a. Show a => [AutoAlpha a] -> ShowS
show :: AutoAlpha a -> String
$cshow :: forall a. Show a => AutoAlpha a -> String
showsPrec :: Int -> AutoAlpha a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> AutoAlpha a -> ShowS
Show)

instance (Typeable a, GenericAlpha a, Show a) => Alpha (AutoAlpha a) where
  aeq' :: AlphaCtx -> AutoAlpha a -> AutoAlpha a -> Bool
aeq' AlphaCtx
ctx (AutoAlpha a
x) (AutoAlpha a
y)
    = forall a. GenericAlpha a => AlphaCtx -> a -> a -> Bool
aeqDefK AlphaCtx
ctx a
x a
y
  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> AutoAlpha a -> f (AutoAlpha a)
fvAny' AlphaCtx
ctx AnyName -> f AnyName
nfn (AutoAlpha a
x)
    = forall a. a -> AutoAlpha a
AutoAlpha forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (g :: * -> *) a.
(GenericAlpha a, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> a -> g a
fvAnyDefK AlphaCtx
ctx AnyName -> f AnyName
nfn a
x
  close :: AlphaCtx -> NamePatFind -> AutoAlpha a -> AutoAlpha a
close AlphaCtx
ctx NamePatFind
npf = forall a. a -> AutoAlpha a
AutoAlpha forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. GenericAlpha a => AlphaCtx -> NamePatFind -> a -> a
closeDefK AlphaCtx
ctx NamePatFind
npf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  open :: AlphaCtx -> NthPatFind -> AutoAlpha a -> AutoAlpha a
open  AlphaCtx
ctx NthPatFind
npf = forall a. a -> AutoAlpha a
AutoAlpha forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. GenericAlpha a => AlphaCtx -> NthPatFind -> a -> a
openDefK  AlphaCtx
ctx NthPatFind
npf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  isPat :: AutoAlpha a -> DisjointSet AnyName
isPat       = forall a. GenericAlpha a => a -> DisjointSet AnyName
isPatDefK   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  isTerm :: AutoAlpha a -> All
isTerm      = forall a. GenericAlpha a => a -> All
isTermDefK  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  isEmbed :: AutoAlpha a -> Bool
isEmbed     = forall a. a -> Bool
isEmbedDefK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  nthPatFind :: AutoAlpha a -> NthPatFind
nthPatFind  = forall a. GenericAlpha a => a -> NthPatFind
nthPatFindDefK  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  namePatFind :: AutoAlpha a -> NamePatFind
namePatFind = forall a. GenericAlpha a => a -> NamePatFind
namePatFindDefK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  swaps' :: AlphaCtx -> Perm AnyName -> AutoAlpha a -> AutoAlpha a
swaps' AlphaCtx
ctx Perm AnyName
perm = forall a. a -> AutoAlpha a
AutoAlpha forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. GenericAlpha a => AlphaCtx -> Perm AnyName -> a -> a
swapsDefK AlphaCtx
ctx Perm AnyName
perm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AutoAlpha a -> a
unAutoAlpha
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> AutoAlpha a -> (AutoAlpha a -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx (AutoAlpha a
x) AutoAlpha a -> Perm AnyName -> m b
cont
    = forall (m :: * -> *) a b.
(LFresh m, GenericAlpha a) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
lfreshenDefK AlphaCtx
ctx a
x (AutoAlpha a -> Perm AnyName -> m b
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> AutoAlpha a
AutoAlpha)
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> AutoAlpha a -> m (AutoAlpha a, Perm AnyName)
freshen' AlphaCtx
ctx (AutoAlpha a
x)
    = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a. a -> AutoAlpha a
AutoAlpha forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(Fresh m, GenericAlpha a) =>
AlphaCtx -> a -> m (a, Perm AnyName)
freshenDefK AlphaCtx
ctx a
x
  acompare' :: AlphaCtx -> AutoAlpha a -> AutoAlpha a -> Ordering
acompare' AlphaCtx
ctx (AutoAlpha a
x) (AutoAlpha a
y)
    = forall a. GenericAlpha a => AlphaCtx -> a -> a -> Ordering
acompareDefK AlphaCtx
ctx a
x a
y

aeqDefK :: forall a. (GenericAlpha a)
        => AlphaCtx -> a -> a -> Bool
aeqDefK :: forall a. GenericAlpha a => AlphaCtx -> a -> a -> Bool
aeqDefK AlphaCtx
c = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
c forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
fvAnyDefK :: forall g a. (GenericAlpha a, Contravariant g, Applicative g)
          => AlphaCtx -> (AnyName -> g AnyName) -> a -> g a
fvAnyDefK :: forall (g :: * -> *) a.
(GenericAlpha a, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> a -> g a
fvAnyDefK AlphaCtx
c AnyName -> g AnyName
nfn = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
c AnyName -> g AnyName
nfn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
closeDefK :: forall a. (GenericAlpha a)
          => AlphaCtx -> NamePatFind -> a -> a
closeDefK :: forall a. GenericAlpha a => AlphaCtx -> NamePatFind -> a -> a
closeDefK AlphaCtx
c NamePatFind
b = forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
c NamePatFind
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
openDefK :: forall a. (GenericAlpha a)
         => AlphaCtx -> NthPatFind -> a -> a
openDefK :: forall a. GenericAlpha a => AlphaCtx -> NthPatFind -> a -> a
openDefK AlphaCtx
c NthPatFind
b = forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
c NthPatFind
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
isPatDefK :: forall a. (GenericAlpha a)
          => a -> DisjointSet AnyName
isPatDefK :: forall a. GenericAlpha a => a -> DisjointSet AnyName
isPatDefK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
isTermDefK :: forall a. (GenericAlpha a)
           => a -> All
isTermDefK :: forall a. GenericAlpha a => a -> All
isTermDefK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
isEmbedDefK :: a -> Bool
isEmbedDefK :: forall a. a -> Bool
isEmbedDefK a
_ = Bool
False
nthPatFindDefK :: forall a. (GenericAlpha a)
               => a -> NthPatFind
nthPatFindDefK :: forall a. GenericAlpha a => a -> NthPatFind
nthPatFindDefK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
namePatFindDefK :: forall a. (GenericAlpha a)
                => a -> NamePatFind
namePatFindDefK :: forall a. GenericAlpha a => a -> NamePatFind
namePatFindDefK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
swapsDefK :: forall a. (GenericAlpha a)
          => AlphaCtx -> Perm AnyName -> a -> a
swapsDefK :: forall a. GenericAlpha a => AlphaCtx -> Perm AnyName -> a -> a
swapsDefK AlphaCtx
ctx Perm AnyName
perm = forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
lfreshenDefK :: forall m a b. (LFresh m, GenericAlpha a)
             => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
lfreshenDefK :: forall (m :: * -> *) a b.
(LFresh m, GenericAlpha a) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
lfreshenDefK AlphaCtx
ctx a
m a -> Perm AnyName -> m b
cont = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0 a
m) (a -> Perm AnyName -> m b
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0)
freshenDefK :: forall m a. (Fresh m, GenericAlpha a)
            => AlphaCtx -> a -> m (a, Perm AnyName)
freshenDefK :: forall (m :: * -> *) a.
(Fresh m, GenericAlpha a) =>
AlphaCtx -> a -> m (a, Perm AnyName)
freshenDefK AlphaCtx
ctx = forall (m :: * -> *) a. Monad m => FFM m a -> m a
retractFFM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0
acompareDefK :: forall a. (GenericAlpha a)
             => AlphaCtx -> a -> a -> Ordering
acompareDefK :: forall a. GenericAlpha a => AlphaCtx -> a -> a -> Ordering
acompareDefK AlphaCtx
c = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
c forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0

-- | The "Generic" representation version of 'Alpha'
class GAlphaK (f :: LoT k -> Type) (a :: LoT k) (b :: LoT k) where
  gaeqK :: AlphaCtx -> f a -> f b -> Bool

  gfvAnyK :: (a ~ b, Contravariant g, Applicative g)
         => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)

  gcloseK :: a ~ b => AlphaCtx -> NamePatFind -> f a -> f a
  gopenK :: a ~ b => AlphaCtx -> NthPatFind -> f a -> f a

  gisPatK :: a ~ b => f a -> DisjointSet AnyName
  gisTermK :: a ~ b => f a -> All

  gnthPatFindK :: a ~ b => f a -> NthPatFind
  gnamePatFindK :: a ~ b => f a -> NamePatFind

  gswapsK :: a ~ b => AlphaCtx -> Perm AnyName -> f a -> f a
  gfreshenK :: (a ~ b, Fresh m) => AlphaCtx -> f a -> FFM m (f a, Perm AnyName)

  glfreshenK :: (a ~ b, LFresh m) => AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c

  gacompareK :: AlphaCtx -> f a -> f b -> Ordering

instance forall t a b.
         (Alpha (Interpret t a), Alpha (Interpret t b),
          Typeable (Interpret t a), Typeable (Interpret t b))
         => GAlphaK (Field t) a b where
  gaeqK :: AlphaCtx -> Field t a -> Field t b -> Bool
gaeqK AlphaCtx
ctx (Field Interpret t a
c1) (Field Interpret t b
c2) =
    case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Interpret t a)) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Interpret t b)) of
      Maybe (Interpret t a :~~: Interpret t b)
Nothing    -> Bool
False
      Just Interpret t a :~~: Interpret t b
HRefl -> forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' AlphaCtx
ctx Interpret t a
c1 Interpret t b
c2
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> Field t a -> g (Field t a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
fvAny' AlphaCtx
ctx AnyName -> g AnyName
nfn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gfvAnyK #-}

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> Field t a -> Field t a
gcloseK AlphaCtx
ctx NamePatFind
b = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close AlphaCtx
ctx NamePatFind
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gcloseK #-}
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> Field t a -> Field t a
gopenK AlphaCtx
ctx NthPatFind
b = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
ctx NthPatFind
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gopenK #-}

  gisPatK :: (a ~ b) => Field t a -> DisjointSet AnyName
gisPatK = forall a. Alpha a => a -> DisjointSet AnyName
isPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gisPatK #-}
  gisTermK :: (a ~ b) => Field t a -> All
gisTermK = forall a. Alpha a => a -> All
isTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gisTermK #-}

  gnthPatFindK :: (a ~ b) => Field t a -> NthPatFind
gnthPatFindK = forall a. Alpha a => a -> NthPatFind
nthPatFind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gnthPatFindK #-}
  gnamePatFindK :: (a ~ b) => Field t a -> NamePatFind
gnamePatFindK = forall a. Alpha a => a -> NamePatFind
namePatFind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gnamePatFindK #-}

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> Field t a -> Field t a
gswapsK AlphaCtx
ctx Perm AnyName
perm = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' AlphaCtx
ctx Perm AnyName
perm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gswapsK #-}
  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> Field t a -> FFM m (Field t a, Perm AnyName)
gfreshenK AlphaCtx
ctx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => m a -> FFM m a
liftFFM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
freshen' AlphaCtx
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx -> Field t a -> (Field t a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (Field Interpret t a
c) Field t a -> Perm AnyName -> m c
cont = forall a (m :: * -> *) b.
(Alpha a, LFresh m) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx Interpret t a
c (Field t a -> Perm AnyName -> m c
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field)
  {-# INLINE glfreshenK #-}

  gacompareK :: AlphaCtx -> Field t a -> Field t b -> Ordering
gacompareK AlphaCtx
ctx (Field Interpret t a
c1) (Field Interpret t b
c2) =
    case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Interpret t a)) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Interpret t b)) of
      Maybe (Interpret t a :~~: Interpret t b)
Nothing    -> forall a. Ord a => a -> a -> Ordering
compare (forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Interpret t a)))
                            (forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(Interpret t b)))
      Just Interpret t a :~~: Interpret t b
HRefl -> forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' AlphaCtx
ctx Interpret t a
c1 Interpret t b
c2

instance GAlphaK f a b => GAlphaK (M1 i d f) a b where
  gaeqK :: AlphaCtx -> M1 i d f a -> M1 i d f b -> Bool
gaeqK AlphaCtx
ctx (M1 f a
f1) (M1 f b
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx f a
f1 f b
f2
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> M1 i d f a -> g (M1 i d f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gfvAnyK #-}

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> M1 i d f a -> M1 i d f a
gcloseK AlphaCtx
ctx NamePatFind
b = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gcloseK #-}
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> M1 i d f a -> M1 i d f a
gopenK AlphaCtx
ctx NthPatFind
b = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gopenK #-}

  gisPatK :: (a ~ b) => M1 i d f a -> DisjointSet AnyName
gisPatK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gisPatK #-}
  gisTermK :: (a ~ b) => M1 i d f a -> All
gisTermK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gisTermK #-}

  gnthPatFindK :: (a ~ b) => M1 i d f a -> NthPatFind
gnthPatFindK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gnthPatFindK #-}
  gnamePatFindK :: (a ~ b) => M1 i d f a -> NamePatFind
gnamePatFindK = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gnamePatFindK #-}

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> M1 i d f a -> M1 i d f a
gswapsK AlphaCtx
ctx Perm AnyName
perm = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gswapsK #-}
  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> M1 i d f a -> FFM m (M1 i d f a, Perm AnyName)
gfreshenK AlphaCtx
ctx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx
-> M1 i d f a -> (M1 i d f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (M1 f a
f) M1 i d f a -> Perm AnyName -> m c
cont =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx f a
f (M1 i d f a -> Perm AnyName -> m c
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)
  {-# INLINE glfreshenK #-}

  gacompareK :: AlphaCtx -> M1 i d f a -> M1 i d f b -> Ordering
gacompareK AlphaCtx
ctx (M1 f a
f1) (M1 f b
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx f a
f1 f b
f2

instance GAlphaK U1 a b where
  gaeqK :: AlphaCtx -> U1 a -> U1 b -> Bool
gaeqK AlphaCtx
_ctx U1 a
_ U1 b
_ = Bool
True
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> U1 a -> g (U1 a)
gfvAnyK AlphaCtx
_ctx AnyName -> g AnyName
_nfn U1 a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k (p :: k). U1 p
U1

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> U1 a -> U1 a
gcloseK AlphaCtx
_ctx NamePatFind
_b U1 a
_ = forall k (p :: k). U1 p
U1
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> U1 a -> U1 a
gopenK AlphaCtx
_ctx NthPatFind
_b U1 a
_ = forall k (p :: k). U1 p
U1

  gisPatK :: (a ~ b) => U1 a -> DisjointSet AnyName
gisPatK U1 a
_ = forall a. Monoid a => a
mempty
  gisTermK :: (a ~ b) => U1 a -> All
gisTermK U1 a
_ = forall a. Monoid a => a
mempty

  gnthPatFindK :: (a ~ b) => U1 a -> NthPatFind
gnthPatFindK U1 a
_ = forall a. Monoid a => a
mempty
  gnamePatFindK :: (a ~ b) => U1 a -> NamePatFind
gnamePatFindK U1 a
_ = forall a. Monoid a => a
mempty

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> U1 a -> U1 a
gswapsK AlphaCtx
_ctx Perm AnyName
_perm U1 a
_ = forall k (p :: k). U1 p
U1
  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> U1 a -> FFM m (U1 a, Perm AnyName)
gfreshenK AlphaCtx
_ctx U1 a
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (forall k (p :: k). U1 p
U1, forall a. Monoid a => a
mempty)
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx -> U1 a -> (U1 a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
_ctx U1 a
_ U1 a -> Perm AnyName -> m c
cont = U1 a -> Perm AnyName -> m c
cont forall k (p :: k). U1 p
U1 forall a. Monoid a => a
mempty

  gacompareK :: AlphaCtx -> U1 a -> U1 b -> Ordering
gacompareK AlphaCtx
_ctx U1 a
_ U1 b
_ = Ordering
EQ

instance (GAlphaK f a b, GAlphaK g a b) => GAlphaK (f :*: g) a b where
  gaeqK :: AlphaCtx -> (:*:) f g a -> (:*:) f g b -> Bool
gaeqK AlphaCtx
ctx (f a
f1 :*: g a
g1) (f b
f2 :*: g b
g2) =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx f a
f1 f b
f2 Bool -> Bool -> Bool
&& forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx g a
g1 g b
g2
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx
-> (AnyName -> g AnyName) -> (:*:) f g a -> g ((:*:) f g a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn (f a
f :*: g a
g) = forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn f a
f
                                    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn g a
g
  {-# INLINE gfvAnyK #-}

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> (:*:) f g a -> (:*:) f g a
gcloseK AlphaCtx
ctx NamePatFind
b (f a
f :*: g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b g a
g
  {-# INLINE gcloseK #-}
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> (:*:) f g a -> (:*:) f g a
gopenK AlphaCtx
ctx NthPatFind
b (f a
f :*: g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b g a
g
  {-# INLINE gopenK #-}

  gisPatK :: (a ~ b) => (:*:) f g a -> DisjointSet AnyName
gisPatK (f a
f :*: g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK f a
f forall a. Semigroup a => a -> a -> a
<> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK g a
g
  {-# INLINE gisPatK #-}
  gisTermK :: (a ~ b) => (:*:) f g a -> All
gisTermK (f a
f :*: g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK f a
f forall a. Semigroup a => a -> a -> a
<> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK g a
g
  {-# INLINE gisTermK #-}

  gnthPatFindK :: (a ~ b) => (:*:) f g a -> NthPatFind
gnthPatFindK (f a
f :*: g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK f a
f forall a. Semigroup a => a -> a -> a
<> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK g a
g
  {-# INLINE gnthPatFindK #-}
  gnamePatFindK :: (a ~ b) => (:*:) f g a -> NamePatFind
gnamePatFindK (f a
f :*: g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK f a
f forall a. Semigroup a => a -> a -> a
<> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK g a
g
  {-# INLINE gnamePatFindK #-}

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> (:*:) f g a -> (:*:) f g a
gswapsK AlphaCtx
ctx Perm AnyName
perm (f a
f :*: g a
g) =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm g a
g
  {-# INLINE gswapsK #-}

  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> (:*:) f g a -> FFM m ((:*:) f g a, Perm AnyName)
gfreshenK AlphaCtx
ctx (f a
f :*: g a
g) = do
    ~(g a
g', Perm AnyName
perm2) <- forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx g a
g
    ~(f a
f', Perm AnyName
perm1) <- forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm2 f a
f)
    forall (m :: * -> *) a. Monad m => a -> m a
return (f a
f' forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
g', Perm AnyName
perm1 forall a. Semigroup a => a -> a -> a
<> Perm AnyName
perm2)
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx
-> (:*:) f g a -> ((:*:) f g a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (f a
f :*: g a
g) (:*:) f g a -> Perm AnyName -> m c
cont =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx g a
g forall a b. (a -> b) -> a -> b
$ \g a
g' Perm AnyName
perm2 ->
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm2 f a
f) forall a b. (a -> b) -> a -> b
$ \f a
f' Perm AnyName
perm1 ->
    (:*:) f g a -> Perm AnyName -> m c
cont (f a
f' forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
g') (Perm AnyName
perm1 forall a. Semigroup a => a -> a -> a
<> Perm AnyName
perm2)
  {-# INLINE glfreshenK #-}

  gacompareK :: AlphaCtx -> (:*:) f g a -> (:*:) f g b -> Ordering
gacompareK AlphaCtx
ctx (f a
f1 :*: g a
g1) (f b
f2 :*: g b
g2) =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx f a
f1 f b
f2 forall a. Semigroup a => a -> a -> a
<> forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx g a
g1 g b
g2

instance (GAlphaK f a b, GAlphaK g a b) => GAlphaK (f :+: g) a b where
  gaeqK :: AlphaCtx -> (:+:) f g a -> (:+:) f g b -> Bool
gaeqK AlphaCtx
ctx  (L1 f a
f1) (L1 f b
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx f a
f1 f b
f2
  gaeqK AlphaCtx
ctx  (R1 g a
g1) (R1 g b
g2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx g a
g1 g b
g2
  gaeqK AlphaCtx
_ctx (:+:) f g a
_       (:+:) f g b
_       = Bool
False
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx
-> (AnyName -> g AnyName) -> (:+:) f g a -> g ((:+:) f g a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn (L1 f a
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn f a
f)
  gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn (R1 g a
g) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn g a
g)
  {-# INLINE gfvAnyK #-}

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> (:+:) f g a -> (:+:) f g a
gcloseK AlphaCtx
ctx NamePatFind
b (L1 f a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b f a
f)
  gcloseK AlphaCtx
ctx NamePatFind
b (R1 g a
g) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b g a
g)
  {-# INLINE gcloseK #-}
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> (:+:) f g a -> (:+:) f g a
gopenK AlphaCtx
ctx NthPatFind
b (L1 f a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b f a
f)
  gopenK AlphaCtx
ctx NthPatFind
b (R1 g a
g) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b g a
g)
  {-# INLINE gopenK #-}

  gisPatK :: (a ~ b) => (:+:) f g a -> DisjointSet AnyName
gisPatK (L1 f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK f a
f
  gisPatK (R1 g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK g a
g
  {-# INLINE gisPatK #-}

  gisTermK :: (a ~ b) => (:+:) f g a -> All
gisTermK (L1 f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK f a
f
  gisTermK (R1 g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK g a
g
  {-# INLINE gisTermK #-}

  gnthPatFindK :: (a ~ b) => (:+:) f g a -> NthPatFind
gnthPatFindK (L1 f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK f a
f
  gnthPatFindK (R1 g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK g a
g
  {-# INLINE gnthPatFindK #-}

  gnamePatFindK :: (a ~ b) => (:+:) f g a -> NamePatFind
gnamePatFindK (L1 f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK f a
f
  gnamePatFindK (R1 g a
g) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK g a
g
  {-# INLINE gnamePatFindK #-}

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> (:+:) f g a -> (:+:) f g a
gswapsK AlphaCtx
ctx Perm AnyName
perm (L1 f a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm f a
f)
  gswapsK AlphaCtx
ctx Perm AnyName
perm (R1 g a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm g a
f)
  {-# INLINE gswapsK #-}

  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> (:+:) f g a -> FFM m ((:+:) f g a, Perm AnyName)
gfreshenK AlphaCtx
ctx (L1 f a
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1) (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx f a
f)
  gfreshenK AlphaCtx
ctx (R1 g a
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx g a
f)
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx
-> (:+:) f g a -> ((:+:) f g a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (L1 f a
f) (:+:) f g a -> Perm AnyName -> m c
cont =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx f a
f ((:+:) f g a -> Perm AnyName -> m c
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)
  glfreshenK AlphaCtx
ctx (R1 g a
g) (:+:) f g a -> Perm AnyName -> m c
cont =
    forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx g a
g ((:+:) f g a -> Perm AnyName -> m c
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1)
  {-# INLINE glfreshenK #-}

  gacompareK :: AlphaCtx -> (:+:) f g a -> (:+:) f g b -> Ordering
gacompareK AlphaCtx
_ctx (L1 f a
_) (R1 g b
_)   = Ordering
LT
  gacompareK AlphaCtx
_ctx (R1 g a
_) (L1 f b
_)   = Ordering
GT
  gacompareK AlphaCtx
ctx  (L1 f a
f1) (L1 f b
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx f a
f1 f b
f2
  gacompareK AlphaCtx
ctx  (R1 g a
g1) (R1 g b
g2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx g a
g1 g b
g2
  {-# INLINE gacompareK #-}

instance ((Interpret c a, Interpret c b) => GAlphaK f a b)
         => GAlphaK (c :=>: f) a b where
  gaeqK :: AlphaCtx -> (:=>:) c f a -> (:=>:) c f b -> Bool
gaeqK AlphaCtx
ctx (SuchThat f a
f1) (SuchThat f b
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx f a
f1 f b
f2
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx
-> (AnyName -> g AnyName) -> (:=>:) c f a -> g ((:=>:) c f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn (SuchThat f a
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn f a
f)
  {-# INLINE gfvAnyK #-}

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> (:=>:) c f a -> (:=>:) c f a
gcloseK AlphaCtx
ctx NamePatFind
b (SuchThat f a
f) = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b f a
f)
  {-# INLINE gcloseK #-}
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> (:=>:) c f a -> (:=>:) c f a
gopenK AlphaCtx
ctx NthPatFind
b (SuchThat f a
f) = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b f a
f)
  {-# INLINE gopenK #-}

  gisPatK :: (a ~ b) => (:=>:) c f a -> DisjointSet AnyName
gisPatK (SuchThat f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK f a
f
  {-# INLINE gisPatK #-}

  gisTermK :: (a ~ b) => (:=>:) c f a -> All
gisTermK (SuchThat f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK f a
f
  {-# INLINE gisTermK #-}

  gnthPatFindK :: (a ~ b) => (:=>:) c f a -> NthPatFind
gnthPatFindK (SuchThat f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK f a
f
  {-# INLINE gnthPatFindK #-}

  gnamePatFindK :: (a ~ b) => (:=>:) c f a -> NamePatFind
gnamePatFindK (SuchThat f a
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK f a
f
  {-# INLINE gnamePatFindK #-}

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> (:=>:) c f a -> (:=>:) c f a
gswapsK AlphaCtx
ctx Perm AnyName
perm (SuchThat f a
f) = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm f a
f)
  {-# INLINE gswapsK #-}

  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> (:=>:) c f a -> FFM m ((:=>:) c f a, Perm AnyName)
gfreshenK AlphaCtx
ctx (SuchThat f a
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat) (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx f a
f)
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx
-> (:=>:) c f a -> ((:=>:) c f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (SuchThat f a
f) (:=>:) c f a -> Perm AnyName -> m c
cont = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx f a
f ((:=>:) c f a -> Perm AnyName -> m c
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat)
  {-# INLINE glfreshenK #-}

  gacompareK :: AlphaCtx -> (:=>:) c f a -> (:=>:) c f b -> Ordering
gacompareK AlphaCtx
ctx (SuchThat f a
f1) (SuchThat f b
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx f a
f1 f b
f2
  {-# INLINE gacompareK #-}

instance (forall (t1 :: k) (t2 :: k). GAlphaK f (t1 ':&&: a) (t2 ':&&: b))
         => GAlphaK (Exists k f) a b where

  gaeqK :: AlphaCtx -> Exists k f a -> Exists k f b -> Bool
gaeqK AlphaCtx
ctx (Exists f (t ':&&: a)
f1) (Exists f (t ':&&: b)
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Bool
gaeqK AlphaCtx
ctx f (t ':&&: a)
f1 f (t ':&&: b)
f2
  {-# INLINE gaeqK #-}

  gfvAnyK :: forall (g :: * -> *).
(a ~ b, Contravariant g, Applicative g) =>
AlphaCtx
-> (AnyName -> g AnyName) -> Exists k f a -> g (Exists k f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn (Exists f (t ':&&: a)
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (g :: * -> *).
(GAlphaK f a b, a ~ b, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAnyK AlphaCtx
ctx AnyName -> g AnyName
nfn f (t ':&&: a)
f)
  {-# INLINE gfvAnyK #-}

  gcloseK :: (a ~ b) => AlphaCtx -> NamePatFind -> Exists k f a -> Exists k f a
gcloseK AlphaCtx
ctx NamePatFind
b (Exists f (t ':&&: a)
f) = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NamePatFind -> f a -> f a
gcloseK AlphaCtx
ctx NamePatFind
b f (t ':&&: a)
f)
  {-# INLINE gcloseK #-}
  gopenK :: (a ~ b) => AlphaCtx -> NthPatFind -> Exists k f a -> Exists k f a
gopenK AlphaCtx
ctx NthPatFind
b (Exists f (t ':&&: a)
f) = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> NthPatFind -> f a -> f a
gopenK AlphaCtx
ctx NthPatFind
b f (t ':&&: a)
f)
  {-# INLINE gopenK #-}

  gisPatK :: (a ~ b) => Exists k f a -> DisjointSet AnyName
gisPatK (Exists f (t ':&&: a)
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> DisjointSet AnyName
gisPatK f (t ':&&: a)
f
  {-# INLINE gisPatK #-}

  gisTermK :: (a ~ b) => Exists k f a -> All
gisTermK (Exists f (t ':&&: a)
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> All
gisTermK f (t ':&&: a)
f
  {-# INLINE gisTermK #-}

  gnthPatFindK :: (a ~ b) => Exists k f a -> NthPatFind
gnthPatFindK (Exists f (t ':&&: a)
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NthPatFind
gnthPatFindK f (t ':&&: a)
f
  {-# INLINE gnthPatFindK #-}

  gnamePatFindK :: (a ~ b) => Exists k f a -> NamePatFind
gnamePatFindK (Exists f (t ':&&: a)
f) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
f a -> NamePatFind
gnamePatFindK f (t ':&&: a)
f
  {-# INLINE gnamePatFindK #-}

  gswapsK :: (a ~ b) => AlphaCtx -> Perm AnyName -> Exists k f a -> Exists k f a
gswapsK AlphaCtx
ctx Perm AnyName
perm (Exists f (t ':&&: a)
f) = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
(GAlphaK f a b, a ~ b) =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswapsK AlphaCtx
ctx Perm AnyName
perm f (t ':&&: a)
f)
  {-# INLINE gswapsK #-}

  gfreshenK :: forall (m :: * -> *).
(a ~ b, Fresh m) =>
AlphaCtx -> Exists k f a -> FFM m (Exists k f a, Perm AnyName)
gfreshenK AlphaCtx
ctx (Exists f (t ':&&: a)
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists) (forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *).
(GAlphaK f a b, a ~ b, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshenK AlphaCtx
ctx f (t ':&&: a)
f)
  {-# INLINE gfreshenK #-}

  glfreshenK :: forall (m :: * -> *) c.
(a ~ b, LFresh m) =>
AlphaCtx
-> Exists k f a -> (Exists k f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx (Exists f (t ':&&: a)
f) Exists k f a -> Perm AnyName -> m c
cont = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) (m :: * -> *)
       c.
(GAlphaK f a b, a ~ b, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c
glfreshenK AlphaCtx
ctx f (t ':&&: a)
f (Exists k f a -> Perm AnyName -> m c
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists)
  {-# INLINE glfreshenK #-}

  gacompareK :: AlphaCtx -> Exists k f a -> Exists k f b -> Ordering
gacompareK AlphaCtx
ctx (Exists f (t ':&&: a)
f1) (Exists f (t ':&&: b)
f2) = forall k (f :: LoT k -> *) (a :: LoT k) (b :: LoT k).
GAlphaK f a b =>
AlphaCtx -> f a -> f b -> Ordering
gacompareK AlphaCtx
ctx f (t ':&&: a)
f1 f (t ':&&: b)
f2

gsubstDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a)
           => Name b -> b -> a -> a
gsubstDefK :: forall a b.
(GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) =>
Name b -> b -> a -> a
gsubstDefK Name b
n b
u a
x =
  if forall a. Name a -> Bool
isFreeName Name b
n
  then case (forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
    Just (SubstName Name a
m) | Name a
m forall a. Eq a => a -> a -> Bool
== Name b
n -> b
u
    Maybe (SubstName a b)
_ -> case (forall b a. Subst b a => a -> Maybe (SubstCoerce a b)
isCoerceVar a
x :: Maybe (SubstCoerce a b)) of
      Just (SubstCoerce Name b
m b -> Maybe a
f) | Name b
m forall a. Eq a => a -> a -> Bool
== Name b
n -> forall a. a -> Maybe a -> a
fromMaybe a
x (b -> Maybe a
f b
u)
      Maybe (SubstCoerce a b)
_                               -> forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
n b
u (forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0 a
x)
  else forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Cannot substitute for bound variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name b
n

gsubstsDefK :: 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
gsubstsDefK [(Name b, b)]
ss a
x
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Name a -> Bool
isFreeName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name b, b)]
ss =
    case (forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
      Just (SubstName Name a
m) | Just (Name a
_, b
u) <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((forall a. Eq a => a -> a -> Bool
==Name a
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name b, b)]
ss -> b
u
      Maybe (SubstName a b)
_ -> case forall b a. Subst b a => a -> Maybe (SubstCoerce a b)
isCoerceVar a
x :: Maybe (SubstCoerce a b) of
          Just (SubstCoerce Name b
m b -> Maybe a
f) | Just (Name b
_, b
u) <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((forall a. Eq a => a -> a -> Bool
==Name b
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name b, b)]
ss -> forall a. a -> Maybe a -> a
fromMaybe a
x (b -> Maybe a
f b
u)
          Maybe (SubstCoerce a b)
_ -> forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss (forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0 a
x)
  | Bool
otherwise =
    forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Cannot substitute for bound variable in: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name b, b)]
ss)

gsubstBvsDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a)
              => AlphaCtx -> [b] -> a -> a
gsubstBvsDefK :: forall a b.
(GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) =>
AlphaCtx -> [b] -> a -> a
gsubstBvsDefK AlphaCtx
ctx [b]
bs a
x =
  case (forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
    Just (SubstName (Bn Integer
j Integer
k)) | AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx forall a. Eq a => a -> a -> Bool
== Integer
j, forall a. Num a => Integer -> a
fromInteger Integer
k forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
bs -> [b]
bs forall a. [a] -> Int -> a
!! forall a. Num a => Integer -> a
fromInteger Integer
k
    Maybe (SubstName a b)
_ -> forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @a @'LoT0 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
bs (forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @a @'LoT0 a
x)

buildSubstName :: forall a b. (Typeable a, Typeable b)
               => Name a -> Maybe (SubstName a b)
buildSubstName :: forall a b.
(Typeable a, Typeable b) =>
Name a -> Maybe (SubstName a b)
buildSubstName Name a
x = case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
  Maybe (a :~~: b)
Nothing    -> forall a. Maybe a
Nothing
  Just a :~~: b
HRefl -> forall a. a -> Maybe a
Just (forall a b. (a ~ b) => Name a -> SubstName a b
SubstName Name a
x)

class GSubstK b (f :: LoT k -> Type) (a :: LoT k) where
  gsubstK :: Name b -> b -> f a -> f a
  gsubstsK :: [(Name b, b)] -> f a -> f a
  gsubstBvsK :: AlphaCtx -> [b] -> f a -> f a

instance Subst b (Interpret t a) => GSubstK b (Field t) a where
  gsubstK :: Name b -> b -> Field t a -> Field t a
gsubstK Name b
nm b
val = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Subst b a => Name b -> b -> a -> a
subst Name b
nm b
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  gsubstsK :: [(Name b, b)] -> Field t a -> Field t a
gsubstsK [(Name b, b)]
ss = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name b, b)]
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField
  gsubstBvsK :: AlphaCtx -> [b] -> Field t a -> Field t a
gsubstBvsK AlphaCtx
ctx [b]
ss = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs AlphaCtx
ctx [b]
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
unField

instance GSubstK b f a => GSubstK b (M1 i c f) a where
  gsubstK :: Name b -> b -> M1 i c f a -> M1 i c f a
gsubstK Name b
nm b
val = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  gsubstsK :: [(Name b, b)] -> M1 i c f a -> M1 i c f a
gsubstsK [(Name b, b)]
ss = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  gsubstBvsK :: AlphaCtx -> [b] -> M1 i c f a -> M1 i c f a
gsubstBvsK AlphaCtx
ctx [b]
ss = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance GSubstK b U1 a where
  gsubstK :: Name b -> b -> U1 a -> U1 a
gsubstK Name b
_nm b
_val U1 a
_ = forall k (p :: k). U1 p
U1
  gsubstsK :: [(Name b, b)] -> U1 a -> U1 a
gsubstsK [(Name b, b)]
_ss U1 a
_ = forall k (p :: k). U1 p
U1
  gsubstBvsK :: AlphaCtx -> [b] -> U1 a -> U1 a
gsubstBvsK AlphaCtx
_ctx [b]
_ss U1 a
_ = forall k (p :: k). U1 p
U1

instance (GSubstK b f a, GSubstK b g a) => GSubstK b (f :*: g) a where
  gsubstK :: Name b -> b -> (:*:) f g a -> (:*:) f g a
gsubstK Name b
nm b
val (f a
f :*: g a
g) = forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val g a
g
  gsubstsK :: [(Name b, b)] -> (:*:) f g a -> (:*:) f g a
gsubstsK [(Name b, b)]
ss (f a
f :*: g a
g) = forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss g a
g
  gsubstBvsK :: AlphaCtx -> [b] -> (:*:) f g a -> (:*:) f g a
gsubstBvsK AlphaCtx
ctx [b]
ss (f a
f :*: g a
g) = forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss g a
g

instance (GSubstK b f a, GSubstK b g a) => GSubstK b (f :+: g) a where
  gsubstK :: Name b -> b -> (:+:) f g a -> (:+:) f g a
gsubstK Name b
nm b
val (L1 f a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val f a
f
  gsubstK Name b
nm b
val (R1 g a
g) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val g a
g

  gsubstsK :: [(Name b, b)] -> (:+:) f g a -> (:+:) f g a
gsubstsK [(Name b, b)]
ss (L1 f a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss f a
f
  gsubstsK [(Name b, b)]
ss (R1 g a
g) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss g a
g

  gsubstBvsK :: AlphaCtx -> [b] -> (:+:) f g a -> (:+:) f g a
gsubstBvsK AlphaCtx
ctx [b]
ss (L1 f a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss f a
f
  gsubstBvsK AlphaCtx
ctx [b]
ss (R1 g a
g) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss g a
g

instance ((Interpret c a) => GSubstK b f a) => GSubstK b (c :=>: f) a where
  gsubstK :: Name b -> b -> (:=>:) c f a -> (:=>:) c f a
gsubstK Name b
nm b
val (SuchThat f a
f) = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val f a
f
  gsubstsK :: [(Name b, b)] -> (:=>:) c f a -> (:=>:) c f a
gsubstsK [(Name b, b)]
ss (SuchThat f a
f) = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss f a
f
  gsubstBvsK :: AlphaCtx -> [b] -> (:=>:) c f a -> (:=>:) c f a
gsubstBvsK AlphaCtx
ctx [b]
ss (SuchThat f a
f) = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss f a
f

instance (forall (t :: k). GSubstK b f (t ':&&: a)) => GSubstK b (Exists k f) a where
  gsubstK :: Name b -> b -> Exists k f a -> Exists k f a
gsubstK Name b
nm b
val (Exists f (t ':&&: a)
f) = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
Name b -> b -> f a -> f a
gsubstK Name b
nm b
val f (t ':&&: a)
f
  gsubstsK :: [(Name b, b)] -> Exists k f a -> Exists k f a
gsubstsK [(Name b, b)]
ss (Exists f (t ':&&: a)
f) = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
[(Name b, b)] -> f a -> f a
gsubstsK [(Name b, b)]
ss f (t ':&&: a)
f
  gsubstBvsK :: AlphaCtx -> [b] -> Exists k f a -> Exists k f a
gsubstBvsK AlphaCtx
ctx [b]
ss (Exists f (t ':&&: a)
f) = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists forall a b. (a -> b) -> a -> b
$ forall k b (f :: LoT k -> *) (a :: LoT k).
GSubstK b f a =>
AlphaCtx -> [b] -> f a -> f a
gsubstBvsK AlphaCtx
ctx [b]
ss f (t ':&&: a)
f