    module Agda.TypeChecking.Monad.Context where

    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
    -- Control.Monad.Fail import is redundant since GHC 8.8.1
    import Control.Monad.Fail (MonadFail)

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

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    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.Free
    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 Agda.Utils.Maybe
    import Agda.Utils.Pretty
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- * Modifying the context

    -- | Modify a 'Context' in a computation.  Warning: does not update
    --   the checkpoints. Use @updateContext@ instead.
    {-# SPECIALIZE unsafeModifyContext :: (Context -> Context) -> TCM a -> TCM a #-}
    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 (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 :: Context
    envContext = Context -> Context
    f (Context -> Context) -> Context -> Context
    forall a b. (a -> b) -> a -> b
    $ TCEnv -> Context
    envContext TCEnv
    e }

    -- | 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
    $ (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (Name, Type) -> Dom (Name, Type)
    forall e. Dom e -> Dom e
    f

    -- | 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' CheckpointId TCEnv
    -> (CheckpointId -> CheckpointId) -> tcm a -> tcm a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' CheckpointId TCEnv
    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' (Map CheckpointId (Substitution' Term)) TCEnv
    -> (Map CheckpointId (Substitution' Term)
        -> Map CheckpointId (Substitution' Term))
    -> tcm a
    -> tcm a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    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' (Map ModuleName CheckpointId) TCState
    -> (Map ModuleName CheckpointId -> Map ModuleName CheckpointId)
    -> tcm a
    -> tcm a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' (Map ModuleName CheckpointId) TCState
    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' [(Name, LocalVar)] ScopeInfo
    -> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> tcm a -> tcm a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a ScopeInfo -> (a -> a) -> m b -> m b
    locallyScope Lens' [(Name, LocalVar)] ScopeInfo
    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' (Map Name (Open (Term, Dom Type))) TCEnv
    -> (Map Name (Open (Term, Dom Type))
        -> Map Name (Open (Term, Dom Type)))
    -> tcm a
    -> tcm a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' (Map Name (Open (Term, Dom Type))) TCEnv
    eLetBindings (Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall a b. a -> b -> a
    const Map Name (Open (Term, Dom Type))
    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' [(Name, LocalVar)] ScopeInfo
    -> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> m a -> m a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a ScopeInfo -> (a -> a) -> m b -> m b
    locallyScope Lens' [(Name, LocalVar)] ScopeInfo
    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 => Int -> tcm a -> tcm a
    unsafeEscapeContext Int
    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
    $ Int -> Context -> Context
    forall a. Int -> [a] -> [a]
    drop Int
    n

    -- | 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 -> Int -> m a -> m a
    escapeContext Impossible
    err Int
    n = Substitution' Term -> (Context -> Context) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext (Impossible -> Int -> Substitution' Term
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    err Int
    n) ((Context -> Context) -> m a -> m a)
    -> (Context -> Context) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Int -> Context -> Context
    forall a. Int -> [a] -> [a]
    drop Int
    n

    -- * Manipulating checkpoints --

    -- | 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
    $ VerboseKey -> Int -> VerboseKey -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> VerboseKey -> m ()
    reportSLn VerboseKey
    "tc.cxt.checkpoint" Int
    105 (VerboseKey -> tcm ()) -> VerboseKey -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "New checkpoint {"
      CheckpointId
    old     <- Lens' CheckpointId TCEnv -> tcm CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
      Map ModuleName CheckpointId
    oldMods <- Lens' (Map ModuleName CheckpointId) TCState
    -> tcm (Map ModuleName CheckpointId)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC  Lens' (Map ModuleName CheckpointId) TCState
    stModuleCheckpoints
      CheckpointId
    chkpt <- tcm CheckpointId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      tcm () -> tcm ()
    forall (m :: * -> *). MonadDebug m => m () -> m ()
    unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Int -> tcm () -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> m () -> m ()
    verboseS VerboseKey
    "tc.cxt.checkpoint" Int
    105 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ do
        Telescope
    cxt <- tcm Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
        Map CheckpointId (Substitution' Term)
    cps <- Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    -> tcm (Map CheckpointId (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    eCheckpoints
        let cps' :: Map CheckpointId (Substitution' Term)
    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 (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 -> Doc
    prCps Map a a
    cps = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ a -> Doc
    forall a. Show a => a -> Doc
    pshow a
    c Doc -> Doc -> Doc
    <+> Doc
    ": " Doc -> Doc -> Doc
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    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 ]
        VerboseKey -> Int -> TCM Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCM Doc -> m ()
    reportSDoc VerboseKey
    "tc.cxt.checkpoint" Int
    105 (TCM Doc -> tcm ()) -> TCM Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Doc
    "old =" Doc -> Doc -> Doc
    <+> CheckpointId -> Doc
    forall a. Show a => a -> Doc
    pshow CheckpointId
    old
          , Doc
    "new =" Doc -> Doc -> Doc
    <+> CheckpointId -> Doc
    forall a. Show a => a -> Doc
    pshow CheckpointId
    chkpt
          , Doc
    "sub =" Doc -> Doc -> Doc
    <+> Substitution' Term -> Doc
    forall a. Pretty a => a -> Doc
    pretty Substitution' Term
    sub
          , Doc
    "cxt =" Doc -> Doc -> Doc
    <+> Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    cxt
          , Doc
    "old substs =" Doc -> Doc -> Doc
    <+> Map CheckpointId (Substitution' Term) -> Doc
    forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc
    prCps Map CheckpointId (Substitution' Term)
    cps
          , Doc
    "new substs =" Doc -> Doc -> Doc
    <?> Map CheckpointId (Substitution' Term) -> Doc
    forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc
    prCps Map CheckpointId (Substitution' Term)
    cps'
          ]
      a
    x <- ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> tcm a -> (TCEnv -> TCEnv) -> tcm a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC tcm a
    k ((TCEnv -> TCEnv) -> tcm a) -> (TCEnv -> TCEnv) -> tcm a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    env -> TCEnv
    env
        { envCurrentCheckpoint :: CheckpointId
    envCurrentCheckpoint = CheckpointId
    chkpt
        , envCheckpoints :: Map CheckpointId (Substitution' Term)
    envCheckpoints       = 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 (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) (TCEnv -> Map CheckpointId (Substitution' Term)
    envCheckpoints TCEnv
    env)
        }
      Map ModuleName CheckpointId
    newMods <- Lens' (Map ModuleName CheckpointId) TCState
    -> tcm (Map ModuleName CheckpointId)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map ModuleName CheckpointId) TCState
    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..
      Lens' (Map ModuleName CheckpointId) TCState
    stModuleCheckpoints Lens' (Map ModuleName CheckpointId) TCState
    -> Map ModuleName CheckpointId -> tcm ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Map ModuleName CheckpointId
    -> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map ModuleName CheckpointId
    oldMods (CheckpointId
    old CheckpointId
    -> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Map ModuleName CheckpointId
    -> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
    forall k a b. Ord k => Map k a -> Map k b -> Map k a
    Map.difference Map ModuleName CheckpointId
    newMods Map ModuleName CheckpointId
    oldMods)
      tcm () -> tcm ()
    forall (m :: * -> *). MonadDebug m => m () -> m ()
    unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Int -> VerboseKey -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> VerboseKey -> m ()
    reportSLn VerboseKey
    "tc.cxt.checkpoint" Int
    105 VerboseKey
    "}"
      a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    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 (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' (Maybe (Substitution' Term)) TCEnv
    -> tcm (Maybe (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC ((Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    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'
         (Maybe (Substitution' Term))
         (Map CheckpointId (Substitution' Term))
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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
      Maybe CheckpointId
    mcp <- (TCState -> Lens' (Maybe CheckpointId) TCState -> Maybe CheckpointId
    forall o i. o -> Lens' i o -> i
    ^. (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
    -> TCState -> f TCState
    Lens' (Map ModuleName CheckpointId) TCState
    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' (Maybe CheckpointId) (Map ModuleName CheckpointId)
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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
      (CheckpointId -> m (Substitution' Term))
    -> Maybe CheckpointId -> m (Maybe (Substitution' Term))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse CheckpointId -> m (Substitution' Term)
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Substitution' Term)
    checkpointSubstitution Maybe CheckpointId
    mcp

    -- * Adding to the context

    {-# SPECIALIZE addCtx :: Name -> Dom Type -> TCM a -> TCM a #-}
    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' :: 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 (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)
        => Name -> Term -> Dom Type -> m a -> m a
      addLetBinding' 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
    $ Name -> Term -> Dom Type -> n (StT t a) -> n (StT t a)
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' 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 (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 VerboseKey
    x Name -> m a
    cont = do
        StT t a
    st <- (Run t -> n (StT t a)) -> t n (StT t 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 -> VerboseKey -> (Name -> n (StT t a)) -> n (StT t a)
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> m a) -> m a
    withFreshName Range
    r VerboseKey
    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
        n (StT t a) -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTransControl t, Monad m) =>
    m (StT t a) -> t m a
    restoreT (n (StT t a) -> t n a) -> n (StT t a) -> t n a
    forall a b. (a -> b) -> a -> b
    $ StT t a -> n (StT t a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return StT t a
    st

    -- | 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 (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext (Int -> Substitution' Term
    forall a. Int -> Substitution' a
    raiseS Int
    1) (((Name
    x,) (Type -> (Name, Type)) -> Dom Type -> Dom (Name, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    a) Dom (Name, Type) -> 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 =>
    VerboseKey -> (Name -> m a) -> m a
    withFreshName_ = Range -> VerboseKey -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange

    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 (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    a
      addLetBinding' :: forall a. Name -> Term -> Dom Type -> ListT m a -> ListT m a
    addLetBinding' 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
    $ Name -> Term -> Dom Type -> m a1 -> m a1
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' 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 (m :: * -> *) a.
    MonadAddContext m =>
    Substitution' Term -> (Context -> Context) -> m a -> m a
    updateContext Substitution' Term
    sub Context -> Context
    f
      withFreshName :: forall a. Range -> VerboseKey -> (Name -> ListT m a) -> ListT m a
    withFreshName Range
    r VerboseKey
    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
    -> VerboseKey
    -> (Name -> m (Maybe (a, ListT m a)))
    -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> m a) -> m a
    withFreshName Range
    r VerboseKey
    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
      VerboseKey -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCM Doc -> m ()
    reportSDoc VerboseKey
    "tc.cxt.shadowing" Int
    80 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "registered" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> Doc
    "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
      (b
    result , Map VerboseKey [VerboseKey]
    useds) <- TCM b -> TCMT IO (b, Map VerboseKey [VerboseKey])
    forall {m :: * -> *} {a}.
    (ReadTCState m, MonadTCState m) =>
    m a -> m (a, Map VerboseKey [VerboseKey])
    listenUsedNames TCM b
    f
      VerboseKey -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCM Doc -> m ()
    reportSDoc VerboseKey
    "tc.cxt.shadowing" Int
    90 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "all used names: " Doc -> Doc -> Doc
    <+> VerboseKey -> Doc
    text (Map VerboseKey [VerboseKey] -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Map VerboseKey [VerboseKey]
    useds)
      Name -> Map VerboseKey [VerboseKey] -> TCMT IO ()
    forall {m :: * -> *}.
    (MonadDebug m, MonadTCState m) =>
    Name -> Map VerboseKey [VerboseKey] -> m ()
    tellShadowing Name
    x Map VerboseKey [VerboseKey]
    useds
      b -> TCM b
    forall (m :: * -> *) a. Monad m => a -> m a
    return b
    result

        where
          listenUsedNames :: m a -> m (a, Map VerboseKey [VerboseKey])
    listenUsedNames m a
    f = do
            Map VerboseKey [VerboseKey]
    origUsedNames <- Lens' (Map VerboseKey [VerboseKey]) TCState
    -> m (Map VerboseKey [VerboseKey])
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map VerboseKey [VerboseKey]) TCState
    stUsedNames
            Lens' (Map VerboseKey [VerboseKey]) TCState
    -> Map VerboseKey [VerboseKey] -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' (Map VerboseKey [VerboseKey]) TCState
    stUsedNames Map VerboseKey [VerboseKey]
    forall k a. Map k a
    Map.empty
            a
    result <- m a
    f
            Map VerboseKey [VerboseKey]
    newUsedNames <- Lens' (Map VerboseKey [VerboseKey]) TCState
    -> m (Map VerboseKey [VerboseKey])
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map VerboseKey [VerboseKey]) TCState
    stUsedNames
            Lens' (Map VerboseKey [VerboseKey]) TCState
    -> Map VerboseKey [VerboseKey] -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' (Map VerboseKey [VerboseKey]) TCState
    stUsedNames (Map VerboseKey [VerboseKey] -> m ())
    -> Map VerboseKey [VerboseKey] -> m ()
    forall a b. (a -> b) -> a -> b
    $ ([VerboseKey] -> [VerboseKey] -> [VerboseKey])
    -> Map VerboseKey [VerboseKey]
    -> Map VerboseKey [VerboseKey]
    -> Map VerboseKey [VerboseKey]
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith [VerboseKey] -> [VerboseKey] -> [VerboseKey]
    forall a. [a] -> [a] -> [a]
    (++) Map VerboseKey [VerboseKey]
    origUsedNames Map VerboseKey [VerboseKey]
    newUsedNames
            (a, Map VerboseKey [VerboseKey])
    -> m (a, Map VerboseKey [VerboseKey])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    result , Map VerboseKey [VerboseKey]
    newUsedNames)

          tellUsedName :: Name -> m ()
    tellUsedName Name
    x = do
            let concreteX :: Name
    concreteX = Name -> Name
    nameConcrete Name
    x
                rawX :: VerboseKey
    rawX      = Name -> VerboseKey
    nameToRawName Name
    concreteX
                rootX :: VerboseKey
    rootX     = Name -> VerboseKey
    nameRoot Name
    concreteX
            Lens' (Maybe [VerboseKey]) TCState
    -> (Maybe [VerboseKey] -> Maybe [VerboseKey]) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens ((Map VerboseKey [VerboseKey] -> f (Map VerboseKey [VerboseKey]))
    -> TCState -> f TCState
    Lens' (Map VerboseKey [VerboseKey]) TCState
    stUsedNames ((Map VerboseKey [VerboseKey] -> f (Map VerboseKey [VerboseKey]))
     -> TCState -> f TCState)
    -> ((Maybe [VerboseKey] -> f (Maybe [VerboseKey]))
        -> Map VerboseKey [VerboseKey] -> f (Map VerboseKey [VerboseKey]))
    -> (Maybe [VerboseKey] -> f (Maybe [VerboseKey]))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey
    -> Lens' (Maybe [VerboseKey]) (Map VerboseKey [VerboseKey])
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key VerboseKey
    rootX) ((Maybe [VerboseKey] -> Maybe [VerboseKey]) -> m ())
    -> (Maybe [VerboseKey] -> Maybe [VerboseKey]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ [VerboseKey] -> Maybe [VerboseKey]
    forall a. a -> Maybe a
    Just ([VerboseKey] -> Maybe [VerboseKey])
    -> (Maybe [VerboseKey] -> [VerboseKey])
    -> Maybe [VerboseKey]
    -> Maybe [VerboseKey]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (VerboseKey
    rawXVerboseKey -> [VerboseKey] -> [VerboseKey]
    forall a. a -> [a] -> [a]
    :) ([VerboseKey] -> [VerboseKey])
    -> (Maybe [VerboseKey] -> [VerboseKey])
    -> Maybe [VerboseKey]
    -> [VerboseKey]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe [VerboseKey] -> [VerboseKey]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat

          tellShadowing :: Name -> Map VerboseKey [VerboseKey] -> m ()
    tellShadowing Name
    x Map VerboseKey [VerboseKey]
    useds = case VerboseKey -> Map VerboseKey [VerboseKey] -> Maybe [VerboseKey]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Name -> VerboseKey
    nameRoot (Name -> VerboseKey) -> Name -> VerboseKey
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    nameConcrete Name
    x) Map VerboseKey [VerboseKey]
    useds of
            Just [VerboseKey]
    shadows -> do
              VerboseKey -> Int -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCM Doc -> m ()
    reportSDoc VerboseKey
    "tc.cxt.shadowing" Int
    80 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "names shadowing" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> Doc
    ": " Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList_ ((VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map VerboseKey -> Doc
    forall a. Pretty a => a -> Doc
    pretty [VerboseKey]
    shadows)
              Lens' (Map Name [VerboseKey]) TCState
    -> (Map Name [VerboseKey] -> Map Name [VerboseKey]) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Map Name [VerboseKey]) TCState
    stShadowingNames ((Map Name [VerboseKey] -> Map Name [VerboseKey]) -> m ())
    -> (Map Name [VerboseKey] -> Map Name [VerboseKey]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ ([VerboseKey] -> [VerboseKey] -> [VerboseKey])
    -> Name
    -> [VerboseKey]
    -> Map Name [VerboseKey]
    -> Map Name [VerboseKey]
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith [VerboseKey] -> [VerboseKey] -> [VerboseKey]
    forall a. [a] -> [a] -> [a]
    (++) Name
    x [VerboseKey]
    shadows
            Maybe [VerboseKey]
    Nothing      -> () -> m ()
    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 a. Bool -> (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. Name -> Term -> Dom Type -> TCM a -> TCM a
    addLetBinding' Name
    x Term
    u Dom Type
    a TCM a
    ret = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
    forall a. Bool -> (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 -> Term -> Dom Type -> TCM a -> TCM a
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    Name -> Term -> Dom Type -> m a -> m a
    defaultAddLetBinding' 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 -> VerboseKey -> (Name -> TCM a) -> TCM a
    withFreshName Range
    r VerboseKey
    x Name -> TCM a
    m = Range -> VerboseKey -> TCMT IO Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    Range -> VerboseKey -> m Name
    freshName Range
    r VerboseKey
    x TCMT IO Name -> (Name -> TCM a) -> TCM a
    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
      Name
    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
      Name -> Dom Type -> m b -> m b
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    dom m b
    ret

    -- | Various specializations of @addCtx@.
    {-# SPECIALIZE addContext :: b -> TCM a -> TCM a #-}
    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 (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
    addContext)
      contextSize :: [a] -> Int
    contextSize = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Int] -> Int) -> ([a] -> [Int]) -> [a] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Int) -> [a] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Int
    forall b. AddContext b => b -> Int
    contextSize

    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 (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx
      contextSize :: (Name, Dom Type) -> Int
    contextSize (Name, Dom Type)
    _ = Int
    1

    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
    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)
    distributeF
      contextSize :: Dom (Name, Type) -> Int
    contextSize Dom (Name, Type)
    _ = Int
    1

    instance AddContext (Dom (String, Type)) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    Dom (VerboseKey, Type) -> m a -> m a
    addContext = (VerboseKey, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ((VerboseKey, Dom Type) -> m a -> m a)
    -> (Dom (VerboseKey, Type) -> (VerboseKey, Dom Type))
    -> Dom (VerboseKey, Type)
    -> m a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (VerboseKey, Type) -> (VerboseKey, Dom Type)
    forall (t :: * -> *) (m :: * -> *) a.
    (Decoration t, Functor m) =>
    t (m a) -> m (t a)
    distributeF
      contextSize :: Dom (VerboseKey, Type) -> Int
    contextSize Dom (VerboseKey, Type)
    _ = Int
    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) = Context -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ((Name -> Name) -> [Name] -> Dom Type -> Context
    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) -> Int
    contextSize ([Name]
    xs, Dom Type
    _) = [Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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) = Context -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ((Name -> Name) -> List1 Name -> Dom Type -> Context
    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) -> Int
    contextSize (List1 Name
    xs, Dom Type
    _) = List1 Name -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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
    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) -> Int
    contextSize ([WithHiding Name]
    xs, Dom Type
    _) = [WithHiding Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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
    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
    addContext ([WithHiding Name]
    xs, Int -> Dom Type -> Dom Type
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Dom Type
    dom)
      contextSize :: (NonEmpty (WithHiding Name), Dom Type) -> Int
    contextSize (NonEmpty (WithHiding Name)
    xs, Dom Type
    _) = NonEmpty (WithHiding Name) -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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
    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 NamedName Name) -> Arg Name -> NamedArg Name)
    -> (Name -> Named NamedName Name)
    -> [Arg Name]
    -> [NamedArg Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Named NamedName Name) -> Arg Name -> NamedArg Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) Name -> Named NamedName Name
    forall a name. a -> Named name a
    unnamed [Arg Name]
    xs :: [NamedArg Name], Type
    t)
      contextSize :: ([Arg Name], Type) -> Int
    contextSize ([Arg Name]
    xs, Type
    _) = [Arg Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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
    addContext (((Arg Name -> NamedArg Name)
    -> List1 (Arg Name) -> List1 (NamedArg Name)
    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 NamedName Name) -> Arg Name -> NamedArg Name)
    -> (Name -> Named NamedName Name)
    -> List1 (Arg Name)
    -> List1 (NamedArg Name)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Named NamedName Name) -> Arg Name -> NamedArg Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) Name -> Named NamedName Name
    forall a name. a -> Named name a
    unnamed List1 (Arg Name)
    xs :: List1 (NamedArg Name), Type
    t)
      contextSize :: (List1 (Arg Name), Type) -> Int
    contextSize (List1 (Arg Name)
    xs, Type
    _) = List1 (Arg Name) -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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
    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) -> Int
    contextSize ([NamedArg Name]
    xs, Type
    _) = [NamedArg Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    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
    addContext (NamedArg Name -> Name
    forall a. NamedArg a -> a
    namedArg NamedArg Name
    x, Type
    t Type -> Dom' Term () -> Dom Type
    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
    addContext ([NamedArg Name]
    xs, Int -> Type -> Type
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Type
    t)
      contextSize :: (List1 (NamedArg Name), Type) -> Int
    contextSize (List1 (NamedArg Name)
    xs, Type
    _) = List1 (NamedArg Name) -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length List1 (NamedArg Name)
    xs

    instance AddContext (String, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (VerboseKey, Dom Type) -> m a -> m a
    addContext (VerboseKey
    s, Dom Type
    dom) m a
    ret =
        Range -> VerboseKey -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange VerboseKey
    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 (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 :: (VerboseKey, Dom Type) -> Int
    contextSize (VerboseKey, Dom Type)
    _ = Int
    1

    instance AddContext (KeepNames String, Dom Type) where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    (KeepNames VerboseKey, Dom Type) -> m a -> m a
    addContext (KeepNames VerboseKey
    s, Dom Type
    dom) m a
    ret =
        Range -> VerboseKey -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> VerboseKey -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange VerboseKey
    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 (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Dom Type -> m a -> m a
    addCtx Name
    x Dom Type
    dom m a
    ret
      contextSize :: (KeepNames VerboseKey, Dom Type) -> Int
    contextSize (KeepNames VerboseKey, Dom Type)
    _ = Int
    1

    instance AddContext (Dom Type) where
      addContext :: forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
    addContext Dom Type
    dom = (VerboseKey, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (VerboseKey
    "_" :: String, Dom Type
    dom)
      contextSize :: Dom Type -> Int
    contextSize Dom Type
    _ = Int
    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
    addContext (Name
    x, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__)
      contextSize :: Name -> Int
    contextSize Name
    _ = Int
    1

    instance {-# OVERLAPPING #-} AddContext String where
      addContext :: forall (m :: * -> *) a.
    MonadAddContext m =>
    VerboseKey -> m a -> m a
    addContext VerboseKey
    s = (VerboseKey, Dom Type) -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (VerboseKey
    s, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__)
      contextSize :: VerboseKey -> Int
    contextSize VerboseKey
    _ = Int
    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) = (VerboseKey -> KeepNames VerboseKey)
    -> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' VerboseKey -> KeepNames VerboseKey
    forall a. a -> KeepNames a
    KeepNames Dom Type
    t Abs Telescope
    tel Telescope -> m a
    loop
      contextSize :: KeepNames Telescope -> Int
    contextSize (KeepNames Telescope
    tel) = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel

    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) = (VerboseKey -> VerboseKey)
    -> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' VerboseKey -> VerboseKey
    forall a. a -> a
    id Dom Type
    t Abs Telescope
    tel Telescope -> m a
    loop
      contextSize :: Telescope -> Int
    contextSize = Telescope -> Int
    forall a. Sized a => a -> Int
    size

    -- | 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 = (VerboseKey -> VerboseKey)
    -> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' VerboseKey -> VerboseKey
    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)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction' VerboseKey -> name
    _ Dom Type
    _ (NoAbs VerboseKey
    _ a
    v) a -> m b
    k = a -> m b
    k a
    v
    underAbstraction' VerboseKey -> name
    wrap Dom Type
    t Abs a
    a a -> m b
    k = (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' VerboseKey -> 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 = (VerboseKey -> VerboseKey)
    -> Dom Type -> Abs a -> (a -> m b) -> m b
    forall a (m :: * -> *) name b.
    (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' VerboseKey -> VerboseKey
    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)) =>
    (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs' VerboseKey -> 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
    addContext (VerboseKey -> name
    wrap (VerboseKey -> name) -> VerboseKey -> name
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseKey
    realName (VerboseKey -> VerboseKey) -> VerboseKey -> VerboseKey
    forall a b. (a -> b) -> a -> b
    $ Abs a -> VerboseKey
    forall a. Abs a -> VerboseKey
    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 :: VerboseKey -> VerboseKey
    realName VerboseKey
    s = if VerboseKey -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName VerboseKey
    s then VerboseKey
    "x" else VerboseKey -> VerboseKey
    argNameToString VerboseKey
    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

    getLetBindings :: MonadTCM tcm => tcm [(Name,(Term,Dom Type))]
    getLetBindings :: forall (tcm :: * -> *).
    MonadTCM tcm =>
    tcm [(Name, (Term, Dom Type))]
    getLetBindings = do
      Map Name (Open (Term, Dom Type))
    bs <- (TCEnv -> Map Name (Open (Term, Dom Type)))
    -> tcm (Map Name (Open (Term, Dom Type)))
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Map Name (Open (Term, Dom Type))
    envLetBindings
      [(Name, Open (Term, Dom Type))]
    -> ((Name, Open (Term, Dom Type)) -> tcm (Name, (Term, Dom Type)))
    -> tcm [(Name, (Term, Dom Type))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Map Name (Open (Term, Dom Type)) -> [(Name, Open (Term, Dom Type))]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name (Open (Term, Dom Type))
    bs) (((Name, Open (Term, Dom Type)) -> tcm (Name, (Term, Dom Type)))
     -> tcm [(Name, (Term, Dom Type))])
    -> ((Name, Open (Term, Dom Type)) -> tcm (Name, (Term, Dom Type)))
    -> tcm [(Name, (Term, Dom Type))]
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    n,Open (Term, Dom Type)
    o) -> (,) Name
    n ((Term, Dom Type) -> (Name, (Term, Dom Type)))
    -> tcm (Term, Dom Type) -> tcm (Name, (Term, Dom Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Open (Term, Dom Type) -> tcm (Term, Dom Type)
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen Open (Term, Dom Type)
    o

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

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

    -- * Querying the context

    -- | Get the current context.
    {-# SPECIALIZE getContext :: TCM [Dom (Name, Type)] #-}
    getContext :: MonadTCEnv m => m [Dom (Name, Type)]
    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 :: (Applicative m, MonadTCEnv m) => m Nat
    getContextSize :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize = Context -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Context -> Int) -> m Context -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Context) -> m Context
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Context
    envContext

    -- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
    {-# SPECIALIZE getContextArgs :: TCM Args #-}
    getContextArgs :: (Applicative m, MonadTCEnv m) => m Args
    getContextArgs :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs = Args -> Args
    forall a. [a] -> [a]
    reverse (Args -> Args) -> (Context -> Args) -> Context -> Args
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Dom (Name, Type) -> Arg Term) -> [Int] -> Context -> Args
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> Dom (Name, Type) -> Arg Term
    forall {t} {b}. Int -> Dom' t b -> Arg Term
    mkArg [Int
    0..] (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
      where mkArg :: Int -> Dom' t b -> Arg Term
    mkArg Int
    i Dom' t b
    dom = Int -> Term
    var Int
    i Term -> Arg b -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom' t b -> Arg b
    forall t a. Dom' t a -> Arg a
    argFromDom Dom' t b
    dom

    -- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
    {-# SPECIALIZE getContextTerms :: TCM [Term] #-}
    getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
    getContextTerms :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
    getContextTerms = (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Term
    var ([Int] -> [Term]) -> (Int -> [Int]) -> Int -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Term]) -> m Int -> m [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize

    -- | Get the current context as a 'Telescope'.
    {-# SPECIALIZE getContextTelescope :: TCM Telescope #-}
    getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope = (Name -> VerboseKey) -> Context -> Telescope
    forall a. (a -> VerboseKey) -> ListTel' a -> Telescope
    telFromList' Name -> VerboseKey
    nameToArgName (Context -> Telescope)
    -> (Context -> Context) -> Context -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> Context
    forall a. [a] -> [a]
    reverse (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

    -- | Get the names of all declarations in the context.
    {-# SPECIALIZE getContextNames :: TCM [Name] #-}
    getContextNames :: (Applicative m, MonadTCEnv m) => m [Name]
    getContextNames :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
    getContextNames = (Dom (Name, Type) -> Name) -> Context -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) (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

    -- | get type of bound variable (i.e. deBruijn index)
    --
    {-# SPECIALIZE lookupBV' :: Nat -> TCM (Maybe (Dom (Name, Type))) #-}
    lookupBV' :: MonadTCEnv m => Nat -> m (Maybe (Dom (Name, Type)))
    lookupBV' :: forall (m :: * -> *).
    MonadTCEnv m =>
    Int -> m (Maybe (Dom (Name, Type)))
    lookupBV' Int
    n = do
      Context
    ctx <- m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
      Maybe (Dom (Name, Type)) -> m (Maybe (Dom (Name, Type)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Dom (Name, Type)) -> m (Maybe (Dom (Name, Type))))
    -> Maybe (Dom (Name, Type)) -> m (Maybe (Dom (Name, Type)))
    forall a b. (a -> b) -> a -> b
    $ Int -> Dom (Name, Type) -> Dom (Name, Type)
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (Dom (Name, Type) -> Dom (Name, Type))
    -> Maybe (Dom (Name, Type)) -> Maybe (Dom (Name, Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Context
    ctx Context -> Int -> Maybe (Dom (Name, Type))
    forall a. [a] -> Int -> Maybe a
    !!! Int
    n

    {-# SPECIALIZE lookupBV :: Nat -> TCM (Dom (Name, Type)) #-}
    lookupBV :: (MonadFail m, MonadTCEnv m) => Nat -> m (Dom (Name, Type))
    lookupBV :: forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m) =>
    Int -> m (Dom (Name, Type))
    lookupBV Int
    n = do
      let failure :: m (Dom (Name, Type))
    failure = do
            Context
    ctx <- m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
            VerboseKey -> m (Dom (Name, Type))
    forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
    fail (VerboseKey -> m (Dom (Name, Type)))
    -> VerboseKey -> m (Dom (Name, Type))
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "de Bruijn index out of scope: " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Int -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Int
    n VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++
                   VerboseKey
    " in context " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ [Name] -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow ((Dom (Name, Type) -> Name) -> Context -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) Context
    ctx)
      m (Dom (Name, Type))
    -> (Dom (Name, Type) -> m (Dom (Name, Type)))
    -> m (Maybe (Dom (Name, Type)))
    -> m (Dom (Name, Type))
    forall (m :: * -> *) b a.
    Monad m =>
    m b -> (a -> m b) -> m (Maybe a) -> m b
    maybeM m (Dom (Name, Type))
    failure Dom (Name, Type) -> m (Dom (Name, Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (m (Maybe (Dom (Name, Type))) -> m (Dom (Name, Type)))
    -> m (Maybe (Dom (Name, Type))) -> m (Dom (Name, Type))
    forall a b. (a -> b) -> a -> b
    $ Int -> m (Maybe (Dom (Name, Type)))
    forall (m :: * -> *).
    MonadTCEnv m =>
    Int -> m (Maybe (Dom (Name, Type)))
    lookupBV' Int
    n

    {-# SPECIALIZE domOfBV :: Nat -> TCM (Dom Type) #-}
    domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type)
    domOfBV :: forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    n = ((Name, Type) -> Type) -> Dom (Name, Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name, Type) -> Type
    forall a b. (a, b) -> b
    snd (Dom (Name, Type) -> Dom Type)
    -> m (Dom (Name, Type)) -> m (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Dom (Name, Type))
    forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m) =>
    Int -> m (Dom (Name, Type))
    lookupBV Int
    n

    {-# SPECIALIZE typeOfBV :: Nat -> TCM Type #-}
    typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type
    typeOfBV :: forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m Type
    typeOfBV Int
    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
    <$> Int -> m (Dom Type)
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    i

    {-# SPECIALIZE nameOfBV' :: Nat -> TCM (Maybe Name) #-}
    nameOfBV' :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Maybe Name)
    nameOfBV' :: forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m (Maybe Name)
    nameOfBV' Int
    n = (Dom (Name, Type) -> Name)
    -> Maybe (Dom (Name, Type)) -> Maybe Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) (Maybe (Dom (Name, Type)) -> Maybe Name)
    -> m (Maybe (Dom (Name, Type))) -> m (Maybe Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Maybe (Dom (Name, Type)))
    forall (m :: * -> *).
    MonadTCEnv m =>
    Int -> m (Maybe (Dom (Name, Type)))
    lookupBV' Int
    n

    {-# SPECIALIZE nameOfBV :: Nat -> TCM Name #-}
    nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name
    nameOfBV :: forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m Name
    nameOfBV Int
    n = (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom (Dom (Name, Type) -> Name) -> m (Dom (Name, Type)) -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Dom (Name, Type))
    forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m) =>
    Int -> m (Dom (Name, Type))
    lookupBV Int
    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 :: (MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type)
    getVarInfo :: forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m) =>
    Name -> m (Term, Dom Type)
    getVarInfo Name
    x =
        do  Context
    ctx <- m Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
            Map Name (Open (Term, Dom Type))
    def <- (TCEnv -> Map Name (Open (Term, Dom Type)))
    -> m (Map Name (Open (Term, Dom Type)))
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Map Name (Open (Term, Dom Type))
    envLetBindings
            case (Dom (Name, Type) -> Bool) -> Context -> Maybe Int
    forall a. (a -> Bool) -> [a] -> Maybe Int
    List.findIndex ((Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    ==Name
    x) (Name -> Bool)
    -> (Dom (Name, Type) -> Name) -> Dom (Name, Type) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) Context
    ctx of
                Just Int
    n -> do
                    Dom Type
    t <- Int -> m (Dom Type)
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    n
                    (Term, Dom Type) -> m (Term, Dom Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Term
    var Int
    n, Dom Type
    t)
                Maybe Int
    _       ->
                    case Name
    -> Map Name (Open (Term, Dom Type))
    -> Maybe (Open (Term, Dom Type))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Map Name (Open (Term, Dom Type))
    def of
                        Just Open (Term, Dom Type)
    vt -> Open (Term, Dom Type) -> m (Term, Dom Type)
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen Open (Term, Dom Type)
    vt
                        Maybe (Open (Term, Dom Type))
    _       -> VerboseKey -> m (Term, Dom Type)
    forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
    fail (VerboseKey -> m (Term, Dom Type))
    -> VerboseKey -> m (Term, Dom Type)
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "unbound variable " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Name -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow (Name -> Name
    nameConcrete Name
    x) VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++
                                    VerboseKey
    " (id: " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ NameId -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow (Name -> NameId
    nameId Name
    x) VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ")"