    {-| EDSL to construct terms without touching De Bruijn indices.

    e.g. given t, u :: Term, Γ ⊢ t, u : A, we can build "λ f. f t u" like this:

    runNames [] $ do
      -- @open@ binds @t@ and @u@ to computations that know how to weaken themselves in
      -- an extended context

      [t,u] <- mapM open [t,u]

      -- @lam@ gives the illusion of HOAS by providing f as a computation.
      -- It also extends the internal context with the name "f", so that
      -- @t@ and @u@ will get weakened in the body.
      -- We apply f with the (<@>) combinator from Agda.TypeChecking.Primitive.

      lam "f" $ \ f -> f <@> t <@> u

    -}
    module Agda.TypeChecking.Names where

    import Control.Monad          ( liftM2, unless )
    import Control.Monad.Except   ( MonadError )
    import Control.Monad.Identity ( Identity, runIdentity )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Reader   ( MonadReader(..), ReaderT, runReaderT )
    import Control.Monad.State    ( MonadState )
    import Control.Monad.Trans    ( MonadTrans, lift )

    import Data.List              ( isSuffixOf )

    import Agda.Syntax.Common hiding (Nat)
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Pretty ()  -- instances only

    import Agda.Utils.Fail (Fail, runFail_)
    import Agda.Utils.List1 ( List1, pattern (:|) )
    import Agda.Utils.Impossible

    newtype NamesT m a = NamesT { forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
    unName :: ReaderT Names m a }
      deriving ( (forall a b. (a -> b) -> NamesT m a -> NamesT m b)
    -> (forall a b. a -> NamesT m b -> NamesT m a)
    -> Functor (NamesT m)
    forall a b. a -> NamesT m b -> NamesT m a
    forall a b. (a -> b) -> NamesT m a -> NamesT m b
    forall (m :: * -> *) a b.
    Functor m =>
    a -> NamesT m b -> NamesT m a
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> NamesT m a -> NamesT m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> NamesT m a -> NamesT m b
    fmap :: forall a b. (a -> b) -> NamesT m a -> NamesT m b
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> NamesT m b -> NamesT m a
    <$ :: forall a b. a -> NamesT m b -> NamesT m a
    Functor
               , Functor (NamesT m)
    Functor (NamesT m) =>
    (forall a. a -> NamesT m a)
    -> (forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b)
    -> (forall a b c.
        (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c)
    -> (forall a b. NamesT m a -> NamesT m b -> NamesT m b)
    -> (forall a b. NamesT m a -> NamesT m b -> NamesT m a)
    -> Applicative (NamesT m)
    forall a. a -> NamesT m a
    forall a b. NamesT m a -> NamesT m b -> NamesT m a
    forall a b. NamesT m a -> NamesT m b -> NamesT m b
    forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
    forall a b c.
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    forall (m :: * -> *). Applicative m => Functor (NamesT m)
    forall (m :: * -> *) a. Applicative m => a -> NamesT m a
    forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m a -> NamesT m b -> NamesT m a
    forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m a -> NamesT m b -> NamesT m b
    forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m (a -> b) -> NamesT m a -> NamesT m b
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
    $cpure :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
    pure :: forall a. a -> NamesT m a
    $c<*> :: forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m (a -> b) -> NamesT m a -> NamesT m b
    <*> :: forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
    $cliftA2 :: forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
    liftA2 :: forall a b c.
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
    $c*> :: forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m a -> NamesT m b -> NamesT m b
    *> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
    $c<* :: forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m a -> NamesT m b -> NamesT m a
    <* :: forall a b. NamesT m a -> NamesT m b -> NamesT m a
    Applicative
               , Applicative (NamesT m)
    Applicative (NamesT m) =>
    (forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b)
    -> (forall a b. NamesT m a -> NamesT m b -> NamesT m b)
    -> (forall a. a -> NamesT m a)
    -> Monad (NamesT m)
    forall a. a -> NamesT m a
    forall a b. NamesT m a -> NamesT m b -> NamesT m b
    forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
    forall (m :: * -> *). Monad m => Applicative (NamesT m)
    forall (m :: * -> *) a. Monad m => a -> NamesT m a
    forall (m :: * -> *) a b.
    Monad m =>
    NamesT m a -> NamesT m b -> NamesT m b
    forall (m :: * -> *) a b.
    Monad m =>
    NamesT m a -> (a -> NamesT m b) -> NamesT m b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall (m :: * -> *) a b.
    Monad m =>
    NamesT m a -> (a -> NamesT m b) -> NamesT m b
    >>= :: forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
    $c>> :: forall (m :: * -> *) a b.
    Monad m =>
    NamesT m a -> NamesT m b -> NamesT m b
    >> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
    $creturn :: forall (m :: * -> *) a. Monad m => a -> NamesT m a
    return :: forall a. a -> NamesT m a
    Monad
               , (forall (m :: * -> *). Monad m => Monad (NamesT m)) =>
    (forall (m :: * -> *) a. Monad m => m a -> NamesT m a)
    -> MonadTrans NamesT
    forall (m :: * -> *). Monad m => Monad (NamesT m)
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    forall (t :: (* -> *) -> * -> *).
    (forall (m :: * -> *). Monad m => Monad (t m)) =>
    (forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
    $clift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    lift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    MonadTrans
               , MonadState s
               , Monad (NamesT m)
    Monad (NamesT m) =>
    (forall a. IO a -> NamesT m a) -> MonadIO (NamesT m)
    forall a. IO a -> NamesT m a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    forall (m :: * -> *). MonadIO m => Monad (NamesT m)
    forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
    $cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
    liftIO :: forall a. IO a -> NamesT m a
    MonadIO
               , Monad (NamesT m)
    Functor (NamesT m)
    Applicative (NamesT m)
    NamesT m PragmaOptions
    NamesT m CommandLineOptions
    (Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
    NamesT m PragmaOptions
    -> NamesT m CommandLineOptions -> HasOptions (NamesT m)
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    m PragmaOptions -> m CommandLineOptions -> HasOptions m
    forall (m :: * -> *). HasOptions m => Monad (NamesT m)
    forall (m :: * -> *). HasOptions m => Functor (NamesT m)
    forall (m :: * -> *). HasOptions m => Applicative (NamesT m)
    forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
    forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
    $cpragmaOptions :: forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
    pragmaOptions :: NamesT m PragmaOptions
    $ccommandLineOptions :: forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
    commandLineOptions :: NamesT m CommandLineOptions
    HasOptions
               , Monad (NamesT m)
    Functor (NamesT m)
    Applicative (NamesT m)
    NamesT m Bool
    NamesT m Verbosity
    NamesT m ProfileOptions
    (Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
    (VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey)
    -> (forall a.
        VerboseKey
        -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a)
    -> (forall a.
        VerboseKey
        -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a)
    -> NamesT m Verbosity
    -> NamesT m ProfileOptions
    -> NamesT m Bool
    -> (forall a. NamesT m a -> NamesT m a)
    -> MonadDebug (NamesT m)
    VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
    forall a.
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
    forall a. NamesT m a -> NamesT m a
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey)
    -> (forall a.
        VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a)
    -> (forall a.
        VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a)
    -> m Verbosity
    -> m ProfileOptions
    -> m Bool
    -> (forall a. m a -> m a)
    -> MonadDebug m
    forall (m :: * -> *). MonadDebug m => Monad (NamesT m)
    forall (m :: * -> *). MonadDebug m => Functor (NamesT m)
    forall (m :: * -> *). MonadDebug m => Applicative (NamesT m)
    forall (m :: * -> *). MonadDebug m => NamesT m Bool
    forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
    forall (m :: * -> *). MonadDebug m => NamesT m ProfileOptions
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
    forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
    $cformatDebugMessage :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
    formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
    $ctraceDebugMessage :: forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
    traceDebugMessage :: forall a.
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
    $cverboseBracket :: forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
    verboseBracket :: forall a.
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
    $cgetVerbosity :: forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
    getVerbosity :: NamesT m Verbosity
    $cgetProfileOptions :: forall (m :: * -> *). MonadDebug m => NamesT m ProfileOptions
    getProfileOptions :: NamesT m ProfileOptions
    $cisDebugPrinting :: forall (m :: * -> *). MonadDebug m => NamesT m Bool
    isDebugPrinting :: NamesT m Bool
    $cnowDebugPrinting :: forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
    nowDebugPrinting :: forall a. NamesT m a -> NamesT m a
    MonadDebug
               , Monad (NamesT m)
    NamesT m TCEnv
    Monad (NamesT m) =>
    NamesT m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a)
    -> MonadTCEnv (NamesT m)
    forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
    forall (m :: * -> *).
    Monad m =>
    m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
    forall (m :: * -> *). MonadTCEnv m => Monad (NamesT m)
    forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
    $caskTC :: forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
    askTC :: NamesT m TCEnv
    $clocalTC :: forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
    localTC :: forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
    MonadTCEnv
               , Monad (NamesT m)
    NamesT m TCState
    Monad (NamesT m) =>
    NamesT m TCState
    -> (TCState -> NamesT m ())
    -> ((TCState -> TCState) -> NamesT m ())
    -> MonadTCState (NamesT m)
    TCState -> NamesT m ()
    (TCState -> TCState) -> NamesT m ()
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (TCState -> m ())
    -> ((TCState -> TCState) -> m ())
    -> MonadTCState m
    forall (m :: * -> *). MonadTCState m => Monad (NamesT m)
    forall (m :: * -> *). MonadTCState m => NamesT m TCState
    forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> NamesT m ()
    $cgetTC :: forall (m :: * -> *). MonadTCState m => NamesT m TCState
    getTC :: NamesT m TCState
    $cputTC :: forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
    putTC :: TCState -> NamesT m ()
    $cmodifyTC :: forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> NamesT m ()
    modifyTC :: (TCState -> TCState) -> NamesT m ()
    MonadTCState
               , Applicative (NamesT m)
    MonadIO (NamesT m)
    HasOptions (NamesT m)
    MonadTCState (NamesT m)
    MonadTCEnv (NamesT m)
    (Applicative (NamesT m), MonadIO (NamesT m), MonadTCEnv (NamesT m),
     MonadTCState (NamesT m), HasOptions (NamesT m)) =>
    (forall a. TCM a -> NamesT m a) -> MonadTCM (NamesT m)
    forall a. TCM a -> NamesT m a
    forall (tcm :: * -> *).
    (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm,
     HasOptions tcm) =>
    (forall a. TCM a -> tcm a) -> MonadTCM tcm
    forall (m :: * -> *). MonadTCM m => Applicative (NamesT m)
    forall (m :: * -> *). MonadTCM m => MonadIO (NamesT m)
    forall (m :: * -> *). MonadTCM m => HasOptions (NamesT m)
    forall (m :: * -> *). MonadTCM m => MonadTCState (NamesT m)
    forall (m :: * -> *). MonadTCM m => MonadTCEnv (NamesT m)
    forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
    $cliftTCM :: forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
    liftTCM :: forall a. TCM a -> NamesT m a
    MonadTCM
               , Monad (NamesT m)
    NamesT m TCState
    Monad (NamesT m) =>
    NamesT m TCState
    -> (forall a b.
        Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b)
    -> (forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a)
    -> ReadTCState (NamesT m)
    forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
    forall a b. Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    forall (m :: * -> *). ReadTCState m => Monad (NamesT m)
    forall (m :: * -> *). ReadTCState m => NamesT m TCState
    forall (m :: * -> *) a.
    ReadTCState m =>
    (TCState -> TCState) -> NamesT m a -> NamesT m a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
    $cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
    getTCState :: NamesT m TCState
    $clocallyTCState :: forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
    locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
    $cwithTCState :: forall (m :: * -> *) a.
    ReadTCState m =>
    (TCState -> TCState) -> NamesT m a -> NamesT m a
    withTCState :: forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
    ReadTCState
               , Applicative (NamesT m)
    HasOptions (NamesT m)
    MonadTCEnv (NamesT m)
    ReadTCState (NamesT m)
    (Applicative (NamesT m), MonadTCEnv (NamesT m),
     ReadTCState (NamesT m), HasOptions (NamesT m)) =>
    (forall a. ReduceM a -> NamesT m a) -> MonadReduce (NamesT m)
    forall a. ReduceM a -> NamesT m a
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
    (forall a. ReduceM a -> m a) -> MonadReduce m
    forall (m :: * -> *). MonadReduce m => Applicative (NamesT m)
    forall (m :: * -> *). MonadReduce m => HasOptions (NamesT m)
    forall (m :: * -> *). MonadReduce m => MonadTCEnv (NamesT m)
    forall (m :: * -> *). MonadReduce m => ReadTCState (NamesT m)
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
    $cliftReduce :: forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
    liftReduce :: forall a. ReduceM a -> NamesT m a
    MonadReduce
               , MonadError e
               , MonadTCEnv (NamesT m)
    MonadTCEnv (NamesT m) =>
    (forall a. Name -> Dom Type -> NamesT m a -> NamesT m a)
    -> (forall a.
        Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
    -> (forall a.
        Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
    -> (forall a.
        Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a)
    -> MonadAddContext (NamesT m)
    forall a. Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
    forall a.
    Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
    forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
    forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
    forall (m :: * -> *).
    MonadTCEnv m =>
    (forall a. Name -> Dom Type -> m a -> m a)
    -> (forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a)
    -> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
    -> (forall a. Range -> VerboseKey -> (Name -> m a) -> m a)
    -> MonadAddContext m
    forall (m :: * -> *). MonadAddContext m => MonadTCEnv (NamesT m)
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> NamesT m a -> NamesT m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
    $caddCtx :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> NamesT m a -> NamesT m a
    addCtx :: forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
    $caddLetBinding' :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
    addLetBinding' :: forall a.
    Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
    $cupdateContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
    updateContext :: forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
    $cwithFreshName :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
    withFreshName :: forall a. Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
    MonadAddContext
               , Monad (NamesT m)
    Functor (NamesT m)
    Applicative (NamesT m)
    (Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
    (SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun)))
    -> HasBuiltins (NamesT m)
    SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
    forall (m :: * -> *). HasBuiltins m => Monad (NamesT m)
    forall (m :: * -> *). HasBuiltins m => Functor (NamesT m)
    forall (m :: * -> *). HasBuiltins m => Applicative (NamesT m)
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
    $cgetBuiltinThing :: forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
    getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
    HasBuiltins
               , Functor (NamesT m)
    Applicative (NamesT m)
    HasOptions (NamesT m)
    MonadTCEnv (NamesT m)
    MonadDebug (NamesT m)
    (Functor (NamesT m), Applicative (NamesT m), HasOptions (NamesT m),
     MonadDebug (NamesT m), MonadTCEnv (NamesT m)) =>
    (QName -> NamesT m Definition)
    -> (QName -> NamesT m (Either SigError Definition))
    -> (QName -> NamesT m RewriteRules)
    -> HasConstInfo (NamesT m)
    QName -> NamesT m RewriteRules
    QName -> NamesT m (Either SigError Definition)
    QName -> NamesT m Definition
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadDebug m,
     MonadTCEnv m) =>
    (QName -> m Definition)
    -> (QName -> m (Either SigError Definition))
    -> (QName -> m RewriteRules)
    -> HasConstInfo m
    forall (m :: * -> *). HasConstInfo m => Functor (NamesT m)
    forall (m :: * -> *). HasConstInfo m => Applicative (NamesT m)
    forall (m :: * -> *). HasConstInfo m => HasOptions (NamesT m)
    forall (m :: * -> *). HasConstInfo m => MonadTCEnv (NamesT m)
    forall (m :: * -> *). HasConstInfo m => MonadDebug (NamesT m)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m RewriteRules
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m Definition
    $cgetConstInfo :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m Definition
    getConstInfo :: QName -> NamesT m Definition
    $cgetConstInfo' :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m (Either SigError Definition)
    getConstInfo' :: QName -> NamesT m (Either SigError Definition)
    $cgetRewriteRulesFor :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m RewriteRules
    getRewriteRulesFor :: QName -> NamesT m RewriteRules
    HasConstInfo
               , MonadTCEnv (NamesT m)
    MonadReduce (NamesT m)
    ReadTCState (NamesT m)
    HasBuiltins (NamesT m)
    MonadAddContext (NamesT m)
    MonadDebug (NamesT m)
    HasConstInfo (NamesT m)
    (HasBuiltins (NamesT m), HasConstInfo (NamesT m),
     MonadAddContext (NamesT m), MonadDebug (NamesT m),
     MonadReduce (NamesT m), MonadTCEnv (NamesT m),
     ReadTCState (NamesT m)) =>
    PureTCM (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadTCEnv (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadReduce (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    ReadTCState (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    HasBuiltins (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadAddContext (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadDebug (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    HasConstInfo (NamesT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
     MonadReduce m, MonadTCEnv m, ReadTCState m) =>
    PureTCM m
    PureTCM
               )

    -- | A list of variable names from a context.
    type Names = [String]

    runNamesT :: Names -> NamesT m a -> m a
    runNamesT :: forall (m :: * -> *) a. Names -> NamesT m a -> m a
    runNamesT Names
    n NamesT m a
    m = ReaderT Names m a -> Names -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (NamesT m a -> ReaderT Names m a
    forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
    unName NamesT m a
    m) Names
    n

    runNames :: Names -> NamesT Identity a -> a
    runNames :: forall a. Names -> NamesT Identity a -> a
    runNames Names
    n NamesT Identity a
    m = Identity a -> a
    forall a. Identity a -> a
    runIdentity (Names -> NamesT Identity a -> Identity a
    forall (m :: * -> *) a. Names -> NamesT m a -> m a
    runNamesT Names
    n NamesT Identity a
    m)

    currentCxt :: Monad m => NamesT m Names
    currentCxt :: forall (m :: * -> *). Monad m => NamesT m Names
    currentCxt = ReaderT Names m Names -> NamesT m Names
    forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
    NamesT ReaderT Names m Names
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    {-# INLINABLE cxtSubst #-}
    -- | @cxtSubst Γ@ returns the substitution needed to go
    --   from Γ to the current context.
    --
    --   Precondition @Γ@ is not a subcontext of the current one.
    cxtSubst :: Monad m => Names -> NamesT m (Substitution' a)
    cxtSubst :: forall (m :: * -> *) a.
    Monad m =>
    Names -> NamesT m (Substitution' a)
    cxtSubst Names
    ctx = do
      ctx' <- NamesT m Names
    forall (m :: * -> *). Monad m => NamesT m Names
    currentCxt
      if (ctx `isSuffixOf` ctx')
         then return $ raiseS (length ctx' - length ctx)
         else
          -- trace ("out of context (" ++ show ctx ++ " is not a sub context of " ++ show ctx' ++ ")")
           __IMPOSSIBLE__

    {-# INLINABLE inCxt #-}
    -- | @inCxt Γ t@ takes a @t@ in context @Γ@ and produce an action that
    --   will return @t@ weakened to the current context.
    --
    --   Fails whenever @cxtSubst Γ@ would.
    inCxt :: (Monad m, Subst a) => Names -> a -> NamesT m a
    inCxt :: forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    Names -> a -> NamesT m a
    inCxt Names
    ctx a
    a = do
      sigma <- Names -> NamesT m (Substitution' (SubstArg a))
    forall (m :: * -> *) a.
    Monad m =>
    Names -> NamesT m (Substitution' a)
    cxtSubst Names
    ctx
      return $ applySubst sigma a

    -- | Closed terms
    cl' :: Applicative m => a -> NamesT m a
    cl' :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
    cl' = a -> NamesT m a
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    cl :: Monad m => m a -> NamesT m a
    cl :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl = m a -> NamesT m a
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    {-# INLINABLE open #-}
    -- | Open terms in the current context.
    open :: (Monad m, Subst a) => a -> NamesT m (NamesT m a)
    open :: forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open a
    a = do
      ctx <- ReaderT Names m Names -> NamesT m Names
    forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
    NamesT ReaderT Names m Names
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      pure $ inCxt ctx a

    -- | Monadic actions standing for variables.
    --
    --   @b@ is quantified over so the same variable can be used e.g. both
    --   as a pattern and as an expression.
    type Var m = forall b. (Subst b, DeBruijn b) => NamesT m b

    {-# INLINE bind #-}
    -- | @bind n f@ provides @f@ with a fresh variable, which can be used in any extended context.
    --
    --   Returns an @Abs@ which binds the extra variable.
    bind :: Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a)
    bind :: forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind VerboseKey
    n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
    f = VerboseKey -> a -> Abs a
    forall a. VerboseKey -> a -> Abs a
    Abs VerboseKey
    n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m a
    forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m a
    bind' VerboseKey
    n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
    f

    {-# INLINABLE bind' #-}
    -- | Like @bind@ but returns a bare term.
    bind' :: Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a
    bind' :: forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m a
    bind' VerboseKey
    n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
    f = do
      cxt <- ReaderT Names m Names -> NamesT m Names
    forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
    NamesT ReaderT Names m Names
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      (NamesT . local (n:) . unName $ f (inCxt (n:cxt) (deBruijnVar 0)))

    -- * Helpers to build lambda abstractions.

    glam :: Monad m
         => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam :: forall (m :: * -> *).
    Monad m =>
    ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam ArgInfo
    info VerboseKey
    n NamesT m Term -> NamesT m Term
    f = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    info (Abs Term -> Term) -> NamesT m (Abs Term) -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
        -> NamesT m Term)
    -> NamesT m (Abs Term)
    forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind VerboseKey
    n (\ forall b. (Subst b, DeBruijn b) => NamesT m b
    x -> NamesT m Term -> NamesT m Term
    f NamesT m Term
    forall b. (Subst b, DeBruijn b) => NamesT m b
    x)

    lam :: Monad m
        => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam :: forall (m :: * -> *).
    Monad m =>
    VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam VerboseKey
    n NamesT m Term -> NamesT m Term
    f = ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam ArgInfo
    defaultArgInfo VerboseKey
    n NamesT m Term -> NamesT m Term
    f

    ilam :: Monad m
        => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam :: forall (m :: * -> *).
    Monad m =>
    VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam VerboseKey
    n NamesT m Term -> NamesT m Term
    f = ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam ArgInfo
    defaultIrrelevantArgInfo VerboseKey
    n NamesT m Term -> NamesT m Term
    f

    -- * Combinators for n-ary binders.

    data AbsN a = AbsN { forall a. AbsN a -> Names
    absNName :: [ArgName], forall a. AbsN a -> a
    unAbsN :: a } deriving ((forall a b. (a -> b) -> AbsN a -> AbsN b)
    -> (forall a b. a -> AbsN b -> AbsN a) -> Functor AbsN
    forall a b. a -> AbsN b -> AbsN a
    forall a b. (a -> b) -> AbsN a -> AbsN b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> AbsN a -> AbsN b
    fmap :: forall a b. (a -> b) -> AbsN a -> AbsN b
    $c<$ :: forall a b. a -> AbsN b -> AbsN a
    <$ :: forall a b. a -> AbsN b -> AbsN a
    Functor,(forall m. Monoid m => AbsN m -> m)
    -> (forall m a. Monoid m => (a -> m) -> AbsN a -> m)
    -> (forall m a. Monoid m => (a -> m) -> AbsN a -> m)
    -> (forall a b. (a -> b -> b) -> b -> AbsN a -> b)
    -> (forall a b. (a -> b -> b) -> b -> AbsN a -> b)
    -> (forall b a. (b -> a -> b) -> b -> AbsN a -> b)
    -> (forall b a. (b -> a -> b) -> b -> AbsN a -> b)
    -> (forall a. (a -> a -> a) -> AbsN a -> a)
    -> (forall a. (a -> a -> a) -> AbsN a -> a)
    -> (forall a. AbsN a -> [a])
    -> (forall a. AbsN a -> Bool)
    -> (forall a. AbsN a -> VerboseLevel)
    -> (forall a. Eq a => a -> AbsN a -> Bool)
    -> (forall a. Ord a => AbsN a -> a)
    -> (forall a. Ord a => AbsN a -> a)
    -> (forall a. Num a => AbsN a -> a)
    -> (forall a. Num a => AbsN a -> a)
    -> Foldable AbsN
    forall a. Eq a => a -> AbsN a -> Bool
    forall a. Num a => AbsN a -> a
    forall a. Ord a => AbsN a -> a
    forall m. Monoid m => AbsN m -> m
    forall a. AbsN a -> Bool
    forall a. AbsN a -> VerboseLevel
    forall a. AbsN a -> [a]
    forall a. (a -> a -> a) -> AbsN a -> a
    forall m a. Monoid m => (a -> m) -> AbsN a -> m
    forall b a. (b -> a -> b) -> b -> AbsN a -> b
    forall a b. (a -> b -> b) -> b -> AbsN a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> VerboseLevel)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => AbsN m -> m
    fold :: forall m. Monoid m => AbsN m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> AbsN a -> a
    foldr1 :: forall a. (a -> a -> a) -> AbsN a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> AbsN a -> a
    foldl1 :: forall a. (a -> a -> a) -> AbsN a -> a
    $ctoList :: forall a. AbsN a -> [a]
    toList :: forall a. AbsN a -> [a]
    $cnull :: forall a. AbsN a -> Bool
    null :: forall a. AbsN a -> Bool
    $clength :: forall a. AbsN a -> VerboseLevel
    length :: forall a. AbsN a -> VerboseLevel
    $celem :: forall a. Eq a => a -> AbsN a -> Bool
    elem :: forall a. Eq a => a -> AbsN a -> Bool
    $cmaximum :: forall a. Ord a => AbsN a -> a
    maximum :: forall a. Ord a => AbsN a -> a
    $cminimum :: forall a. Ord a => AbsN a -> a
    minimum :: forall a. Ord a => AbsN a -> a
    $csum :: forall a. Num a => AbsN a -> a
    sum :: forall a. Num a => AbsN a -> a
    $cproduct :: forall a. Num a => AbsN a -> a
    product :: forall a. Num a => AbsN a -> a
    Foldable,Functor AbsN
    Foldable AbsN
    (Functor AbsN, Foldable AbsN) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> AbsN a -> f (AbsN b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        AbsN (f a) -> f (AbsN a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> AbsN a -> m (AbsN b))
    -> (forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a))
    -> Traversable AbsN
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a)
    forall (f :: * -> *) a. Applicative f => AbsN (f a) -> f (AbsN a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AbsN a -> m (AbsN b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AbsN a -> f (AbsN b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AbsN a -> f (AbsN b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AbsN a -> f (AbsN b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => AbsN (f a) -> f (AbsN a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => AbsN (f a) -> f (AbsN a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AbsN a -> m (AbsN b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AbsN a -> m (AbsN b)
    $csequence :: forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a)
    sequence :: forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a)
    Traversable)

    instance Subst a => Subst (AbsN a) where
      type SubstArg (AbsN a) = SubstArg a
      applySubst :: Substitution' (SubstArg (AbsN a)) -> AbsN a -> AbsN a
    applySubst Substitution' (SubstArg (AbsN a))
    rho (AbsN Names
    xs a
    a) = Names -> a -> AbsN a
    forall a. Names -> a -> AbsN a
    AbsN Names
    xs (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (VerboseLevel
    -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a. VerboseLevel -> Substitution' a -> Substitution' a
    liftS (Names -> VerboseLevel
    forall a. [a] -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length Names
    xs) Substitution' (SubstArg a)
    Substitution' (SubstArg (AbsN a))
    rho) a
    a)

    -- | Will crash on @NoAbs@
    toAbsN :: Abs (AbsN a) -> AbsN a
    toAbsN :: forall a. Abs (AbsN a) -> AbsN a
    toAbsN (Abs VerboseKey
    n AbsN a
    x') = Names -> a -> AbsN a
    forall a. Names -> a -> AbsN a
    AbsN (VerboseKey
    n VerboseKey -> Names -> Names
    forall a. a -> [a] -> [a]
    : AbsN a -> Names
    forall a. AbsN a -> Names
    absNName AbsN a
    x') (AbsN a -> a
    forall a. AbsN a -> a
    unAbsN AbsN a
    x')
    toAbsN NoAbs{}    = AbsN a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# INLINABLE absAppN #-}
    absAppN :: Subst a => AbsN a -> [SubstArg a] -> a
    absAppN :: forall a. Subst a => AbsN a -> [SubstArg a] -> a
    absAppN AbsN a
    f [SubstArg a]
    xs = [SubstArg a] -> Substitution' (SubstArg a)
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([SubstArg a] -> [SubstArg a]
    forall a. [a] -> [a]
    reverse [SubstArg a]
    xs) Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` AbsN a -> a
    forall a. AbsN a -> a
    unAbsN AbsN a
    f

    type ArgVars m = (forall b. (Subst b, DeBruijn b) => [NamesT m (Arg b)])

    type Vars m = (forall b. (Subst b, DeBruijn b) => [NamesT m b])

    {-# INLINABLE bindN #-}
    bindN :: ( Monad m
            ) =>
            [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
    bindN :: forall (m :: * -> *) a.
    Monad m =>
    Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
    bindN [] Vars m -> NamesT m a
    f = Names -> a -> AbsN a
    forall a. Names -> a -> AbsN a
    AbsN [] (a -> AbsN a) -> NamesT m a -> NamesT m (AbsN a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Vars m -> NamesT m a
    f []
    bindN (VerboseKey
    x:Names
    xs) Vars m -> NamesT m a
    f = Abs (AbsN a) -> AbsN a
    forall a. Abs (AbsN a) -> AbsN a
    toAbsN (Abs (AbsN a) -> AbsN a)
    -> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
        -> NamesT m (AbsN a))
    -> NamesT m (Abs (AbsN a))
    forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind VerboseKey
    x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
    x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
    forall (m :: * -> *) a.
    Monad m =>
    Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
    bindN Names
    xs (\ Vars m
    xs -> Vars m -> NamesT m a
    f (NamesT m b
    forall b. (Subst b, DeBruijn b) => NamesT m b
    xNamesT m b -> [NamesT m b] -> [NamesT m b]
    forall a. a -> [a] -> [a]
    :[NamesT m b]
    Vars m
    xs)))

    {-# INLINABLE bindNArg #-}
    bindNArg :: ( Monad m
            ) =>
            [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
    bindNArg :: forall (m :: * -> *) a.
    Monad m =>
    [Arg VerboseKey] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
    bindNArg [] ArgVars m -> NamesT m a
    f = Names -> a -> AbsN a
    forall a. Names -> a -> AbsN a
    AbsN [] (a -> AbsN a) -> NamesT m a -> NamesT m (AbsN a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgVars m -> NamesT m a
    f []
    bindNArg (Arg ArgInfo
    i VerboseKey
    x:[Arg VerboseKey]
    xs) ArgVars m -> NamesT m a
    f = Abs (AbsN a) -> AbsN a
    forall a. Abs (AbsN a) -> AbsN a
    toAbsN (Abs (AbsN a) -> AbsN a)
    -> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
        -> NamesT m (AbsN a))
    -> NamesT m (Abs (AbsN a))
    forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind VerboseKey
    x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
    x -> [Arg VerboseKey] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
    forall (m :: * -> *) a.
    Monad m =>
    [Arg VerboseKey] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
    bindNArg [Arg VerboseKey]
    xs (\ ArgVars m
    xs -> ArgVars m -> NamesT m a
    f ((ArgInfo -> b -> Arg b
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (b -> Arg b) -> NamesT m b -> NamesT m (Arg b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT m b
    forall b. (Subst b, DeBruijn b) => NamesT m b
    x)NamesT m (Arg b) -> [NamesT m (Arg b)] -> [NamesT m (Arg b)]
    forall a. a -> [a] -> [a]
    :[NamesT m (Arg b)]
    ArgVars m
    xs)))

    type Vars1 m = (forall b. (Subst b, DeBruijn b) => List1 (NamesT m b))

    bindN1 :: Monad m
      => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
    bindN1 :: forall (m :: * -> *) a.
    Monad m =>
    List1 VerboseKey -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
    bindN1 (VerboseKey
    x :| Names
    xs) Vars1 m -> NamesT m a
    f = Abs (AbsN a) -> AbsN a
    forall a. Abs (AbsN a) -> AbsN a
    toAbsN (Abs (AbsN a) -> AbsN a)
    -> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
        -> NamesT m (AbsN a))
    -> NamesT m (Abs (AbsN a))
    forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind VerboseKey
    x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
    x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
    forall (m :: * -> *) a.
    Monad m =>
    Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
    bindN Names
    xs (\ Vars m
    xs -> Vars1 m -> NamesT m a
    f (NamesT m b
    forall b. (Subst b, DeBruijn b) => NamesT m b
    x NamesT m b -> [NamesT m b] -> NonEmpty (NamesT m b)
    forall a. a -> [a] -> NonEmpty a
    :| [NamesT m b]
    Vars m
    xs)))

    glamN :: (Functor m, Monad m) =>
             [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    glamN :: forall (m :: * -> *).
    (Functor m, Monad m) =>
    [Arg VerboseKey]
    -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    glamN [] NamesT m Args -> NamesT m Term
    f = NamesT m Args -> NamesT m Term
    f (NamesT m Args -> NamesT m Term) -> NamesT m Args -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ Args -> NamesT m Args
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
    glamN (Arg ArgInfo
    i VerboseKey
    n:[Arg VerboseKey]
    ns) NamesT m Args -> NamesT m Term
    f = ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    ArgInfo
    -> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam ArgInfo
    i VerboseKey
    n ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT m Term
    x -> [Arg VerboseKey]
    -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    (Functor m, Monad m) =>
    [Arg VerboseKey]
    -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    glamN [Arg VerboseKey]
    ns (\ NamesT m Args
    xs -> NamesT m Args -> NamesT m Term
    f ((:) (Arg Term -> Args -> Args)
    -> NamesT m (Arg Term) -> NamesT m (Args -> Args)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Term -> Arg Term) -> NamesT m Term -> NamesT m (Arg Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT m Term
    x) NamesT m (Args -> Args) -> NamesT m Args -> NamesT m Args
    forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT m Args
    xs))

    applyN :: ( Monad m
            , Subst a
            ) =>
            NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
    applyN :: forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
    applyN NamesT m (AbsN a)
    f [NamesT m (SubstArg a)]
    xs = do
      f <- NamesT m (AbsN a)
    f
      xs <- sequence xs
      unless (length xs == length (absNName f)) $ __IMPOSSIBLE__
      return $ absAppN f xs

    {-# INLINABLE applyN' #-}
    applyN' :: ( Monad m
            , Subst a
            ) =>
            NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a
    applyN' :: forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a
    applyN' NamesT m (AbsN a)
    f NamesT m [SubstArg a]
    xs = do
      f <- NamesT m (AbsN a)
    f
      xs <- xs
      unless (length xs == length (absNName f)) $ __IMPOSSIBLE__
      return $ absAppN f xs

    {-# INLINABLE abstractN #-}
    abstractN :: ( Monad m
                 , Abstract a
                 ) =>
                 NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
    abstractN :: forall (m :: * -> *) a.
    (Monad m, Abstract a) =>
    NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
    abstractN NamesT m Telescope
    tel Vars m -> NamesT m a
    f = do
      tel <- NamesT m Telescope
    tel
      u <- bindN (teleNames tel) f
      return $ abstract tel $ unAbsN u

    {-# INLINABLE abstractT #-}
    abstractT :: ( Monad m
                 , Abstract a
                 ) =>
                 String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
    abstractT :: forall (m :: * -> *) a.
    (Monad m, Abstract a) =>
    VerboseKey -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
    abstractT VerboseKey
    n NamesT m Type
    ty Var m -> NamesT m a
    f = do
      u <- VerboseKey -> (Var m -> NamesT m a) -> NamesT m (Abs a)
    forall (m :: * -> *) a.
    Monad m =>
    VerboseKey
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind VerboseKey
    n Var m -> NamesT m a
    f
      ty <- ty
      let tel = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    ty) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Telescope -> Abs Telescope
    forall a. VerboseKey -> a -> Abs a
    Abs VerboseKey
    n Telescope
    forall a. Tele a
    EmptyTel
      return $ abstract tel $ unAbs u

    lamTel :: Monad m => NamesT m (Abs [Term]) -> NamesT m ([Term])
    lamTel :: forall (m :: * -> *).
    Monad m =>
    NamesT m (Abs [Term]) -> NamesT m [Term]
    lamTel NamesT m (Abs [Term])
    t = (Abs Term -> Term) -> [Abs Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo) ([Abs Term] -> [Term])
    -> (Abs [Term] -> [Abs Term]) -> Abs [Term] -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs [Term] -> [Abs Term]
    forall (t :: * -> *) (f :: * -> *) a.
    (Traversable t, Applicative f) =>
    t (f a) -> f (t a)
    forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
    sequenceA (Abs [Term] -> [Term]) -> NamesT m (Abs [Term]) -> NamesT m [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT m (Abs [Term])
    t

    appTel :: Monad m => NamesT m [Term] -> NamesT m Term -> NamesT m [Term]
    appTel :: forall (m :: * -> *).
    Monad m =>
    NamesT m [Term] -> NamesT m Term -> NamesT m [Term]
    appTel = ([Term] -> Term -> [Term])
    -> NamesT m [Term] -> NamesT m Term -> NamesT m [Term]
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (\ [Term]
    fs Term
    x -> (Term -> Term) -> [Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo Term
    x]) [Term]
    fs)