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

    e.g. if 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.
      -- Then we finish the job using the (<@>) combinator from Agda.TypeChecking.Primitive

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

    -}
    module Agda.TypeChecking.Names where

    -- Control.Monad.Fail import is redundant since GHC 8.8.1
    import Control.Monad.Fail (MonadFail)

    import Control.Monad          ( liftM2, unless )
    import Control.Monad.Except   ( MonadError )
    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.Free

    import Agda.Utils.Fail (Fail, runFail_)

    instance HasBuiltins m => HasBuiltins (NamesT m) where
      getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun))
    getBuiltinThing String
    b = m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun))
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun)))
    -> m (Maybe (Builtin PrimFun))
    -> NamesT m (Maybe (Builtin PrimFun))
    forall a b. (a -> b) -> a -> b
    $ String -> m (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    String -> m (Maybe (Builtin PrimFun))
    getBuiltinThing String
    b

    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
    <$ :: forall a b. a -> NamesT m b -> NamesT m a
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> NamesT m b -> NamesT m a
    fmap :: forall a b. (a -> b) -> NamesT m a -> NamesT m b
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> NamesT m a -> NamesT m b
    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
    <* :: forall a b. NamesT m a -> NamesT m b -> NamesT m a
    $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 b
    $c*> :: forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m a -> NamesT m b -> NamesT m b
    liftA2 :: forall a b c.
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
    $cliftA2 :: forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
    <*> :: forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
    $c<*> :: forall (m :: * -> *) a b.
    Applicative m =>
    NamesT m (a -> b) -> NamesT m a -> NamesT m b
    pure :: forall a. a -> NamesT m a
    $cpure :: forall (m :: * -> *) a. Applicative m => a -> 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
    return :: forall a. a -> NamesT m a
    $creturn :: forall (m :: * -> *) a. Monad m => a -> NamesT m a
    >> :: forall a b. NamesT m 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 -> (a -> NamesT m b) -> NamesT m b
    $c>>= :: forall (m :: * -> *) a b.
    Monad m =>
    NamesT m a -> (a -> NamesT m b) -> NamesT m b
    Monad
               , Monad (NamesT m)
    Monad (NamesT m)
    -> (forall a. String -> NamesT m a) -> MonadFail (NamesT m)
    forall a. String -> NamesT m a
    forall (m :: * -> *).
    Monad m -> (forall a. String -> m a) -> MonadFail m
    forall {m :: * -> *}. MonadFail m => Monad (NamesT m)
    forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
    fail :: forall a. String -> NamesT m a
    $cfail :: forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
    MonadFail
               , (forall (m :: * -> *) a. Monad m => m a -> NamesT m a)
    -> MonadTrans NamesT
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    forall (t :: (* -> *) -> * -> *).
    (forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
    lift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    $clift :: 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
    liftIO :: forall a. IO a -> NamesT m a
    $cliftIO :: forall (m :: * -> *) a. MonadIO m => 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
    commandLineOptions :: NamesT m CommandLineOptions
    $ccommandLineOptions :: forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
    pragmaOptions :: NamesT m PragmaOptions
    $cpragmaOptions :: forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
    HasOptions
               , Monad (NamesT m)
    Functor (NamesT m)
    Applicative (NamesT m)
    NamesT m Bool
    NamesT m Verbosity
    Functor (NamesT m)
    -> Applicative (NamesT m)
    -> Monad (NamesT m)
    -> (String -> VerboseLevel -> TCM Doc -> NamesT m String)
    -> (forall a.
        String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
    -> (forall a.
        String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
    -> NamesT m Verbosity
    -> NamesT m Bool
    -> (forall a. NamesT m a -> NamesT m a)
    -> MonadDebug (NamesT m)
    String -> VerboseLevel -> TCM Doc -> NamesT m String
    forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
    forall a. NamesT m a -> NamesT m a
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> Monad m
    -> (String -> VerboseLevel -> TCM Doc -> m String)
    -> (forall a. String -> VerboseLevel -> String -> m a -> m a)
    -> (forall a. String -> VerboseLevel -> String -> m a -> m a)
    -> m Verbosity
    -> 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 =>
    String -> VerboseLevel -> TCM Doc -> NamesT m String
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
    forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
    nowDebugPrinting :: forall a. NamesT m a -> NamesT m a
    $cnowDebugPrinting :: forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
    isDebugPrinting :: NamesT m Bool
    $cisDebugPrinting :: forall (m :: * -> *). MonadDebug m => NamesT m Bool
    getVerbosity :: NamesT m Verbosity
    $cgetVerbosity :: forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
    verboseBracket :: forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
    $cverboseBracket :: forall (m :: * -> *) a.
    MonadDebug m =>
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
    traceDebugMessage :: forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
    $ctraceDebugMessage :: forall (m :: * -> *) a.
    MonadDebug m =>
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
    formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NamesT m String
    $cformatDebugMessage :: forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> TCM Doc -> NamesT m String
    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
    localTC :: forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
    $clocalTC :: forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
    askTC :: NamesT m TCEnv
    $caskTC :: forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
    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 ()
    modifyTC :: (TCState -> TCState) -> NamesT m ()
    $cmodifyTC :: forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> NamesT m ()
    putTC :: TCState -> NamesT m ()
    $cputTC :: forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
    getTC :: NamesT m TCState
    $cgetTC :: forall (m :: * -> *). MonadTCState m => NamesT m TCState
    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
    liftTCM :: forall a. TCM a -> NamesT m a
    $cliftTCM :: forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
    MonadTCM
               , Monad (NamesT m)
    NamesT m TCState
    Monad (NamesT m)
    -> NamesT m TCState
    -> (forall a b.
        Lens' a TCState -> (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' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (forall a b. Lens' a TCState -> (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' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
    withTCState :: forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
    $cwithTCState :: forall (m :: * -> *) a.
    ReadTCState m =>
    (TCState -> TCState) -> NamesT m a -> NamesT m a
    locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
    $clocallyTCState :: forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
    getTCState :: NamesT m TCState
    $cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
    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
    liftReduce :: forall a. ReduceM a -> NamesT m a
    $cliftReduce :: forall (m :: * -> *) a. MonadReduce m => 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. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
    -> (forall a.
        Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
    -> (forall a.
        Range -> String -> (Name -> NamesT m a) -> NamesT m a)
    -> MonadAddContext (NamesT m)
    forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
    forall a. 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. Name -> Term -> Dom Type -> m a -> m a)
    -> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
    -> (forall a. Range -> String -> (Name -> m a) -> m a)
    -> MonadAddContext m
    forall {m :: * -> *}. MonadAddContext m => MonadTCEnv (NamesT m)
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> NamesT m a) -> NamesT m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    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
    withFreshName :: forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
    $cwithFreshName :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> NamesT m a) -> NamesT m a
    updateContext :: forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
    $cupdateContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
    addLetBinding' :: forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
    $caddLetBinding' :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
    addCtx :: forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
    $caddCtx :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> NamesT m a -> NamesT m a
    MonadAddContext
               , Functor (NamesT m)
    MonadFail (NamesT m)
    Applicative (NamesT m)
    MonadDebug (NamesT m)
    HasOptions (NamesT m)
    MonadTCEnv (NamesT m)
    Functor (NamesT m)
    -> Applicative (NamesT m)
    -> MonadFail (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
    -> MonadFail 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 => MonadFail (NamesT m)
    forall {m :: * -> *}. HasConstInfo m => Applicative (NamesT m)
    forall {m :: * -> *}. HasConstInfo m => MonadDebug (NamesT m)
    forall {m :: * -> *}. HasConstInfo m => HasOptions (NamesT m)
    forall {m :: * -> *}. HasConstInfo m => MonadTCEnv (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
    getRewriteRulesFor :: QName -> NamesT m RewriteRules
    $cgetRewriteRulesFor :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m RewriteRules
    getConstInfo' :: QName -> NamesT m (Either SigError Definition)
    $cgetConstInfo' :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m (Either SigError Definition)
    getConstInfo :: QName -> NamesT m Definition
    $cgetConstInfo :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> NamesT m Definition
    HasConstInfo
               , MonadDebug (NamesT m)
    MonadTCEnv (NamesT m)
    MonadReduce (NamesT m)
    ReadTCState (NamesT m)
    MonadAddContext (NamesT m)
    HasBuiltins (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
    -> MonadDebug m
    -> MonadReduce m
    -> MonadTCEnv m
    -> ReadTCState m
    -> PureTCM m
    forall {m :: * -> *}.
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadDebug (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) =>
    MonadAddContext (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) =>
    HasConstInfo (NamesT m)
    PureTCM
               )

    -- deriving instance MonadState s m => MonadState s (NamesT m)

    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

    -- We use @Fail@ instead of @Identity@ because the computation can fail.
    runNames :: Names -> NamesT Fail a -> a
    runNames :: forall a. Names -> NamesT Fail a -> a
    runNames Names
    n NamesT Fail a
    m = Fail a -> a
    forall a. Fail a -> a
    runFail_ (Names -> NamesT Fail a -> Fail a
    forall (m :: * -> *) a. Names -> NamesT m a -> m a
    runNamesT Names
    n NamesT Fail 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

    cxtSubst :: MonadFail m => Names -> NamesT m (Substitution' a)
    cxtSubst :: forall (m :: * -> *) a.
    MonadFail m =>
    Names -> NamesT m (Substitution' a)
    cxtSubst Names
    ctx = do
      Names
    ctx' <- NamesT m Names
    forall (m :: * -> *). Monad m => NamesT m Names
    currentCxt
      if (Names
    ctx Names -> Names -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isSuffixOf` Names
    ctx')
         then Substitution' a -> NamesT m (Substitution' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Substitution' a -> NamesT m (Substitution' a))
    -> Substitution' a -> NamesT m (Substitution' a)
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel -> Substitution' a
    forall a. VerboseLevel -> Substitution' a
    raiseS (Names -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length Names
    ctx' VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    - Names -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length Names
    ctx)
         else String -> NamesT m (Substitution' a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> NamesT m (Substitution' a))
    -> String -> NamesT m (Substitution' a)
    forall a b. (a -> b) -> a -> b
    $ String
    "thing out of context (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Names -> String
    forall a. Show a => a -> String
    show Names
    ctx String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not a sub context of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Names -> String
    forall a. Show a => a -> String
    show Names
    ctx' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    inCxt :: (MonadFail m, Subst a) => Names -> a -> NamesT m a
    inCxt :: forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    Names -> a -> NamesT m a
    inCxt Names
    ctx a
    a = do
      Substitution' (SubstArg a)
    sigma <- Names -> NamesT m (Substitution' (SubstArg a))
    forall (m :: * -> *) a.
    MonadFail m =>
    Names -> NamesT m (Substitution' a)
    cxtSubst Names
    ctx
      a -> NamesT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> NamesT m a) -> a -> NamesT m a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    sigma a
    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 (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 (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    open :: (MonadFail m, Subst a) => a -> NamesT m (NamesT m a)
    open :: forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open a
    a = do
      Names
    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
      NamesT m a -> NamesT m (NamesT m a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NamesT m a -> NamesT m (NamesT m a))
    -> NamesT m a -> NamesT m (NamesT m a)
    forall a b. (a -> b) -> a -> b
    $ Names -> a -> NamesT m a
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    Names -> a -> NamesT m a
    inCxt Names
    ctx a
    a

    bind' :: (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a
    bind' :: forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    String -> (NamesT m b -> NamesT m a) -> NamesT m a
    bind' String
    n NamesT m b -> NamesT m a
    f = do
      Names
    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
      (ReaderT Names m a -> NamesT m a
    forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
    NamesT (ReaderT Names m a -> NamesT m a)
    -> (NamesT m a -> ReaderT Names m a) -> NamesT m a -> NamesT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Names -> Names) -> ReaderT Names m a -> ReaderT Names m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (String
    nString -> Names -> Names
    forall a. a -> [a] -> [a]
    :) (ReaderT Names m a -> ReaderT Names m a)
    -> (NamesT m a -> ReaderT Names m a)
    -> NamesT m a
    -> ReaderT Names m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamesT m a -> ReaderT Names m a
    forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
    unName (NamesT m a -> NamesT m a) -> NamesT m a -> NamesT m a
    forall a b. (a -> b) -> a -> b
    $ NamesT m b -> NamesT m a
    f (Names -> b -> NamesT m b
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    Names -> a -> NamesT m a
    inCxt (String
    nString -> Names -> Names
    forall a. a -> [a] -> [a]
    :Names
    cxt) (VerboseLevel -> b
    forall a. DeBruijn a => VerboseLevel -> a
    deBruijnVar VerboseLevel
    0)))

    bind :: ( MonadFail m
            , Subst b
            , DeBruijn b
            , Subst a
            , Free a
            ) =>
            ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
    bind :: forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    String -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
    bind String
    n NamesT m b -> NamesT m a
    f = String -> a -> Abs a
    forall a. String -> a -> Abs a
    Abs String
    n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> (NamesT m b -> NamesT m a) -> NamesT m a
    forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    String -> (NamesT m b -> NamesT m a) -> NamesT m a
    bind' String
    n NamesT m b -> NamesT m a
    f

    glam :: MonadFail m
         => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam :: forall (m :: * -> *).
    MonadFail m =>
    ArgInfo
    -> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam ArgInfo
    info String
    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
    <$> String -> (NamesT m Term -> NamesT m Term) -> NamesT m (Abs Term)
    forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    String -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
    bind String
    n NamesT m Term -> NamesT m Term
    f

    glamN :: (Functor m, MonadFail m) =>
             [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    glamN :: forall (m :: * -> *).
    (Functor m, MonadFail m) =>
    [Arg String] -> (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 (f :: * -> *) a. Applicative f => a -> f a
    pure []
    glamN (Arg ArgInfo
    i String
    n:[Arg String]
    ns) NamesT m Args -> NamesT m Term
    f = ArgInfo
    -> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgInfo
    -> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam ArgInfo
    i String
    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 String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    (Functor m, MonadFail m) =>
    [Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
    glamN [Arg String]
    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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT m Args
    xs))

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

    ilam :: MonadFail m
        => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam :: forall (m :: * -> *).
    MonadFail m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam String
    n NamesT m Term -> NamesT m Term
    f = ArgInfo
    -> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgInfo
    -> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    glam (Relevance -> ArgInfo -> ArgInfo
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    Irrelevant ArgInfo
    defaultArgInfo) String
    n NamesT m Term -> NamesT m Term
    f