    module Agda.TypeChecking.Monad.Context where

    import Data.Text (Text)
    import qualified Data.Text as T

    import Control.Monad                ( (<=<), forM, when )
    import Control.Monad.Except
    import Control.Monad.Reader
    import Control.Monad.State
    import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )
    import Control.Monad.Trans.Identity ( IdentityT )
    import Control.Monad.Trans.Maybe
    import Control.Monad.Writer         ( WriterT )

    import Data.Foldable
    import qualified Data.List as List
    import qualified Data.Map as Map

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Concrete.Name (NameInScope(..), LensInScope(..), nameRoot, nameToRawName)
    import Agda.Syntax.Internal
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Monad.Open
    import Agda.TypeChecking.Monad.State

    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List ((!!!), downFrom)
    import Agda.Utils.ListT
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Maybe
    import Agda.Utils.Size
    import Agda.Utils.Tuple
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    -- * Modifying the context

    -- | Modify a 'Context' in a computation.  Warning: does not update
    --   the checkpoints. Use @updateContext@ instead.
    {-# INLINE unsafeModifyContext #-}
    unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext Context -> Context
    f = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envContext = f $ envContext e }

    {-# INLINE modifyContextInfo #-}
    -- | Modify the 'Dom' part of context entries.
    modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a
    modifyContextInfo :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (forall e. Dom e -> Dom e) -> tcm a -> tcm a
    modifyContextInfo forall e. Dom e -> Dom e
    f = (Context -> Context) -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext ((Context -> Context) -> tcm a -> tcm a)
    -> (Context -> Context) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ (ContextEntry -> ContextEntry) -> Context -> Context
    forall a b. (a -> b) -> [a] -> [b]
    map ((ContextEntry -> ContextEntry) -> Context -> Context)
    -> (ContextEntry -> ContextEntry) -> Context -> Context
    forall a b. (a -> b) -> a -> b
    $ \case
        (CtxVar Name
    x Dom Type
    a)   -> Name -> Dom Type -> ContextEntry
    CtxVar Name
    x (Dom Type -> Dom Type
    forall e. Dom e -> Dom e
    f Dom Type
    a)

    -- | Change to top (=empty) context. Resets the checkpoints.
    {-# SPECIALIZE inTopContext :: TCM a -> TCM a #-}
    inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a
    inTopContext :: forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext tcm a
    cont =
      (Context -> Context) -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext (Context -> Context -> Context
    forall a b. a -> b -> a
    const [])
            (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv CheckpointId
    -> (CheckpointId -> CheckpointId) -> tcm a -> tcm a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint (CheckpointId -> CheckpointId -> CheckpointId
    forall a b. a -> b -> a
    const CheckpointId
    0)
            (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv (Map CheckpointId (Substitution' Term))
    -> (Map CheckpointId (Substitution' Term)
        -> Map CheckpointId (Substitution' Term))
    -> tcm a
    -> tcm a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map CheckpointId (Substitution' Term))
    eCheckpoints (Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    forall a b. a -> b -> a
    const (Map CheckpointId (Substitution' Term)
     -> Map CheckpointId (Substitution' Term)
     -> Map CheckpointId (Substitution' Term))
    -> Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ CheckpointId
    -> Substitution' Term -> Map CheckpointId (Substitution' Term)
    forall k a. k -> a -> Map k a
    Map.singleton CheckpointId
    0 Substitution' Term
    forall a. Substitution' a
    IdS)
            (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCState (Map ModuleName CheckpointId)
    -> (Map ModuleName CheckpointId -> Map ModuleName CheckpointId)
    -> tcm a
    -> tcm a
    forall a b. Lens' TCState a -> (a -> a) -> tcm b -> tcm b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
    -> TCState -> f TCState
    Lens' TCState (Map ModuleName CheckpointId)
    stModuleCheckpoints (Map ModuleName CheckpointId
    -> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
    forall a b. a -> b -> a
    const Map ModuleName CheckpointId
    forall k a. Map k a
    Map.empty)
            (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' ScopeInfo [(Name, LocalVar)]
    -> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> tcm a -> tcm a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' ScopeInfo a -> (a -> a) -> m b -> m b
    locallyScope ([(Name, LocalVar)] -> f [(Name, LocalVar)])
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo [(Name, LocalVar)]
    scopeLocals ([(Name, LocalVar)] -> [(Name, LocalVar)] -> [(Name, LocalVar)]
    forall a b. a -> b -> a
    const [])
            (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv (Map Name (Open LetBinding))
    -> (Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> tcm a
    -> tcm a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map Name (Open LetBinding))
    eLetBindings (Map Name (Open LetBinding)
    -> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
    forall a b. a -> b -> a
    const Map Name (Open LetBinding)
    forall k a. Map k a
    Map.empty)
            (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ tcm a
    cont

    -- | Change to top (=empty) context, but don't update the checkpoints. Totally
    --   not safe!
    {-# SPECIALIZE unsafeInTopContext :: TCM a -> TCM a #-}
    unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a
    unsafeInTopContext :: forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    unsafeInTopContext m a
    cont =
      Lens' ScopeInfo [(Name, LocalVar)]
    -> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> m a -> m a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' ScopeInfo a -> (a -> a) -> m b -> m b
    locallyScope ([(Name, LocalVar)] -> f [(Name, LocalVar)])
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo [(Name, LocalVar)]
    scopeLocals ([(Name, LocalVar)] -> [(Name, LocalVar)] -> [(Name, LocalVar)]
    forall a b. a -> b -> a
    const []) (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $
        (Context -> Context) -> m a -> m a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext (Context -> Context -> Context
    forall a b. a -> b -> a
    const []) m a
    cont

    -- | Delete the last @n@ bindings from the context.
    --
    --   Doesn't update checkpoints! Use `escapeContext` or `updateContext
    --   rho (drop n)` instead, for an appropriate substitution `rho`.
    {-# SPECIALIZE unsafeEscapeContext :: Int -> TCM a -> TCM a #-}
    unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
    unsafeEscapeContext :: forall (tcm :: * -> *) a. MonadTCM tcm => Nat -> tcm a -> tcm a
    unsafeEscapeContext Nat
    n = (Context -> Context) -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext ((Context -> Context) -> tcm a -> tcm a)
    -> (Context -> Context) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Nat -> Context -> Context
    forall a. Nat -> [a] -> [a]
    drop Nat
    n

    {-# SPECIALIZE escapeContext :: Impossible -> Int -> TCM a -> TCM a #-}
    -- | Delete the last @n@ bindings from the context. Any occurrences of
    -- these variables are replaced with the given @err@.
    escapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a
    escapeContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    err Nat
    n = Substitution' Term -> (Context -> Context) -> m a -> m a
    forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext (Impossible -> Nat -> Substitution' Term
    forall a. Impossible -> Nat -> Substitution' a
    strengthenS Impossible
    err Nat
    n) ((Context -> Context) -> m a -> m a)
    -> (Context -> Context) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Nat -> Context -> Context
    forall a. Nat -> [a] -> [a]
    drop Nat
    n

    -- * Manipulating checkpoints --

    {-# SPECIALIZE checkpoint :: Substitution -> TCM a -> TCM a #-}
    -- | Add a new checkpoint. Do not use directly!
    checkpoint
      :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm)
      => Substitution -> tcm a -> tcm a
    checkpoint :: forall (tcm :: * -> *) a.
    (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
     ReadTCState tcm) =>
    Substitution' Term -> tcm a -> tcm a
    checkpoint Substitution' Term
    sub tcm a
    k = do
      tcm () -> tcm ()
    forall (m :: * -> *). MonadDebug m => m () -> m ()
    unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Nat -> String -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "tc.cxt.checkpoint" Nat
    105 (String -> tcm ()) -> String -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String
    "New checkpoint {"
      old     <- Lens' TCEnv CheckpointId -> tcm CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
      oldMods <- useTC  stModuleCheckpoints
      chkpt <- fresh
      unlessDebugPrinting $ verboseS "tc.cxt.checkpoint" 105 $ do
        cxt <- getContextTelescope
        cps <- viewTC eCheckpoints
        let cps' = CheckpointId
    -> Substitution' Term
    -> Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert CheckpointId
    chkpt Substitution' Term
    forall a. Substitution' a
    IdS (Map CheckpointId (Substitution' Term)
     -> Map CheckpointId (Substitution' Term))
    -> Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ (Substitution' Term -> Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term)
    forall a b. (a -> b) -> Map CheckpointId a -> Map CheckpointId b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg (Substitution' Term))
    -> Substitution' Term -> Substitution' Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Substitution' Term))
    sub) Map CheckpointId (Substitution' Term)
    cps
            prCps Map a a
    cps = [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    vcat [ a -> Doc Aspects
    forall a. Show a => a -> Doc Aspects
    pshow a
    c Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ": " Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    s | (a
    c, a
    s) <- Map a a -> [(a, a)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map a a
    cps ]
        reportSDoc "tc.cxt.checkpoint" 105 $ return $ nest 2 $ vcat
          [ "old =" <+> pshow old
          , "new =" <+> pshow chkpt
          , "sub =" <+> pretty sub
          , "cxt =" <+> pretty cxt
          , "old substs =" <+> prCps cps
          , "new substs =" <?> prCps cps'
          ]
      x <- flip localTC k $ \ TCEnv
    env -> TCEnv
    env
        { envCurrentCheckpoint = chkpt
        , envCheckpoints       = Map.insert chkpt IdS $
                                  fmap (applySubst sub) (envCheckpoints env)
        }
      newMods <- useTC stModuleCheckpoints
      -- Set the checkpoint for introduced modules to the old checkpoint when the
      -- new one goes out of scope. #2897: This isn't actually sound for modules
      -- created under refined parent parameters, but as long as those modules
      -- aren't named we shouldn't look at the checkpoint. The right thing to do
      -- would be to not store these modules in the checkpoint map, but todo..
      stModuleCheckpoints `setTCLens` Map.union oldMods (old <$ newMods)
      unlessDebugPrinting $ reportSLn "tc.cxt.checkpoint" 105 "}"
      return x

    -- | Get the substitution from the context at a given checkpoint to the current context.
    checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution
    checkpointSubstitution :: forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Substitution' Term)
    checkpointSubstitution = tcm (Substitution' Term)
    -> (Substitution' Term -> tcm (Substitution' Term))
    -> Maybe (Substitution' Term)
    -> tcm (Substitution' Term)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe tcm (Substitution' Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Substitution' Term -> tcm (Substitution' Term)
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Substitution' Term) -> tcm (Substitution' Term))
    -> (CheckpointId -> tcm (Maybe (Substitution' Term)))
    -> CheckpointId
    -> tcm (Substitution' Term)
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< CheckpointId -> tcm (Maybe (Substitution' Term))
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Maybe (Substitution' Term))
    checkpointSubstitution'

    -- | Get the substitution from the context at a given checkpoint to the current context.
    checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution)
    checkpointSubstitution' :: forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Maybe (Substitution' Term))
    checkpointSubstitution' CheckpointId
    chkpt = Lens' TCEnv (Maybe (Substitution' Term))
    -> tcm (Maybe (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC ((Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map CheckpointId (Substitution' Term))
    eCheckpoints ((Map CheckpointId (Substitution' Term)
      -> f (Map CheckpointId (Substitution' Term)))
     -> TCEnv -> f TCEnv)
    -> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
        -> Map CheckpointId (Substitution' Term)
        -> f (Map CheckpointId (Substitution' Term)))
    -> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> TCEnv
    -> f TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CheckpointId
    -> Lens'
         (Map CheckpointId (Substitution' Term))
         (Maybe (Substitution' Term))
    forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
    key CheckpointId
    chkpt)

    -- | Get substitution @Γ ⊢ ρ : Γm@ where @Γ@ is the current context
    --   and @Γm@ is the module parameter telescope of module @m@.
    --
    --   Returns @Nothing@ in case the we don't have a checkpoint for @m@.
    getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution)
    getModuleParameterSub :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m (Maybe (Substitution' Term))
    getModuleParameterSub ModuleName
    m = do
      mcp <- (TCState -> Lens' TCState (Maybe CheckpointId) -> Maybe CheckpointId
    forall o i. o -> Lens' o i -> i
    ^. (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
    -> TCState -> f TCState
    Lens' TCState (Map ModuleName CheckpointId)
    stModuleCheckpoints ((Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
     -> TCState -> f TCState)
    -> ((Maybe CheckpointId -> f (Maybe CheckpointId))
        -> Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
    -> (Maybe CheckpointId -> f (Maybe CheckpointId))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName
    -> Lens' (Map ModuleName CheckpointId) (Maybe CheckpointId)
    forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
    key ModuleName
    m) (TCState -> Maybe CheckpointId)
    -> m TCState -> m (Maybe CheckpointId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      traverse checkpointSubstitution mcp

    -- * Adding to the context

    class MonadTCEnv m => MonadAddContext m where
      -- | @addCtx x arg cont@ add a variable to the context.
      --
      --   Chooses an unused 'Name'.
      --
      --   Warning: Does not update module parameter substitution!
      addCtx :: Name -> Dom Type -> m a -> m a

      -- | Add a let bound variable to the context
      addLetBinding' :: Origin -> Name -> Term -> Dom Type -> m a -> m a

      -- | Update the context.
      --   Requires a substitution that transports things living in the old context
      --   to the new.
      updateContext :: Substitution -> (Context -> Context) -> m a -> m a

      withFreshName :: Range -> ArgName -> (Name -> m a) -> m a

      default addCtx
        :: (MonadAddContext n, MonadTransControl t, t n ~ m)
        => Name -> Dom Type -> m a -> m a
      addCtx Name
    x Dom Type
    a = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
    (MonadTransControl t, Monad (t m), Monad m) =>
    (m (StT t a) -> m (StT t b)) -> t m a -> t m b
    liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
    -> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall a b. (a -> b) -> a -> b
    $ Name -> Dom Type -> n (StT t a) -> n (StT t a)
    forall a. Name -> Dom Type -> n a -> n a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    a

      default addLetBinding'
        :: (MonadAddContext n, MonadTransControl t, t n ~ m)
        => Origin -> Name -> Term -> Dom Type -> m a -> m a
      addLetBinding' Origin
    o Name
    x Term
    u Dom Type
    a = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
    (MonadTransControl t, Monad (t m), Monad m) =>
    (m (StT t a) -> m (StT t b)) -> t m a -> t m b
    liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
    -> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall a b. (a -> b) -> a -> b
    $ Origin -> Name -> Term -> Dom Type -> n (StT t a) -> n (StT t a)
    forall a. Origin -> Name -> Term -> Dom Type -> n a -> n a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Origin -> Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' Origin
    o Name
    x Term
    u Dom Type
    a

      default updateContext
        :: (MonadAddContext n, MonadTransControl t, t n ~ m)
        => Substitution -> (Context -> Context) -> m a -> m a
      updateContext Substitution' Term
    sub Context -> Context
    f = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
    (MonadTransControl t, Monad (t m), Monad m) =>
    (m (StT t a) -> m (StT t b)) -> t m a -> t m b
    liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
    -> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall a b. (a -> b) -> a -> b
    $ Substitution' Term
    -> (Context -> Context) -> n (StT t a) -> n (StT t a)
    forall a. Substitution' Term -> (Context -> Context) -> n a -> n a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext Substitution' Term
    sub Context -> Context
    f

      default withFreshName
        :: (MonadAddContext n, MonadTransControl t, t n ~ m)
        => Range -> ArgName -> (Name -> m a) -> m a
      withFreshName Range
    r String
    x Name -> m a
    cont = do
        st <- (Run t -> n (StT t a)) -> t n (StT t a)
    forall (m :: * -> *) a. Monad m => (Run t -> m a) -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTransControl t, Monad m) =>
    (Run t -> m a) -> t m a
    liftWith ((Run t -> n (StT t a)) -> t n (StT t a))
    -> (Run t -> n (StT t a)) -> t n (StT t a)
    forall a b. (a -> b) -> a -> b
    $ \ Run t
    run -> do
          Range -> String -> (Name -> n (StT t a)) -> n (StT t a)
    forall a. Range -> String -> (Name -> n a) -> n a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> m a) -> m a
    withFreshName Range
    r String
    x ((Name -> n (StT t a)) -> n (StT t a))
    -> (Name -> n (StT t a)) -> n (StT t a)
    forall a b. (a -> b) -> a -> b
    $ t n a -> n (StT t a)
    Run t
    run (t n a -> n (StT t a)) -> (Name -> t n a) -> Name -> n (StT t a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> m a
    Name -> t n a
    cont
        restoreT $ return st

    {-# INLINE defaultAddCtx #-}
    -- | Default implementation of addCtx in terms of updateContext
    defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a
    defaultAddCtx :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    defaultAddCtx Name
    x Dom Type
    a m a
    ret =
      Substitution' Term -> (Context -> Context) -> m a -> m a
    forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS Nat
    1) (Name -> Dom Type -> ContextEntry
    CtxVar Name
    x Dom Type
    a ContextEntry -> Context -> Context
    forall a. a -> [a] -> [a]
    :) m a
    ret

    withFreshName_ :: (MonadAddContext m) => ArgName -> (Name -> m a) -> m a
    withFreshName_ :: forall (m :: * -> *) a.
    MonadAddContext m =>
    String -> (Name -> m a) -> m a
    withFreshName_ = Range -> String -> (Name -> m a) -> m a
    forall a. Range -> String -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange

    instance MonadAddContext m => MonadAddContext (ChangeT m)
    instance MonadAddContext m => MonadAddContext (ExceptT e m)
    instance MonadAddContext m => MonadAddContext (IdentityT m)
    instance MonadAddContext m => MonadAddContext (MaybeT m)
    instance MonadAddContext m => MonadAddContext (ReaderT r m)
    instance MonadAddContext m => MonadAddContext (StateT r m)
    instance (Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m)
    deriving instance MonadAddContext m => MonadAddContext (BlockT m)

    instance MonadAddContext m => MonadAddContext (ListT m) where
      addCtx :: forall a. Name -> Dom Type -> ListT m a -> ListT m a
    addCtx Name
    x Dom Type
    a             = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
    -> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ Name -> Dom Type -> m a1 -> m a1
    forall a. Name -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    a
      addLetBinding' :: forall a.
    Origin -> Name -> Term -> Dom Type -> ListT m a -> ListT m a
    addLetBinding' Origin
    o Name
    x Term
    u Dom Type
    a = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
    -> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ Origin -> Name -> Term -> Dom Type -> m a1 -> m a1
    forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Origin -> Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' Origin
    o Name
    x Term
    u Dom Type
    a
      updateContext :: forall a.
    Substitution' Term
    -> (Context -> Context) -> ListT m a -> ListT m a
    updateContext Substitution' Term
    sub Context -> Context
    f    = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
    -> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ Substitution' Term -> (Context -> Context) -> m a1 -> m a1
    forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext Substitution' Term
    sub Context -> Context
    f
      withFreshName :: forall a. Range -> String -> (Name -> ListT m a) -> ListT m a
    withFreshName Range
    r String
    x Name -> ListT m a
    cont = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ Range
    -> String
    -> (Name -> m (Maybe (a, ListT m a)))
    -> m (Maybe (a, ListT m a))
    forall a. Range -> String -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> m a) -> m a
    withFreshName Range
    r String
    x ((Name -> m (Maybe (a, ListT m a))) -> m (Maybe (a, ListT m a)))
    -> (Name -> m (Maybe (a, ListT m a))) -> m (Maybe (a, ListT m a))
    forall a b. (a -> b) -> a -> b
    $ ListT m a -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT (ListT m a -> m (Maybe (a, ListT m a)))
    -> (Name -> ListT m a) -> Name -> m (Maybe (a, ListT m a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> ListT m a
    cont

    -- | Run the given TCM action, and register the given variable as
    --   being shadowed by all the names with the same root that are added
    --   to the context during this TCM action.
    withShadowingNameTCM :: Name -> TCM b -> TCM b
    withShadowingNameTCM :: forall b. Name -> TCM b -> TCM b
    withShadowingNameTCM Name
    x TCM b
    f = do
      String -> Nat -> TCM (Doc Aspects) -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM (Doc Aspects) -> m ()
    reportSDoc String
    "tc.cxt.shadowing" Nat
    80 (TCM (Doc Aspects) -> TCMT IO ())
    -> TCM (Doc Aspects) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM (Doc Aspects)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> TCM (Doc Aspects))
    -> Doc Aspects -> TCM (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "registered" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Name
    x Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "for shadowing"
      Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Name -> NameInScope
    forall a. LensInScope a => a -> NameInScope
    isInScope Name
    x NameInScope -> NameInScope -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameInScope
    InScope) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Name -> TCMT IO ()
    forall {m :: * -> *}. MonadTCState m => Name -> m ()
    tellUsedName Name
    x
      (result , useds) <- TCM b -> TCMT IO (b, Map String (Set1 String))
    forall {m :: * -> *} {a}.
    (ReadTCState m, MonadTCState m) =>
    m a -> m (a, Map String (Set1 String))
    listenUsedNames TCM b
    f
      reportSDoc "tc.cxt.shadowing" 90 $ pure $ "all used names: " <+> text (show useds)
      tellShadowing x useds
      return result

        where
          listenUsedNames :: m a -> m (a, Map String (Set1 String))
    listenUsedNames m a
    f = do
            origUsedNames <- Lens' TCState (Map String (Set1 String))
    -> m (Map String (Set1 String))
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Map String (Set1 String) -> f (Map String (Set1 String)))
    -> TCState -> f TCState
    Lens' TCState (Map String (Set1 String))
    stUsedNames
            setTCLens stUsedNames Map.empty
            result <- f
            newUsedNames <- useTC stUsedNames
            setTCLens stUsedNames $ Map.unionWith (<>) origUsedNames newUsedNames
            return (result , newUsedNames)

          tellUsedName :: Name -> m ()
    tellUsedName Name
    x = do
            let concreteX :: Name
    concreteX = Name -> Name
    nameConcrete Name
    x
                rawX :: String
    rawX      = Name -> String
    nameToRawName Name
    concreteX
                rootX :: String
    rootX     = Name -> String
    nameRoot Name
    concreteX
            Lens' TCState (Maybe (Set1 String))
    -> (Maybe (Set1 String) -> Maybe (Set1 String)) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens ((Map String (Set1 String) -> f (Map String (Set1 String)))
    -> TCState -> f TCState
    Lens' TCState (Map String (Set1 String))
    stUsedNames ((Map String (Set1 String) -> f (Map String (Set1 String)))
     -> TCState -> f TCState)
    -> ((Maybe (Set1 String) -> f (Maybe (Set1 String)))
        -> Map String (Set1 String) -> f (Map String (Set1 String)))
    -> (Maybe (Set1 String) -> f (Maybe (Set1 String)))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Lens' (Map String (Set1 String)) (Maybe (Set1 String))
    forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
    key String
    rootX) ((Maybe (Set1 String) -> Maybe (Set1 String)) -> m ())
    -> (Maybe (Set1 String) -> Maybe (Set1 String)) -> m ()
    forall a b. (a -> b) -> a -> b
    $
              Set1 String -> Maybe (Set1 String)
    forall a. a -> Maybe a
    Just (Set1 String -> Maybe (Set1 String))
    -> (Maybe (Set1 String) -> Set1 String)
    -> Maybe (Set1 String)
    -> Maybe (Set1 String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> Set String -> Set1 String
    forall a. Ord a => a -> Set a -> NESet a
    Set1.insertSet String
    rawX) (Set String -> Set1 String)
    -> (Maybe (Set1 String) -> Set String)
    -> Maybe (Set1 String)
    -> Set1 String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe (Set1 String) -> Set String
    forall a. Maybe (Set1 a) -> Set a
    Set1.toSet'

          tellShadowing :: Name -> Map String (Set1 String) -> m ()
    tellShadowing Name
    x Map String (Set1 String)
    useds = case String -> Map String (Set1 String) -> Maybe (Set1 String)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Name -> String
    nameRoot (Name -> String) -> Name -> String
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    nameConcrete Name
    x) Map String (Set1 String)
    useds of
            Just Set1 String
    shadows -> do
              String -> Nat -> TCM (Doc Aspects) -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM (Doc Aspects) -> m ()
    reportSDoc String
    "tc.cxt.shadowing" Nat
    80 (TCM (Doc Aspects) -> m ()) -> TCM (Doc Aspects) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM (Doc Aspects)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> TCM (Doc Aspects))
    -> Doc Aspects -> TCM (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $
                Doc Aspects
    "names shadowing" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Name
    x Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ": " Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+>
                [Doc Aspects] -> Doc Aspects
    forall a. Pretty a => [a] -> Doc Aspects
    prettyList_ ((String -> Doc Aspects) -> [String] -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty ([String] -> [Doc Aspects]) -> [String] -> [Doc Aspects]
    forall a b. (a -> b) -> a -> b
    $ Set1 String -> [String]
    forall a. NESet a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Set1 String
    shadows)
              Lens' TCState (Map Name (Set1 String))
    -> (Map Name (Set1 String) -> Map Name (Set1 String)) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens (Map Name (Set1 String) -> f (Map Name (Set1 String)))
    -> TCState -> f TCState
    Lens' TCState (Map Name (Set1 String))
    stShadowingNames ((Map Name (Set1 String) -> Map Name (Set1 String)) -> m ())
    -> (Map Name (Set1 String) -> Map Name (Set1 String)) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Set1 String -> Set1 String -> Set1 String)
    -> Name
    -> Set1 String
    -> Map Name (Set1 String)
    -> Map Name (Set1 String)
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Set1 String -> Set1 String -> Set1 String
    forall a. Semigroup a => a -> a -> a
    (<>) Name
    x Set1 String
    shadows
            Maybe (Set1 String)
    Nothing      -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance MonadAddContext TCM where
      addCtx :: forall a. Name -> Dom Type -> TCM a -> TCM a
    addCtx Name
    x Dom Type
    a TCM a
    ret = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x) (Name -> TCM a -> TCM a
    forall b. Name -> TCM b -> TCM b
    withShadowingNameTCM Name
    x) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
        Name -> Dom Type -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    defaultAddCtx Name
    x Dom Type
    a TCM a
    ret

      addLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a
    addLetBinding' Origin
    o Name
    x Term
    u Dom Type
    a TCM a
    ret = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x) (Name -> TCM a -> TCM a
    forall b. Name -> TCM b -> TCM b
    withShadowingNameTCM Name
    x) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
        Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    Origin -> Name -> Term -> Dom Type -> m a -> m a
    defaultAddLetBinding' Origin
    o Name
    x Term
    u Dom Type
    a TCM a
    ret

      updateContext :: forall a.
    Substitution' Term -> (Context -> Context) -> TCM a -> TCM a
    updateContext Substitution' Term
    sub Context -> Context
    f = (Context -> Context) -> TCMT IO a -> TCMT IO a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext Context -> Context
    f (TCMT IO a -> TCMT IO a)
    -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' Term -> TCMT IO a -> TCMT IO a
    forall (tcm :: * -> *) a.
    (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
     ReadTCState tcm) =>
    Substitution' Term -> tcm a -> tcm a
    checkpoint Substitution' Term
    sub

      withFreshName :: forall a. Range -> String -> (Name -> TCM a) -> TCM a
    withFreshName Range
    r String
    x Name -> TCM a
    m = Range -> String -> TCMT IO Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    Range -> String -> m Name
    freshName Range
    r String
    x TCMT IO Name -> (Name -> TCM a) -> TCM a
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Name -> TCM a
    m

    addRecordNameContext
      :: (MonadAddContext m, MonadFresh NameId m)
      => Dom Type -> m b -> m b
    addRecordNameContext :: forall (m :: * -> *) b.
    (MonadAddContext m, MonadFresh NameId m) =>
    Dom Type -> m b -> m b
    addRecordNameContext Dom Type
    dom m b
    ret = do
      x <- Name -> Name
    forall a. LensInScope a => a -> a
    setNotInScope (Name -> Name) -> m Name -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Name
    forall (m :: * -> *). MonadFresh NameId m => m Name
    freshRecordName
      addCtx x dom ret

    -- | Various specializations of @addCtx@.
    class AddContext b where
      addContext :: (MonadAddContext m) => b -> m a -> m a
      contextSize :: b -> Nat

    -- | Wrapper to tell 'addContext' not to mark names as
    --   'NotInScope'. Used when adding a user-provided, but already type
    --   checked, telescope to the context.
    newtype KeepNames a = KeepNames a

    instance {-# OVERLAPPABLE #-} AddContext a => AddContext [a] where
      addContext :: forall (m :: * -> *) a. MonadAddContext m => [a] -> m a -> m a
    addContext = (m a -> [a] -> m a) -> [a] -> m a -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((a -> m a -> m a) -> m a -> [a] -> m a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr a -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => a -> m a -> m a
    addContext); {-# INLINABLE addContext #-}
      contextSize :: [a] -> Nat
    contextSize = [Nat] -> Nat
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Nat] -> Nat) -> ([a] -> [Nat]) -> [a] -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Nat) -> [a] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Nat
    forall b. AddContext b => b -> Nat
    contextSize

    instance AddContext ContextEntry where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    ContextEntry -> m a -> m a
    addContext (CtxVar Name
    x Dom Type
    a) = Name -> Dom Type -> m a -> m a
    forall a. Name -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    a
      {-# INLINE addContext #-}
      contextSize :: ContextEntry -> Nat
    contextSize ContextEntry
    _ = Nat
    1

    instance AddContext (Name, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (Name, Dom Type) -> m a -> m a
    addContext = (Name -> Dom Type -> m a -> m a) -> (Name, Dom Type) -> m a -> m a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Dom Type -> m a -> m a
    forall a. Name -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx; {-# INLINE addContext #-}
      contextSize :: (Name, Dom Type) -> Nat
    contextSize (Name, Dom Type)
    _ = Nat
    1
    {-# SPECIALIZE addContext :: (Name, Dom Type) -> TCM a -> TCM a #-}

    instance AddContext (Dom (Name, Type)) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Dom (Name, Type) -> m a -> m a
    addContext = (Name, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (Name, Dom Type) -> m a -> m a
    addContext ((Name, Dom Type) -> m a -> m a)
    -> (Dom (Name, Type) -> (Name, Dom Type))
    -> Dom (Name, Type)
    -> m a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Dom Type)
    forall (t :: * -> *) (m :: * -> *) a.
    (Decoration t, Functor m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a.
    Functor m =>
    Dom' Term (m a) -> m (Dom' Term a)
    distributeF
      contextSize :: Dom (Name, Type) -> Nat
    contextSize Dom (Name, Type)
    _ = Nat
    1

    instance AddContext (Dom (String, Type)) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Dom (String, Type) -> m a -> m a
    addContext = (String, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext ((String, Dom Type) -> m a -> m a)
    -> (Dom (String, Type) -> (String, Dom Type))
    -> Dom (String, Type)
    -> m a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (String, Type) -> (String, Dom Type)
    forall (t :: * -> *) (m :: * -> *) a.
    (Decoration t, Functor m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a.
    Functor m =>
    Dom' Term (m a) -> m (Dom' Term a)
    distributeF
      contextSize :: Dom (String, Type) -> Nat
    contextSize Dom (String, Type)
    _ = Nat
    1

    instance AddContext ([Name], Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    ([Name], Dom Type) -> m a -> m a
    addContext ([Name]
    xs, Dom Type
    dom) = ListTel' Name -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    ListTel' Name -> m a -> m a
    addContext ((Name -> Name) -> [Name] -> Dom Type -> ListTel' Name
    forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    bindsToTel' Name -> Name
    forall a. a -> a
    id [Name]
    xs Dom Type
    dom)
      contextSize :: ([Name], Dom Type) -> Nat
    contextSize ([Name]
    xs, Dom Type
    _) = [Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Name]
    xs

    instance AddContext (List1 Name, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (List1 Name, Dom Type) -> m a -> m a
    addContext (List1 Name
    xs, Dom Type
    dom) = ListTel' Name -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    ListTel' Name -> m a -> m a
    addContext ((Name -> Name) -> List1 Name -> Dom Type -> ListTel' Name
    forall a. (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
    bindsToTel'1 Name -> Name
    forall a. a -> a
    id List1 Name
    xs Dom Type
    dom)
      contextSize :: (List1 Name, Dom Type) -> Nat
    contextSize (List1 Name
    xs, Dom Type
    _) = List1 Name -> Nat
    forall a. NonEmpty a -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length List1 Name
    xs

    instance AddContext ([WithHiding Name], Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    ([WithHiding Name], Dom Type) -> m a -> m a
    addContext ([]    , Dom Type
    dom) = m a -> m a
    forall a. a -> a
    id
      addContext (WithHiding Name
    x : [WithHiding Name]
    xs, Dom Type
    dom) = (NonEmpty (WithHiding Name), Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (NonEmpty (WithHiding Name), Dom Type) -> m a -> m a
    addContext (WithHiding Name
    x WithHiding Name -> [WithHiding Name] -> NonEmpty (WithHiding Name)
    forall a. a -> [a] -> NonEmpty a
    :| [WithHiding Name]
    xs, Dom Type
    dom)
      contextSize :: ([WithHiding Name], Dom Type) -> Nat
    contextSize ([WithHiding Name]
    xs, Dom Type
    _) = [WithHiding Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [WithHiding Name]
    xs

    instance AddContext (List1 (WithHiding Name), Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (NonEmpty (WithHiding Name), Dom Type) -> m a -> m a
    addContext (WithHiding Hiding
    h Name
    x :| [WithHiding Name]
    xs, Dom Type
    dom) =
        (Name, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (Name, Dom Type) -> m a -> m a
    addContext (Name
    x , (Hiding -> Hiding) -> Dom Type -> Dom Type
    forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
    mapHiding (Hiding -> Hiding -> Hiding
    forall a. Monoid a => a -> a -> a
    mappend Hiding
    h) Dom Type
    dom) (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
        ([WithHiding Name], Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    ([WithHiding Name], Dom Type) -> m a -> m a
    addContext ([WithHiding Name]
    xs, Nat -> Dom Type -> Dom Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Dom Type
    dom)
      contextSize :: (NonEmpty (WithHiding Name), Dom Type) -> Nat
    contextSize (NonEmpty (WithHiding Name)
    xs, Dom Type
    _) = NonEmpty (WithHiding Name) -> Nat
    forall a. NonEmpty a -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length NonEmpty (WithHiding Name)
    xs

    instance AddContext ([Arg Name], Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    ([Arg Name], Type) -> m a -> m a
    addContext ([Arg Name]
    xs, Type
    t) = ([NamedArg Name], Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    ([NamedArg Name], Type) -> m a -> m a
    addContext (((Arg Name -> NamedArg Name) -> [Arg Name] -> [NamedArg Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Arg Name -> NamedArg Name) -> [Arg Name] -> [NamedArg Name])
    -> ((Name -> Named_ Name) -> Arg Name -> NamedArg Name)
    -> (Name -> Named_ Name)
    -> [Arg Name]
    -> [NamedArg Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Named_ Name) -> Arg Name -> NamedArg Name
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) Name -> Named_ Name
    forall a name. a -> Named name a
    unnamed [Arg Name]
    xs :: [NamedArg Name], Type
    t)
      contextSize :: ([Arg Name], Type) -> Nat
    contextSize ([Arg Name]
    xs, Type
    _) = [Arg Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Name]
    xs

    instance AddContext (List1 (Arg Name), Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (List1 (Arg Name), Type) -> m a -> m a
    addContext (List1 (Arg Name)
    xs, Type
    t) = (List1 (NamedArg Name), Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (List1 (NamedArg Name), Type) -> m a -> m a
    addContext (((Arg Name -> NamedArg Name)
    -> List1 (Arg Name) -> List1 (NamedArg Name)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Arg Name -> NamedArg Name)
     -> List1 (Arg Name) -> List1 (NamedArg Name))
    -> ((Name -> Named_ Name) -> Arg Name -> NamedArg Name)
    -> (Name -> Named_ Name)
    -> List1 (Arg Name)
    -> List1 (NamedArg Name)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Named_ Name) -> Arg Name -> NamedArg Name
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) Name -> Named_ Name
    forall a name. a -> Named name a
    unnamed List1 (Arg Name)
    xs :: List1 (NamedArg Name), Type
    t)
      contextSize :: (List1 (Arg Name), Type) -> Nat
    contextSize (List1 (Arg Name)
    xs, Type
    _) = List1 (Arg Name) -> Nat
    forall a. NonEmpty a -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length List1 (Arg Name)
    xs

    instance AddContext ([NamedArg Name], Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    ([NamedArg Name], Type) -> m a -> m a
    addContext ([], Type
    _)     = m a -> m a
    forall a. a -> a
    id
      addContext (NamedArg Name
    x : [NamedArg Name]
    xs, Type
    t) = (List1 (NamedArg Name), Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (List1 (NamedArg Name), Type) -> m a -> m a
    addContext (NamedArg Name
    x NamedArg Name -> [NamedArg Name] -> List1 (NamedArg Name)
    forall a. a -> [a] -> NonEmpty a
    :| [NamedArg Name]
    xs, Type
    t)
      contextSize :: ([NamedArg Name], Type) -> Nat
    contextSize ([NamedArg Name]
    xs, Type
    _) = [NamedArg Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [NamedArg Name]
    xs

    instance AddContext (List1 (NamedArg Name), Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (List1 (NamedArg Name), Type) -> m a -> m a
    addContext (NamedArg Name
    x :| [NamedArg Name]
    xs, Type
    t) =
        (Name, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (Name, Dom Type) -> m a -> m a
    addContext (NamedArg Name -> Name
    forall a. NamedArg a -> a
    namedArg NamedArg Name
    x, Type
    t Type -> Dom' Term () -> Dom Type
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NamedArg Name -> Dom' Term ()
    domFromNamedArgName NamedArg Name
    x) (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
        ([NamedArg Name], Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    ([NamedArg Name], Type) -> m a -> m a
    addContext ([NamedArg Name]
    xs, Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Type
    t)
      contextSize :: (List1 (NamedArg Name), Type) -> Nat
    contextSize (List1 (NamedArg Name)
    xs, Type
    _) = List1 (NamedArg Name) -> Nat
    forall a. NonEmpty a -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length List1 (NamedArg Name)
    xs

    instance AddContext (String, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    s, Dom Type
    dom) m a
    ret =
        Range -> String -> (Name -> m a) -> m a
    forall a. Range -> String -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange String
    s ((Name -> m a) -> m a) -> (Name -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \Name
    x -> Name -> Dom Type -> m a -> m a
    forall a. Name -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx (Name -> Name
    forall a. LensInScope a => a -> a
    setNotInScope Name
    x) Dom Type
    dom m a
    ret
      contextSize :: (String, Dom Type) -> Nat
    contextSize (String, Dom Type)
    _ = Nat
    1
    {-# SPECIALIZE addContext :: (String, Dom Type) -> TCM a -> TCM a #-}

    instance AddContext (Text, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (Text, Dom Type) -> m a -> m a
    addContext (Text
    s, Dom Type
    dom) m a
    ret = (String, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (Text -> String
    T.unpack Text
    s, Dom Type
    dom) m a
    ret
      contextSize :: (Text, Dom Type) -> Nat
    contextSize (Text, Dom Type)
    _ = Nat
    1
    {-# SPECIALIZE addContext :: (Text, Dom Type) -> TCM a -> TCM a #-}

    instance AddContext (KeepNames String, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (KeepNames String, Dom Type) -> m a -> m a
    addContext (KeepNames String
    s, Dom Type
    dom) m a
    ret =
        Range -> String -> (Name -> m a) -> m a
    forall a. Range -> String -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange String
    s ((Name -> m a) -> m a) -> (Name -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \ Name
    x -> Name -> Dom Type -> m a -> m a
    forall a. Name -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    dom m a
    ret
      contextSize :: (KeepNames String, Dom Type) -> Nat
    contextSize (KeepNames String, Dom Type)
    _ = Nat
    1
    {-# SPECIALIZE addContext :: (KeepNames String, Dom Type) -> TCM a -> TCM a #-}

    instance AddContext (Dom Type) where
      addContext :: forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
    addContext Dom Type
    dom = (String, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    "_" :: String, Dom Type
    dom)
      contextSize :: Dom Type -> Nat
    contextSize Dom Type
    _ = Nat
    1

    instance AddContext Name where
      addContext :: forall (m :: * -> *) a. MonadAddContext m => Name -> m a -> m a
    addContext Name
    x = (Name, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (Name, Dom Type) -> m a -> m a
    addContext (Name
    x, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__)
      contextSize :: Name -> Nat
    contextSize Name
    _ = Nat
    1

    instance {-# OVERLAPPING #-} AddContext String where
      addContext :: forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
    addContext String
    s = (String, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    s, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__)
      contextSize :: String -> Nat
    contextSize String
    _ = Nat
    1

    instance AddContext (KeepNames Telescope) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    KeepNames Telescope -> m a -> m a
    addContext (KeepNames Telescope
    tel) m a
    ret = Telescope -> m a
    loop Telescope
    tel where
        loop :: Telescope -> m a
    loop Telescope
    EmptyTel          = m a
    ret
        loop (ExtendTel Dom Type
    t Abs Telescope
    tel) = (String -> KeepNames String)
    -> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' String -> KeepNames String
    forall a. a -> KeepNames a
    KeepNames Dom Type
    t Abs Telescope
    tel Telescope -> m a
    loop
      contextSize :: KeepNames Telescope -> Nat
    contextSize (KeepNames Telescope
    tel) = Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    tel
    {-# SPECIALIZE addContext :: KeepNames Telescope -> TCM a -> TCM a #-}

    instance AddContext Telescope where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel m a
    ret = Telescope -> m a
    loop Telescope
    tel where
        loop :: Telescope -> m a
    loop Telescope
    EmptyTel          = m a
    ret
        loop (ExtendTel Dom Type
    t Abs Telescope
    tel) = (String -> String)
    -> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' String -> String
    forall a. a -> a
    id Dom Type
    t Abs Telescope
    tel Telescope -> m a
    loop
      contextSize :: Telescope -> Nat
    contextSize = Telescope -> Nat
    forall a. Sized a => a -> Nat
    size
    {-# SPECIALIZE addContext :: Telescope -> TCM a -> TCM a #-}

    -- | Go under an abstraction.  Do not extend context in case of 'NoAbs'.
    {-# SPECIALIZE underAbstraction :: Subst a => Dom Type -> Abs a -> (a -> TCM b) -> TCM b #-}
    underAbstraction :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction :: forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction = (String -> String) -> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' String -> String
    forall a. a -> a
    id

    underAbstraction' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
                         (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' :: forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' String -> name
    _ Dom Type
    _ (NoAbs String
    _ a
    v) a -> m b
    k = a -> m b
    k a
    v
    underAbstraction' String -> name
    wrap Dom Type
    t Abs a
    a a -> m b
    k = (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' String -> name
    wrap Dom Type
    t Abs a
    a a -> m b
    k

    -- | Go under an abstraction, treating 'NoAbs' as 'Abs'.
    underAbstractionAbs :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs :: forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs = (String -> String) -> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' String -> String
    forall a. a -> a
    id

    underAbstractionAbs'
      :: (Subst a, MonadAddContext m, AddContext (name, Dom Type))
      => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' :: forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' String -> name
    wrap Dom Type
    t Abs a
    a a -> m b
    k = (name, Dom Type) -> m b -> m b
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (name, Dom Type) -> m a -> m a
    addContext (String -> name
    wrap (String -> name) -> String -> name
    forall a b. (a -> b) -> a -> b
    $ String -> String
    realName (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ Abs a -> String
    forall a. Abs a -> String
    absName Abs a
    a, Dom Type
    t) (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ a -> m b
    k (a -> m b) -> a -> m b
    forall a b. (a -> b) -> a -> b
    $ Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    a
      where
        realName :: String -> String
    realName String
    s = if String -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName String
    s then String
    "x" else String -> String
    argNameToString String
    s

    -- | Go under an abstract without worrying about the type to add to the context.
    {-# SPECIALIZE underAbstraction_ :: Subst a => Abs a -> (a -> TCM b) -> TCM b #-}
    underAbstraction_ :: (Subst a, MonadAddContext m) => Abs a -> (a -> m b) -> m b
    underAbstraction_ :: forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ = Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__

    -- | Map a monadic function on the thing under the abstraction, adding
    --   the abstracted variable to the context.
    mapAbstraction
      :: (Subst a, Subst b, MonadAddContext m)
      => Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction :: forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction Dom Type
    dom a -> m b
    f Abs a
    x = (Abs a
    x Abs a -> b -> Abs b
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>) (b -> Abs b) -> m b -> m (Abs b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    dom Abs a
    x a -> m b
    f

    mapAbstraction_
      :: (Subst a, Subst b, MonadAddContext m)
      => (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction_ :: forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction_ = Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__

    {-# SPECIALIZE getLetBindings :: TCM [(Name, LetBinding)] #-}
    getLetBindings :: MonadTCEnv tcm => tcm [(Name, LetBinding)]
    getLetBindings :: forall (tcm :: * -> *). MonadTCEnv tcm => tcm [(Name, LetBinding)]
    getLetBindings = do
      bs <- (TCEnv -> Map Name (Open LetBinding))
    -> tcm (Map Name (Open LetBinding))
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Map Name (Open LetBinding)
    envLetBindings
      forM (Map.toList bs) $ \ (Name
    n, Open LetBinding
    o) -> (,) Name
    n (LetBinding -> (Name, LetBinding))
    -> tcm LetBinding -> tcm (Name, LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Open LetBinding -> tcm LetBinding
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen Open LetBinding
    o

    -- | Add a let bound variable
    {-# SPECIALIZE defaultAddLetBinding' :: Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a #-}
    defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Origin -> Name -> Term -> Dom Type -> m a -> m a
    defaultAddLetBinding' :: forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    Origin -> Name -> Term -> Dom Type -> m a -> m a
    defaultAddLetBinding' Origin
    o Name
    x Term
    v Dom Type
    t m a
    ret = do
        vt <- LetBinding -> m (Open LetBinding)
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen (LetBinding -> m (Open LetBinding))
    -> LetBinding -> m (Open LetBinding)
    forall a b. (a -> b) -> a -> b
    $ Origin -> Term -> Dom Type -> LetBinding
    LetBinding Origin
    o Term
    v Dom Type
    t
        flip localTC ret $ \TCEnv
    e -> TCEnv
    e { envLetBindings = Map.insert x vt $ envLetBindings e }

    -- | Add a let bound variable
    {-# SPECIALIZE addLetBinding :: ArgInfo -> Origin -> Name -> Term -> Type -> TCM a -> TCM a #-}
    addLetBinding :: MonadAddContext m => ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
    addLetBinding :: forall (m :: * -> *) a.
    MonadAddContext m =>
    ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
    addLetBinding ArgInfo
    info Origin
    o Name
    x Term
    v Type
    t0 m a
    ret = Origin -> Name -> Term -> Dom Type -> m a -> m a
    forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Origin -> Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' Origin
    o Name
    x Term
    v (ArgInfo -> Type -> Dom Type
    forall a. ArgInfo -> a -> Dom a
    defaultArgDom ArgInfo
    info Type
    t0) m a
    ret

    {-# SPECIALIZE removeLetBinding :: Name -> TCM a -> TCM a #-}
    -- | Remove a let bound variable.
    removeLetBinding :: MonadTCEnv m => Name -> m a -> m a
    removeLetBinding :: forall (m :: * -> *) a. MonadTCEnv m => Name -> m a -> m a
    removeLetBinding Name
    x = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envLetBindings = Map.delete x (envLetBindings e) }

    {-# SPECIALIZE removeLetBindingsFrom :: Name -> TCM a -> TCM a #-}
    -- | Remove a let bound variable and all let bindings introduced after it. For instance before
    --   printing its body to avoid folding the binding itself, or using bindings defined later.
    --   Relies on the invariant that names introduced later are sorted after earlier names.
    removeLetBindingsFrom :: MonadTCEnv m => Name -> m a -> m a
    removeLetBindingsFrom :: forall (m :: * -> *) a. MonadTCEnv m => Name -> m a -> m a
    removeLetBindingsFrom Name
    x = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envLetBindings = fst $ Map.split x (envLetBindings e) }

    -- * Querying the context

    -- | Get the current context.
    {-# SPECIALIZE getContext :: TCM Context #-}
    getContext :: MonadTCEnv m => m Context
    getContext :: forall (m :: * -> *). MonadTCEnv m => m Context
    getContext = (TCEnv -> Context) -> m Context
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Context
    envContext

    -- | Get the size of the current context.
    {-# SPECIALIZE getContextSize :: TCM Nat #-}
    getContextSize :: (MonadTCEnv m) => m Nat
    getContextSize :: forall (m :: * -> *). MonadTCEnv m => m Nat
    getContextSize = Context -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length (Context -> Nat) -> m Context -> m Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    {-# SPECIALIZE getContextVars :: TCM [(Int, Dom Name)] #-}
    getContextVars :: (MonadTCEnv m) => m [(Int, Dom Name)]
    getContextVars :: forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom Name)]
    getContextVars = Context -> [(Nat, Dom Name)]
    contextVars (Context -> [(Nat, Dom Name)]) -> m Context -> m [(Nat, Dom Name)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    {-# SPECIALIZE getContextVars' :: TCM [(Int, Dom Name)] #-}
    getContextVars' :: (MonadTCEnv m) => m [(Int, Dom Name)]
    getContextVars' :: forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom Name)]
    getContextVars' = Context -> [(Nat, Dom Name)]
    contextVars' (Context -> [(Nat, Dom Name)]) -> m Context -> m [(Nat, Dom Name)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    contextVars :: Context -> [(Int, Dom Name)]
    contextVars :: Context -> [(Nat, Dom Name)]
    contextVars = [(Nat, Dom Name)] -> [(Nat, Dom Name)]
    forall a. [a] -> [a]
    reverse ([(Nat, Dom Name)] -> [(Nat, Dom Name)])
    -> (Context -> [(Nat, Dom Name)]) -> Context -> [(Nat, Dom Name)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> [(Nat, Dom Name)]
    contextVars'

    contextVars' :: Context -> [(Int, Dom Name)]
    contextVars' :: Context -> [(Nat, Dom Name)]
    contextVars' = (Nat -> ContextEntry -> (Nat, Dom Name))
    -> [Nat] -> Context -> [(Nat, Dom Name)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> ContextEntry -> (Nat, Dom Name)
    forall {a}. a -> ContextEntry -> (a, Dom Name)
    mkVar [Nat
    0..]
      where
        mkVar :: a -> ContextEntry -> (a, Dom Name)
    mkVar a
    i (CtxVar Name
    x Dom Type
    a) = (a
    i, Dom Type
    a Dom Type -> Name -> Dom Name
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Name
    x)

    -- | Generate @[var (n - 1), ..., var 0]@ for all bound variables in the context.
    {-# SPECIALIZE getContextArgs :: TCM Args #-}
    getContextArgs :: (MonadTCEnv m) => m Args
    getContextArgs :: forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs = Context -> Args
    contextArgs (Context -> Args) -> m Context -> m Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    contextArgs :: Context -> Args
    contextArgs :: Context -> Args
    contextArgs = ((Nat, Dom Name) -> Arg Term) -> [(Nat, Dom Name)] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Nat
    i,Dom Name
    x) -> Nat -> Term
    var Nat
    i Term -> Arg Name -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Name -> Arg Name
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Name
    x) ([(Nat, Dom Name)] -> Args)
    -> (Context -> [(Nat, Dom Name)]) -> Context -> Args
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> [(Nat, Dom Name)]
    contextVars

    -- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
    {-# SPECIALIZE getContextTerms :: TCM [Term] #-}
    getContextTerms :: (MonadTCEnv m) => m [Term]
    getContextTerms :: forall (m :: * -> *). MonadTCEnv m => m [Term]
    getContextTerms = (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg (Args -> [Term]) -> m Args -> m [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs

    contextTerms :: Context -> [Term]
    contextTerms :: Context -> [Term]
    contextTerms = (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg (Args -> [Term]) -> (Context -> Args) -> Context -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> Args
    contextArgs

    -- | Get the current context as a 'Telescope'.
    {-# SPECIALIZE getContextTelescope :: TCM Telescope #-}
    getContextTelescope :: (MonadTCEnv m) => m Telescope
    getContextTelescope :: forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope = Context -> Telescope
    contextToTel (Context -> Telescope) -> m Context -> m Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    contextToTel :: Context -> Telescope
    contextToTel :: Context -> Telescope
    contextToTel = Context -> Telescope
    go (Context -> Telescope)
    -> (Context -> Context) -> Context -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> Context
    forall a. [a] -> [a]
    reverse
      where
        go :: Context -> Telescope
    go [] = Telescope
    forall a. Tele a
    EmptyTel
        go (CtxVar Name
    x Dom Type
    a   : Context
    ctx) = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Name -> String
    nameToArgName Name
    x) (Context -> Telescope
    go Context
    ctx)

    -- | Get the names of all declarations in the context.
    {-# SPECIALIZE getContextNames :: TCM [Name] #-}
    getContextNames :: (MonadTCEnv m) => m [Name]
    getContextNames :: forall (m :: * -> *). MonadTCEnv m => m [Name]
    getContextNames = Context -> [Name]
    contextNames (Context -> [Name]) -> m Context -> m [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    {-# SPECIALIZE getContextNames' :: TCM [Name] #-}
    getContextNames' :: (MonadTCEnv m) => m [Name]
    getContextNames' :: forall (m :: * -> *). MonadTCEnv m => m [Name]
    getContextNames' = Context -> [Name]
    contextNames' (Context -> [Name]) -> m Context -> m [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    contextNames :: Context -> [Name]
    contextNames :: Context -> [Name]
    contextNames = ((Nat, Dom Name) -> Name) -> [(Nat, Dom Name)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom Name -> Name
    forall t e. Dom' t e -> e
    unDom (Dom Name -> Name)
    -> ((Nat, Dom Name) -> Dom Name) -> (Nat, Dom Name) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat, Dom Name) -> Dom Name
    forall a b. (a, b) -> b
    snd) ([(Nat, Dom Name)] -> [Name])
    -> (Context -> [(Nat, Dom Name)]) -> Context -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> [(Nat, Dom Name)]
    contextVars

    contextNames' :: Context -> [Name]
    contextNames' :: Context -> [Name]
    contextNames' = ((Nat, Dom Name) -> Name) -> [(Nat, Dom Name)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom Name -> Name
    forall t e. Dom' t e -> e
    unDom (Dom Name -> Name)
    -> ((Nat, Dom Name) -> Dom Name) -> (Nat, Dom Name) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat, Dom Name) -> Dom Name
    forall a b. (a, b) -> b
    snd) ([(Nat, Dom Name)] -> [Name])
    -> (Context -> [(Nat, Dom Name)]) -> Context -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> [(Nat, Dom Name)]
    contextVars'

    -- | get type of bound variable (i.e. deBruijn index)
    --
    lookupBV_ :: Nat -> Context -> Maybe ContextEntry
    lookupBV_ :: Nat -> Context -> Maybe ContextEntry
    lookupBV_ Nat
    n Context
    ctx = Nat -> ContextEntry -> ContextEntry
    forall a. Subst a => Nat -> a -> a
    raise (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) (ContextEntry -> ContextEntry)
    -> Maybe ContextEntry -> Maybe ContextEntry
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Context
    ctx Context -> Nat -> Maybe ContextEntry
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    n

    {-# SPECIALIZE lookupBV' :: Nat -> TCM (Maybe ContextEntry) #-}
    lookupBV' :: MonadTCEnv m => Nat -> m (Maybe ContextEntry)
    lookupBV' :: forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe ContextEntry)
    lookupBV' Nat
    n = Nat -> Context -> Maybe ContextEntry
    lookupBV_ Nat
    n (Context -> Maybe ContextEntry)
    -> m Context -> m (Maybe ContextEntry)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext

    {-# SPECIALIZE lookupBV :: Nat -> TCM ContextEntry #-}
    lookupBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m ContextEntry
    lookupBV :: forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m ContextEntry
    lookupBV Nat
    n = do
      let failure :: m ContextEntry
    failure = do
            ctx <- m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
            __IMPOSSIBLE_VERBOSE__ $ unwords
              [ "de Bruijn index out of scope:", show n
              , "in context", prettyShow $ map ctxEntryName ctx
              ]
      m (Maybe ContextEntry)
    -> m ContextEntry
    -> (ContextEntry -> m ContextEntry)
    -> m ContextEntry
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Nat -> m (Maybe ContextEntry)
    forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe ContextEntry)
    lookupBV' Nat
    n) m ContextEntry
    failure ContextEntry -> m ContextEntry
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    ctxEntryName :: ContextEntry -> Name
    ctxEntryName :: ContextEntry -> Name
    ctxEntryName (CtxVar Name
    x Dom Type
    _) = Name
    x

    ctxEntryDom :: ContextEntry -> Dom Type
    ctxEntryDom :: ContextEntry -> Dom Type
    ctxEntryDom (CtxVar Name
    _ Dom Type
    a) = Dom Type
    a

    ctxEntryType :: ContextEntry -> Type
    ctxEntryType :: ContextEntry -> Type
    ctxEntryType = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type)
    -> (ContextEntry -> Dom Type) -> ContextEntry -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ContextEntry -> Dom Type
    ctxEntryDom

    {-# SPECIALIZE domOfBV :: Nat -> TCM (Dom Type) #-}
    domOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m (Dom Type)
    domOfBV :: forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m (Dom Type)
    domOfBV Nat
    n = ContextEntry -> Dom Type
    ctxEntryDom (ContextEntry -> Dom Type) -> m ContextEntry -> m (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> m ContextEntry
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m ContextEntry
    lookupBV Nat
    n

    {-# SPECIALIZE typeOfBV :: Nat -> TCM Type #-}
    typeOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m Type
    typeOfBV :: forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Type
    typeOfBV Nat
    i = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type) -> m (Dom Type) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> m (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m (Dom Type)
    domOfBV Nat
    i

    {-# SPECIALIZE nameOfBV' :: Nat -> TCM (Maybe Name) #-}
    nameOfBV' :: (MonadTCEnv m) => Nat -> m (Maybe Name)
    nameOfBV' :: forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe Name)
    nameOfBV' Nat
    n = (ContextEntry -> Name) -> Maybe ContextEntry -> Maybe Name
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ContextEntry -> Name
    ctxEntryName (Maybe ContextEntry -> Maybe Name)
    -> m (Maybe ContextEntry) -> m (Maybe Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> m (Maybe ContextEntry)
    forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe ContextEntry)
    lookupBV' Nat
    n

    {-# SPECIALIZE nameOfBV :: Nat -> TCM Name #-}
    nameOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m Name
    nameOfBV :: forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Name
    nameOfBV Nat
    n = ContextEntry -> Name
    ctxEntryName (ContextEntry -> Name) -> m ContextEntry -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> m ContextEntry
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m ContextEntry
    lookupBV Nat
    n

    -- | Get the term corresponding to a named variable. If it is a lambda bound
    --   variable the deBruijn index is returned and if it is a let bound variable
    --   its definition is returned.
    {-# SPECIALIZE getVarInfo :: Name -> TCM (Term, Dom Type) #-}
    getVarInfo :: (MonadDebug m, MonadTCEnv m) => Name -> m (Term, Dom Type)
    getVarInfo :: forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Name -> m (Term, Dom Type)
    getVarInfo Name
    x =
        do  ctx <- m [(Nat, Dom Name)]
    forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom Name)]
    getContextVars'
            def <- asksTC envLetBindings
            case List.findIndex ((== x) . unDom . snd) ctx of
                Just Nat
    n -> do
                    t <- Nat -> m (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m (Dom Type)
    domOfBV Nat
    n
                    return (var n, t)
                Maybe Nat
    _       ->
                    case Name -> Map Name (Open LetBinding) -> Maybe (Open LetBinding)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Map Name (Open LetBinding)
    def of
                        Just Open LetBinding
    vt -> do
                          LetBinding _ v t <- Open LetBinding -> m LetBinding
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen Open LetBinding
    vt
                          return (v, t)
                        Maybe (Open LetBinding)
    _ -> String -> m (Term, Dom Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ (String -> m (Term, Dom Type)) -> String -> m (Term, Dom Type)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords
                          [ String
    "unbound variable"
                          , Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> String) -> Name -> String
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    nameConcrete Name
    x
                          , String
    "(id: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NameId -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> NameId
    nameId Name
    x) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                          ]