content: {-# OPTIONS_HADDOCK show-extensions #-}
  -- |
  -- Module     : Unbound.Generics.LocallyNameless.Alpha
  -- Copyright  : (c) 2014, Aleksey Kliger
  -- License    : BSD3 (See LICENSE)
  -- Maintainer : Aleksey Kliger
  -- Stability  : experimental
  --
  -- Use the 'Alpha' typeclass to mark types that may contain 'Name's.
  {-# LANGUAGE DefaultSignatures
               , FlexibleContexts
               , TypeOperators
               , RankNTypes
    #-}
  module Unbound.Generics.LocallyNameless.Alpha (
    -- * Name-aware opertions
    Alpha(..)
    -- * Binder variables
    , DisjointSet(..)
    , inconsistentDisjointSet
    , singletonDisjointSet
    , isConsistentDisjointSet
    , isNullDisjointSet
    -- * Implementation details
    , NthPatFind(..)
    , NamePatFind(..)
    , AlphaCtx
    , ctxLevel
    , initialCtx
    , patternCtx
    , termCtx
    , isTermCtx
    , incrLevelCtx
    , decrLevelCtx
    , isZeroLevelCtx
    , ctxLevel
    -- * Internal
    , gaeq
    , gfvAny
    , gclose
    , gopen
    , gisPat
    , gisTerm
    , gnthPatFind
    , gnamePatFind
    , gswaps
    , gfreshen
    , glfreshen
    , gacompare
      -- ** Interal helpers for gfreshen
    , FFM
    , liftFFM
    , retractFFM
    ) where
  
  import Control.Applicative (Applicative(..), (<$>))
  import Control.Arrow (first)
  import Control.Monad (liftM)
  import Data.Function (on)
  import Data.Functor.Contravariant (Contravariant(..))
  import Data.Foldable (Foldable(..))
  import Data.List (intersect)
  import Data.List.NonEmpty (NonEmpty)
  import Data.Monoid (Monoid(..), All(..))
  import Data.Ratio (Ratio)
  import Data.Semigroup as Sem
  import Data.Typeable (Typeable, gcast, typeOf)
  import GHC.Generics
  
  import Unbound.Generics.LocallyNameless.Name
  import Unbound.Generics.LocallyNameless.Fresh
  import Unbound.Generics.LocallyNameless.LFresh
  import Unbound.Generics.PermM
  
  -- | Some 'Alpha' operations need to record information about their
  -- progress.  Instances should just pass it through unchanged.
  --
  -- The context records whether we are currently operating on terms or patterns,
  -- and how many binding levels we've descended.
  data AlphaCtx = AlphaCtx { ctxMode :: !Mode, ctxLevel :: !Integer }
  
  data Mode = Term | Pat
            deriving Eq
  
  -- | The starting context for alpha operations: we are expecting to
  -- work on terms and we are under no binders.
  initialCtx :: AlphaCtx
  initialCtx = AlphaCtx { ctxMode = Term, ctxLevel = 0 }
  
  -- | Switches to a context where we expect to operate on patterns.
  patternCtx :: AlphaCtx -> AlphaCtx
  patternCtx ctx = ctx { ctxMode = Pat }
  
  -- | Switches to a context where we expect to operate on terms.
  termCtx :: AlphaCtx -> AlphaCtx
  termCtx ctx = ctx { ctxMode = Term }
  
  -- | Returns 'True' iff we are in a context where we expect to see terms.
  isTermCtx :: AlphaCtx -> Bool
  isTermCtx (AlphaCtx {ctxMode = Term}) = True
  isTermCtx _                           = False
  
  -- | Increment the number of binders that we are operating under.
  incrLevelCtx :: AlphaCtx -> AlphaCtx
  incrLevelCtx ctx = ctx { ctxLevel = 1 + ctxLevel ctx }
  
  -- | Decrement the number of binders that we are operating under.
  decrLevelCtx :: AlphaCtx -> AlphaCtx
  decrLevelCtx ctx = ctx { ctxLevel = ctxLevel ctx - 1 }
  
  -- | Are we operating under no binders?
  isZeroLevelCtx :: AlphaCtx -> Bool
  isZeroLevelCtx ctx = ctxLevel ctx == 0
  
  -- | A @DisjointSet a@ is a 'Just' a list of distinct @a@s.  In addition to a monoidal
  -- structure, a disjoint set also has an annihilator 'inconsistentDisjointSet'.
  --
  -- @
  --   inconsistentDisjointSet \<> s == inconsistentDisjointSet
  --   s \<> inconsistentDisjoinSet == inconsistentDisjointSet
  -- @
  newtype DisjointSet a = DisjointSet (Maybe [a])
  
  -- | @since 0.3.2
  instance Eq a => Sem.Semigroup (DisjointSet a) where
    (<>) = \s1 s2 ->
      case (s1, s2) of
        (DisjointSet (Just xs), DisjointSet (Just ys)) | disjointLists xs ys -> DisjointSet (Just (xs <> ys))
        _ -> inconsistentDisjointSet
  
  instance Eq a => Monoid (DisjointSet a) where
    mempty = DisjointSet (Just [])
    mappend = (<>)
  
  instance Foldable DisjointSet where
    foldMap summarize (DisjointSet ms) = foldMap (foldMap summarize) ms
  
  -- | Returns a @DisjointSet a@ that is the annihilator element for the 'Monoid' instance of 'DisjointSet'.
  inconsistentDisjointSet :: DisjointSet a
  inconsistentDisjointSet = DisjointSet Nothing
  
  -- | @singletonDisjointSet x@ a @DisjointSet a@ that contains the single element @x@
  singletonDisjointSet :: a -> DisjointSet a
  singletonDisjointSet x = DisjointSet (Just [x])
  
  disjointLists :: Eq a => [a] -> [a] -> Bool
  disjointLists xs ys = null (intersect xs ys)
  
  -- | @isConsistentDisjointSet@ returns @True@ iff the given disjoint set is not inconsistent.
  isConsistentDisjointSet :: DisjointSet a -> Bool
  isConsistentDisjointSet (DisjointSet Nothing) = False
  isConsistentDisjointSet _ = True
  
  -- | @isNullDisjointSet@ return @True@ iff the given disjoint set is 'mempty'.
  isNullDisjointSet :: DisjointSet a -> Bool
  isNullDisjointSet (DisjointSet (Just [])) = True
  isNullDisjointSet _ = False
  
  -- | Types that are instances of @Alpha@ may participate in name representation.
  --
  -- Minimal instance is entirely empty, provided that your type is an instance of
  -- 'Generic'.
  class (Show a) => Alpha a where
    -- | See 'Unbound.Generics.LocallyNameless.Operations.aeq'.
    aeq' :: AlphaCtx -> a -> a -> Bool
    default aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool
    aeq' c = (gaeq c) `on` from
    {-# INLINE aeq' #-}
  
    -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.
    --
    -- @
    --  fvAny' :: Fold a AnyName
    -- @
    fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
    default fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
    fvAny' c nfn = fmap to . gfvAny c nfn . from
    {-# INLINE fvAny' #-}
  
    -- | Replace free names by bound names.
    close :: AlphaCtx -> NamePatFind -> a -> a
    default close :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NamePatFind -> a -> a
    close c b = to . gclose c b . from
    {-# INLINE close #-}
  
    -- | Replace bound names by free names.
    open :: AlphaCtx -> NthPatFind -> a -> a
    default open :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NthPatFind -> a -> a
    open c b = to . gopen c b . from
    {-# INLINE open #-}
  
    -- | @isPat x@ dynamically checks whether @x@ can be used as a valid pattern.
    isPat :: a -> DisjointSet AnyName
    default isPat :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName
    isPat = gisPat . from
    {-# INLINE isPat #-}
  
    -- | @isPat x@ dynamically checks whether @x@ can be used as a valid term.
    isTerm :: a -> All
    default isTerm :: (Generic a, GAlpha (Rep a)) => a -> All
    isTerm = gisTerm . from
    {-# INLINE isTerm #-}
  
    -- | @isEmbed@ is needed internally for the implementation of
    --   'isPat'.  @isEmbed@ is true for terms wrapped in 'Embed' and zero
    --   or more occurrences of 'Shift'.  The default implementation
    --   simply returns @False@.
    isEmbed :: a -> Bool
    isEmbed _ = False
    {-# INLINE isEmbed #-}
  
    -- | If @a@ is a pattern, finds the @n@th name in the pattern
    -- (starting from zero), returning the number of names encountered
    -- if not found.
    nthPatFind :: a -> NthPatFind
    default nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind
    nthPatFind = gnthPatFind . from
    {-# INLINE nthPatFind #-}
  
    -- | If @a@ is a pattern, find the index of the given name in the pattern.
    namePatFind :: a -> NamePatFind
    default namePatFind :: (Generic a, GAlpha (Rep a)) => a -> NamePatFind
    namePatFind = gnamePatFind . from
    {-# INLINE namePatFind #-}
  
    -- | See 'Unbound.Generics.LocallyNameless.Operations.swaps'. Apply
    -- the given permutation of variable names to the given pattern.
    swaps' :: AlphaCtx -> Perm AnyName -> a -> a
    default swaps' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a
    swaps' ctx perm = to . gswaps ctx perm . from
    {-# INLINE swaps' #-}
  
    -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.
    lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
    default lfreshen' :: (LFresh m, Generic a, GAlpha (Rep a))
                         => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
    lfreshen' ctx m cont = glfreshen ctx (from m) (cont . to)
    {-# INLINE lfreshen' #-}
  
    -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.  Rename the free variables
    -- in the given term to be distinct from all other names seen in the monad @m@.
    freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
    default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
    freshen' ctx = retractFFM . liftM (first to) . gfreshen ctx . from
  
    -- | See 'Unbound.Generics.LocallyNameless.Operations.acompare'. An alpha-respecting total order on terms involving binders.
    acompare' :: AlphaCtx -> a -> a -> Ordering
    default acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering
    acompare' c = (gacompare c) `on` from
  
  -- Internal: the free monad over the Functor f.  Note that 'freshen''
  -- has a monadic return type and moreover we have to thread the
  -- permutation through the 'gfreshen' calls to crawl over the value
  -- constructors.  Since we don't know anything about the monad @m@,
  -- GHC can't help us.  But note that none of the code in the generic
  -- 'gfreshen' instances actually makes use of the 'Fresh.fresh'
  -- function; they just plumb the dictionary through to any 'K' nodes
  -- that happen to contain a value of a type like 'Name' that does
  -- actually freshen something.  So what we do is we actually make
  -- gfreshen work not in the monad @m@, but in the monad @FFM m@ and
  -- then use 'retractFFM' in the default 'Alpha' method to return back
  -- down to @m@.  We don't really make use of the fact that 'FFM'
  -- reassociates the binds of the underlying monad, but it doesn't hurt
  -- anything.  Mostly what we care about is giving the inliner a chance
  -- to eliminate most of the monadic plumbing.
  newtype FFM f a = FFM { runFFM :: forall r . (a -> r) -> (f r -> r) -> r }
  
  instance Functor (FFM f) where
    fmap f (FFM h) = FFM (\r j -> h (r . f) j)
    {-# INLINE fmap #-}
  
  instance Applicative (FFM f) where
    pure x = FFM (\r _j -> r x)
    {-# INLINE pure #-}
    (FFM h) <*> (FFM k) = FFM (\r j -> h (\f -> k (r . f) j) j)
    {-# INLINE (<*>) #-}
  
  instance Monad (FFM f) where
    return = pure
    {-# INLINE return #-}
    (FFM h) >>= f = FFM (\r j -> h (\x -> runFFM (f x) r j) j)
    {-# INLINE (>>=) #-}
  
  instance Fresh m => Fresh (FFM m) where
    fresh = liftFFM . fresh 
    {-# INLINE fresh #-}
  
  liftFFM :: Monad m => m a -> FFM m a
  liftFFM m = FFM (\r j -> j (liftM r m))
  {-# INLINE liftFFM #-}
  
  retractFFM :: Monad m => FFM m a -> m a
  retractFFM (FFM h) = h return j
    where
      j mmf = mmf >>= \mf -> mf
  {-# INLINE retractFFM #-}
  
  -- | The result of @'nthPatFind' a i@ is @Left k@ where @i-k@ is the
  -- number of names in pattern @a@ (with @k < i@) or @Right x@ where @x@
  -- is the @i@th name in @a@
  newtype NthPatFind = NthPatFind { runNthPatFind :: Integer -> Either Integer AnyName }
  
  -- | @since 0.3.2
  instance Sem.Semigroup NthPatFind where
    (<>) = \(NthPatFind f) (NthPatFind g) ->
      NthPatFind $ \i -> case f i of
      Left i' -> g i'
      found@Right {} -> found
  
  instance Monoid NthPatFind where
    mempty = NthPatFind Left
    mappend = (<>)
  
  -- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that
  -- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name
  -- in @a@
  newtype NamePatFind = NamePatFind { runNamePatFind :: AnyName
                                                        -- Left - names skipped over
                                                        -- Right - index of the name we found
                                                        -> Either Integer Integer }
  
  -- | @since 0.3.2
  instance Sem.Semigroup NamePatFind where
    (<>) = \(NamePatFind f) (NamePatFind g) ->
      NamePatFind $ \nm -> case f nm of
      ans@Right {} -> ans
      Left n -> case g nm of
        Left m -> Left $! n + m
        Right i -> Right $! n + i
  
  instance Monoid NamePatFind where
    mempty = NamePatFind (\_ -> Left 0)
    mappend = (<>)
  
  -- | The "Generic" representation version of 'Alpha'
  class GAlpha f where
    gaeq :: AlphaCtx -> f a -> f a -> Bool
  
    gfvAny :: (Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
  
    gclose :: AlphaCtx -> NamePatFind -> f a -> f a
    gopen :: AlphaCtx -> NthPatFind -> f a -> f a
  
    gisPat :: f a -> DisjointSet AnyName
    gisTerm :: f a -> All
  
    gnthPatFind :: f a -> NthPatFind
    gnamePatFind :: f a -> NamePatFind
  
    gswaps :: AlphaCtx -> Perm AnyName -> f a -> f a
    gfreshen :: Fresh m => AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
  
    glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
  
    gacompare :: AlphaCtx -> f a -> f a -> Ordering
  
  instance (Alpha c) => GAlpha (K1 i c) where
    gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2
    {-# INLINE gaeq #-}
  
    gfvAny ctx nfn = fmap K1 . fvAny' ctx nfn . unK1
    {-# INLINE gfvAny #-}
    
    gclose ctx b = K1 . close ctx b . unK1
    {-# INLINE gclose #-}
    gopen ctx b = K1 . open ctx b . unK1
    {-# INLINE gopen #-}
  
    gisPat = isPat . unK1
    {-# INLINE gisPat #-}
    gisTerm = isTerm . unK1
    {-# INLINE gisTerm #-}
  
    gnthPatFind = nthPatFind . unK1
    {-# INLINE gnthPatFind #-}
    gnamePatFind = namePatFind . unK1
    {-# INLINE gnamePatFind #-}
  
    gswaps ctx perm = K1 . swaps' ctx perm . unK1
    {-# INLINE gswaps #-}
    gfreshen ctx = liftM (first K1) . liftFFM . freshen' ctx . unK1
    {-# INLINE gfreshen #-}
  
    glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1)
    {-# INLINE glfreshen #-}
  
    gacompare ctx (K1 c1) (K1 c2) = acompare' ctx c1 c2
  
  instance GAlpha f => GAlpha (M1 i c f) where
    gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2
    {-# INLINE gaeq #-}
  
    gfvAny ctx nfn = fmap M1 . gfvAny ctx nfn . unM1
    {-# INLINE gfvAny #-}
  
    gclose ctx b = M1 . gclose ctx b . unM1
    {-# INLINE gclose #-}
    gopen ctx b = M1 . gopen ctx b . unM1
    {-# INLINE gopen #-}
  
    gisPat = gisPat . unM1
    {-# INLINE gisPat #-}
    gisTerm = gisTerm . unM1
    {-# INLINE gisTerm #-}
  
    gnthPatFind = gnthPatFind . unM1
    {-# INLINE gnthPatFind #-}
    gnamePatFind = gnamePatFind . unM1
    {-# INLINE gnamePatFind #-}
  
    gswaps ctx perm = M1 . gswaps ctx perm . unM1
    {-# INLINE gswaps #-}
    gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1
    {-# INLINE gfreshen #-}
  
    glfreshen ctx (M1 f) cont =
      glfreshen ctx f (cont . M1)
    {-# INLINE glfreshen #-}
  
    gacompare ctx (M1 f1) (M1 f2) = gacompare ctx f1 f2
  
  instance GAlpha U1 where
    gaeq _ctx _ _ = True
    {-# INLINE gaeq #-}
  
    gfvAny _ctx _nfn _ = pure U1
  
    gclose _ctx _b _ = U1
    gopen _ctx _b _ = U1
  
    gisPat _ = mempty
    gisTerm _ = mempty
  
    gnthPatFind _ = mempty
    gnamePatFind _ = mempty
  
    gswaps _ctx _perm _ = U1
    gfreshen _ctx _ = return (U1, mempty)
    {-# INLINE gfreshen #-}
  
    glfreshen _ctx _ cont = cont U1 mempty
  
    gacompare _ctx _ _ = EQ
  
  instance GAlpha V1 where
    gaeq _ctx _ _ = False
    {-# INLINE gaeq #-}
  
    gfvAny _ctx _nfn = pure
  
    gclose _ctx _b _ = undefined
    gopen _ctx _b _ = undefined
  
    gisPat _ = mempty
    gisTerm _ = mempty
  
    gnthPatFind _ = mempty
    gnamePatFind _ = mempty
  
    gswaps _ctx _perm _ = undefined
    gfreshen _ctx _ = return (undefined, mempty)
    {-# INLINE gfreshen #-}
  
    glfreshen _ctx _ cont = cont undefined mempty
  
    gacompare _ctx _ _ = error "LocallyNameless.gacompare: undefined for empty data types"
  
  instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where
    gaeq ctx (f1 :*: g1) (f2 :*: g2) =
      gaeq ctx f1 f2 && gaeq ctx g1 g2
    {-# INLINE gaeq #-}
  
    gfvAny ctx nfn (f :*: g) = (:*:) <$> gfvAny ctx nfn f
                                     <*> gfvAny ctx nfn g
    {-# INLINE gfvAny #-}
  
    gclose ctx b (f :*: g) = gclose ctx b f :*: gclose ctx b g
    {-# INLINE gclose #-}
    gopen ctx b (f :*: g) = gopen ctx b f :*: gopen ctx b g
    {-# INLINE gopen #-}
  
    gisPat (f :*: g) = gisPat f <> gisPat g
    {-# INLINE gisPat #-}
    gisTerm (f :*: g) = gisTerm f <> gisTerm g
    {-# INLINE gisTerm #-}
  
    gnthPatFind (f :*: g) = gnthPatFind f <> gnthPatFind g
    {-# INLINE gnthPatFind #-}
    gnamePatFind (f :*: g) = gnamePatFind f <> gnamePatFind g
    {-# INLINE gnamePatFind #-}
  
    gswaps ctx perm (f :*: g) =
      gswaps ctx perm f :*: gswaps ctx perm g
    {-# INLINE gswaps #-}
  
    gfreshen ctx (f :*: g) = do
      ~(g', perm2) <- gfreshen ctx g
      ~(f', perm1) <- gfreshen ctx (gswaps ctx perm2 f)
      return (f' :*: g', perm1 <> perm2)
    {-# INLINE gfreshen #-}
  
    glfreshen ctx (f :*: g) cont =
      glfreshen ctx g $ \g' perm2 ->
      glfreshen ctx (gswaps ctx perm2 f) $ \f' perm1 ->
      cont (f' :*: g') (perm1 <> perm2)
    {-# INLINE glfreshen #-}
  
    gacompare ctx (f1 :*: g1) (f2 :*: g2) =
      (gacompare ctx f1 f2) <> (gacompare ctx g1 g2)
  
  instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where
    gaeq ctx  (L1 f1) (L1 f2) = gaeq ctx f1 f2
    gaeq ctx  (R1 g1) (R1 g2) = gaeq ctx g1 g2
    gaeq _ctx _       _       = False
    {-# INLINE gaeq #-}
  
    gfvAny ctx nfn (L1 f) = fmap L1 (gfvAny ctx nfn f)
    gfvAny ctx nfn (R1 g) = fmap R1 (gfvAny ctx nfn g)
    {-# INLINE gfvAny #-}
    
    gclose ctx b (L1 f) = L1 (gclose ctx b f)
    gclose ctx b (R1 g) = R1 (gclose ctx b g)
    {-# INLINE gclose #-}
    gopen ctx b (L1 f) = L1 (gopen ctx b f)
    gopen ctx b (R1 g) = R1 (gopen ctx b g)
    {-# INLINE gopen #-}
  
    gisPat (L1 f) = gisPat f
    gisPat (R1 g) = gisPat g
    {-# INLINE gisPat #-}
  
    gisTerm (L1 f) = gisTerm f
    gisTerm (R1 g) = gisTerm g
    {-# INLINE gisTerm #-}
  
    gnthPatFind (L1 f) = gnthPatFind f
    gnthPatFind (R1 g) = gnthPatFind g
    {-# INLINE gnthPatFind #-}
  
    gnamePatFind (L1 f) = gnamePatFind f
    gnamePatFind (R1 g) = gnamePatFind g
    {-# INLINE gnamePatFind #-}
  
    gswaps ctx perm (L1 f) = L1 (gswaps ctx perm f)
    gswaps ctx perm (R1 f) = R1 (gswaps ctx perm f)
    {-# INLINE gswaps #-}
  
    gfreshen ctx (L1 f) = liftM (first L1) (gfreshen ctx f)
    gfreshen ctx (R1 f) = liftM (first R1) (gfreshen ctx f)
    {-# INLINE gfreshen #-}
    
    glfreshen ctx (L1 f) cont =
      glfreshen ctx f (cont . L1)
    glfreshen ctx (R1 g) cont =
      glfreshen ctx g (cont . R1)
    {-# INLINE glfreshen #-}
  
    gacompare _ctx (L1 _) (R1 _)   = LT
    gacompare _ctx (R1 _) (L1 _)   = GT
    gacompare ctx  (L1 f1) (L1 f2) = gacompare ctx f1 f2
    gacompare ctx  (R1 g1) (R1 g2) = gacompare ctx g1 g2
    {-# INLINE gacompare #-}
  
  -- ============================================================
  -- Alpha instances for the usual types
  
  instance Alpha Int where
    aeq' _ctx i j = i == j
  
    fvAny' _ctx _nfn i = pure i
  
    close _ctx _b i = i
    open _ctx _b i = i
  
    isPat _ = mempty
    isTerm _ = mempty
  
    nthPatFind _ = mempty
    namePatFind _ = mempty
  
    swaps' _ctx _p i = i
    freshen' _ctx i = return (i, mempty)
    lfreshen' _ctx i cont = cont i mempty
  
    acompare' _ctx i j = compare i j
  
  instance Alpha Char where
    aeq' _ctx i j = i == j
  
    fvAny' _ctx _nfn i = pure i
  
    close _ctx _b i = i
    open _ctx _b i = i
  
    isPat _ = mempty
    isTerm _ = mempty
  
    nthPatFind _ = mempty
    namePatFind _ = mempty
  
    swaps' _ctx _p i = i
    freshen' _ctx i = return (i, mempty)
    lfreshen' _ctx i cont = cont i mempty
  
    acompare' _ctx i j = compare i j
  
  instance Alpha Integer where
    aeq' _ctx i j = i == j
  
    fvAny' _ctx _nfn i = pure i
  
    close _ctx _b i = i
    open _ctx _b i = i
  
    isPat _ = mempty
    isTerm _ = mempty
  
    nthPatFind _ = mempty
    namePatFind _ = mempty
  
    swaps' _ctx _p i = i
    freshen' _ctx i = return (i, mempty)
    lfreshen' _ctx i cont = cont i mempty
  
    acompare' _ctx i j = compare i j
  
  instance Alpha Float where
    aeq' _ctx i j = i == j
  
    fvAny' _ctx _nfn i = pure i
  
    close _ctx _b i = i
    open _ctx _b i = i
  
    isPat _ = mempty
    isTerm _ = mempty
  
    nthPatFind _ = mempty
    namePatFind _ = mempty
  
    swaps' _ctx _p i = i
    freshen' _ctx i = return (i, mempty)
    lfreshen' _ctx i cont = cont i mempty
  
    acompare' _ctx i j = compare i j
  
  instance Alpha Double where
    aeq' _ctx i j = i == j
  
    fvAny' _ctx _nfn i = pure i
  
    close _ctx _b i = i
    open _ctx _b i = i
  
    isPat _ = mempty
    isTerm _ = mempty
  
    nthPatFind _ = mempty
    namePatFind _ = mempty
  
    swaps' _ctx _p i = i
    freshen' _ctx i = return (i, mempty)
    lfreshen' _ctx i cont = cont i mempty
  
    acompare' _ctx i j = compare i j
  
  instance (Integral n, Alpha n) => Alpha (Ratio n) where
    aeq' _ctx i j = i == j
  
    fvAny' _ctx _nfn i = pure i
  
    close _ctx _b i = i
    open _ctx _b i = i
  
    isPat _ = mempty
    isTerm _ = mempty
  
    nthPatFind _ = mempty
    namePatFind _ = mempty
  
    swaps' _ctx _p i = i
    freshen' _ctx i = return (i, mempty)
    lfreshen' _ctx i cont = cont i mempty
  
    acompare' _ctx i j = compare i j
  
  instance Alpha Bool
  
  instance Alpha a => Alpha (Maybe a)
  instance Alpha a => Alpha [a]
  instance Alpha a => Alpha (NonEmpty a)
  instance Alpha ()
  instance (Alpha a,Alpha b) => Alpha (Either a b)
  instance (Alpha a,Alpha b) => Alpha (a,b)
  instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)
  instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
  instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
     Alpha (a,b,c,d,e)
  
  -- ============================================================
  -- Alpha instances for interesting types
  
  instance Typeable a => Alpha (Name a) where
    aeq' ctx n1 n2 =
      if isTermCtx ctx
      then n1 == n2 -- in terms, better be the same name
      else True     -- in a pattern, names are always equivlent (since
                    -- they're both bound, so they can vary).
  
    fvAny' ctx nfn nm = if isTermCtx ctx && isFreeName nm
                        then contramap AnyName  (nfn (AnyName nm))
                        else pure nm
  
    open ctx b a@(Bn l k) =
      if ctxMode ctx == Term && ctxLevel ctx == l
      then case runNthPatFind b k of
        Right (AnyName nm) -> case gcast nm of
          Just nm' -> nm'
          Nothing -> error "LocallyNameless.open: inconsistent sorts"
        Left _ -> error "LocallyNameless.open : inconsistency - pattern had too few variables"
      else
        a
    open _ctx _ a = a
  
    close ctx b a@(Fn _ _) =
      if isTermCtx ctx
      then case runNamePatFind b (AnyName a) of
        Right k -> Bn (ctxLevel ctx) k
        Left _ -> a
      else a
    close _ctx _ a = a
    
  
    isPat n = if isFreeName n
              then singletonDisjointSet (AnyName n)
              else inconsistentDisjointSet
  
    isTerm _ = mempty
  
    nthPatFind nm = NthPatFind $ \i ->
      if i == 0 then Right (AnyName nm) else Left $! i-1
  
    namePatFind nm1 = NamePatFind $ \(AnyName nm2) ->
      case gcast nm1 of
        Just nm1' -> if nm1' == nm2 then Right 0 else Left 1
        Nothing -> Left 1
  
    swaps' ctx perm nm =
      if isTermCtx ctx
      then case apply perm (AnyName nm) of
        AnyName nm' ->
          case gcast nm' of
            Just nm'' -> nm''
            Nothing -> error "Internal error swaps' on a Name returned permuted name of wrong sort"
      else nm
        
    freshen' ctx nm =
      if not (isTermCtx ctx)
      then do
        nm' <- fresh nm
        return (nm', single (AnyName nm) (AnyName nm'))
      else error "freshen' on a Name in term position"
  
    lfreshen' ctx nm cont =
      if not (isTermCtx ctx)
      then do
        nm' <- lfresh nm
        avoid [AnyName nm'] $ cont nm' $ single (AnyName nm) (AnyName nm')
      else error "lfreshen' on a Name in term position"
  
    acompare' ctx (Fn s1 i1) (Fn s2 i2)
      | isTermCtx ctx = (compare s1 s2) <> (compare i1 i2)
  
    acompare' ctx n1@(Bn i1 j1) n2@(Bn i2 j2)
      | isTermCtx ctx = mconcat [ compare (typeOf n1) (typeOf n2)
                                , compare i1 i2
                                , compare j1 j2
                                ]
  
    acompare' ctx (Fn _ _) (Bn _ _) | isTermCtx ctx = LT
    acompare' ctx (Bn _ _) (Fn _ _) | isTermCtx ctx = GT
  
    acompare' _ _          _                        = EQ
  
  instance Alpha AnyName where
    aeq' ctx x y =
      if x == y
      then True
      else
        -- in a term unequal variables are unequal, in a pattern it's
        -- ok.
        not (isTermCtx ctx)
  
    fvAny' ctx nfn n@(AnyName nm) = if isTermCtx ctx && isFreeName nm
                                    then nfn n
                                    else pure n
  
    isTerm _ = mempty
  
    isPat n@(AnyName nm) = if isFreeName nm
                           then singletonDisjointSet n
                           else inconsistentDisjointSet
  
    swaps' ctx perm n =
      if isTermCtx ctx
      then apply perm n
      else n
  
    freshen' ctx (AnyName nm) =
      if isTermCtx ctx
      then error "LocallyNameless.freshen' on AnyName in Term mode"
      else do
        nm' <- fresh nm
        return (AnyName nm', single (AnyName nm) (AnyName nm'))
  
    lfreshen' ctx (AnyName nm) cont =
      if isTermCtx ctx
      then error "LocallyNameless.lfreshen' on AnyName in Term mode"
      else do
        nm' <- lfresh nm
        avoid [AnyName nm'] $ cont (AnyName nm') $ single (AnyName nm) (AnyName nm')
  
    open ctx b (AnyName nm) = AnyName (open ctx b nm)
  
    close ctx b (AnyName nm) = AnyName (close ctx b nm)
      
    nthPatFind nm = NthPatFind $ \i ->
      if i == 0 then Right nm else Left $! i - 1
  
    namePatFind nmHave = NamePatFind $ \nmWant ->
      if nmHave == nmWant then Right 0 else Left 1
  
    acompare' _ x y | x == y = EQ
  
    acompare' ctx (AnyName n1) (AnyName n2)
      | isTermCtx ctx =
        case compare (typeOf n1) (typeOf n2) of
          EQ -> case gcast n2 of
            Just n2' -> acompare' ctx n1 n2'
            Nothing -> error "LocallyNameless.acompare': Equal type representations, but gcast failed in comparing two AnyName values"
          ord -> ord
  
    acompare' _ _ _ = EQ
  