    {-# OPTIONS_GHC -Wunused-imports #-}

    -- Initially authored by Andreas, 2013-10-22.

    -- | A bidirectional type checker for internal syntax.
    --
    --   Performs checking on unreduced terms.
    --   With the exception that projection-like function applications
    --   have to be reduced since they break bidirectionality.

    module Agda.TypeChecking.CheckInternal
      ( MonadCheckInternal
      , checkType, infer, inferSpine
      , CheckInternal(..)
      , Action(..), defaultAction, eraseUnusedAction
      ) where

    import Control.Monad

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Common.Pretty (prettyShow)

    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.ProjectionLike (elimView, ProjEliminator(..))
    import Agda.TypeChecking.Records (shouldBeProjectible)
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Sort
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Function (applyWhen, applyWhenM)
    import Agda.Utils.Functor (($>))
    import Agda.Utils.Maybe
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    import Agda.Interaction.Options

    -- * Bidirectional rechecker

    type MonadCheckInternal m = MonadConversion m

    {-# SPECIALIZE checkType :: Type -> TCM () #-}
    -- | Entry point for e.g. checking WithFunctionType.
    checkType :: (MonadCheckInternal m) => Type -> m ()
    checkType :: forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
    checkType Type
    t = Constraint -> m () -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Constraint -> m () -> m ()
    catchConstraint (Type -> Constraint
    CheckType Type
    t) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Type -> m ()
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    a -> m ()
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf Type ~ ()) =>
    Type -> m ()
    inferInternal Type
    t

    -- | 'checkInternal' traverses the whole 'Term', and we can use this
    --   traversal to modify the term.
    data Action m = Action
      { forall (m :: * -> *). Action m -> Type -> Term -> m Term
    preAction  :: Type -> Term -> m Term
        -- ^ Called on each subterm before the checker runs.
      , forall (m :: * -> *). Action m -> Type -> Term -> m Term
    postAction :: Type -> Term -> m Term
        -- ^ Called on each subterm after the type checking.
      , forall (m :: * -> *). Action m -> Modality -> Modality -> Modality
    modalityAction :: Modality -> Modality -> Modality
        -- ^ Called for each @ArgInfo@.
        --   The first 'Modality' is from the type,
        --   the second from the term.
      , forall (m :: * -> *). Action m -> Term -> m Term
    elimViewAction :: Term -> m Term
        -- ^ Called for bringing projection-like funs in post-fix form
      }

    -- | The default action is to not change the 'Term' at all.
    defaultAction :: PureTCM m => Action m
    --(MonadReduce m, MonadTCEnv m, HasConstInfo m) => Action m
    defaultAction :: forall (m :: * -> *). PureTCM m => Action m
    defaultAction = Action
      { preAction :: Type -> Term -> m Term
    preAction       = \ Type
    _ -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      , postAction :: Type -> Term -> m Term
    postAction      = \ Type
    _ -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      , modalityAction :: Modality -> Modality -> Modality
    modalityAction  = \ Modality
    _ -> Modality -> Modality
    forall a. a -> a
    id
      , elimViewAction :: Term -> m Term
    elimViewAction  = ProjEliminator -> Term -> m Term
    forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    EvenLone
      }

    eraseUnusedAction :: Action TCM
    eraseUnusedAction :: Action TCM
    eraseUnusedAction = Action TCM
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction { postAction = eraseUnused }
      where
        eraseUnused :: Type -> Term -> TCM Term
        eraseUnused :: Type -> Term -> TCM Term
    eraseUnused Type
    t = \case
          Def QName
    f Elims
    es -> do
            pols <- QName -> TCMT IO [Polarity]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
    getPolarity QName
    f
            return $ Def f $ eraseIfNonvariant pols es
          Term
    v        -> Term -> TCM Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

        eraseIfNonvariant :: [Polarity] -> Elims -> Elims
        eraseIfNonvariant :: [Polarity] -> Elims -> Elims
    eraseIfNonvariant []                  Elims
    es             = Elims
    es
        eraseIfNonvariant [Polarity]
    pols                []             = []
        eraseIfNonvariant (Polarity
    Nonvariant : [Polarity]
    pols) (Elim
    e : Elims
    es) = ((Term -> Term) -> Elim -> Elim
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Term
    dontCare Elim
    e) Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : [Polarity] -> Elims -> Elims
    eraseIfNonvariant [Polarity]
    pols Elims
    es
        eraseIfNonvariant (Polarity
    _          : [Polarity]
    pols) (Elim
    e : Elims
    es) = Elim
    e Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : [Polarity] -> Elims -> Elims
    eraseIfNonvariant [Polarity]
    pols Elims
    es

    class CheckInternal a where
      checkInternal' :: (MonadCheckInternal m) => Action m -> a -> Comparison -> TypeOf a -> m a

      checkInternal :: (MonadCheckInternal m) => a -> Comparison -> TypeOf a -> m ()
      checkInternal a
    v Comparison
    cmp TypeOf a
    t = m a -> m ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (m a -> m ()) -> m a -> m ()
    forall a b. (a -> b) -> a -> b
    $ Action m -> a -> Comparison -> TypeOf a -> m a
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    Action m -> a -> Comparison -> TypeOf a -> m a
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> a -> Comparison -> TypeOf a -> m a
    checkInternal' Action m
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction a
    v Comparison
    cmp TypeOf a
    t

      inferInternal' :: (MonadCheckInternal m, TypeOf a ~ ()) => Action m -> a -> m a
      inferInternal' Action m
    act a
    v = Action m -> a -> Comparison -> TypeOf a -> m a
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    Action m -> a -> Comparison -> TypeOf a -> m a
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> a -> Comparison -> TypeOf a -> m a
    checkInternal' Action m
    act a
    v Comparison
    CmpEq ()

      inferInternal :: (MonadCheckInternal m, TypeOf a ~ ()) => a -> m ()
      inferInternal a
    v = a -> Comparison -> TypeOf a -> m ()
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    a -> Comparison -> TypeOf a -> m ()
    forall (m :: * -> *).
    MonadCheckInternal m =>
    a -> Comparison -> TypeOf a -> m ()
    checkInternal a
    v Comparison
    CmpEq ()

    {-# SPECIALIZE checkInternal' :: Action TCM -> Term  -> Comparison -> TypeOf Term -> TCM Term #-}
    {-# SPECIALIZE checkInternal' :: Action TCM -> Type  -> Comparison -> TypeOf Type -> TCM Type #-}
    {-# SPECIALIZE checkInternal' :: Action TCM -> Elims -> Comparison -> TypeOf Type -> TCM Elims #-}
    {-# SPECIALIZE checkInternal  :: Term -> Comparison -> TypeOf Term -> TCM () #-}
    {-# SPECIALIZE checkInternal  :: Type -> Comparison -> TypeOf Type -> TCM () #-}

    instance CheckInternal Type where
      checkInternal' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Comparison -> TypeOf Type -> m Type
    checkInternal' Action m
    action (El Sort' Term
    s Term
    t) Comparison
    cmp TypeOf Type
    _ = do
        t' <- Action m -> Term -> Comparison -> TypeOf Term -> m Term
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    Action m -> a -> Comparison -> TypeOf a -> m a
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> TypeOf Term -> m Term
    checkInternal' Action m
    action Term
    t Comparison
    cmp (Sort' Term -> Type
    sort Sort' Term
    s)
        s' <- sortOf t'
        compareSort cmp s' s
        return (El s t')

    instance CheckInternal Term where
      checkInternal' :: (MonadCheckInternal m) => Action m -> Term -> Comparison -> Type -> m Term
      checkInternal' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    v Comparison
    cmp Type
    t = String -> Int -> String -> m Term -> m Term
    forall a. String -> Int -> String -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Int -> String -> m a -> m a
    verboseBracket String
    "tc.check.internal" Int
    20 String
    "" (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ do

        -- Debug print
        String -> Int -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
    verboseS String
    "tc.check.internal" Int
    20 do
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.check.internal" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "checking internal "
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t ] ]
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.check.internal" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "checking internal with DB indices"
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t ] ]
          ctx <- m Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
          unless (null ctx) $ reportSDoc "tc.check.internal" 30 $ sep
            [ "In context"
            , nest 2 $ sep [ prettyTCM ctx ] ]

        -- Bring projection-like funs in post-fix form,
        -- (even lone ones by default).
        v <- Action m -> Term -> m Term
    forall (m :: * -> *). Action m -> Term -> m Term
    elimViewAction Action m
    action (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Action m -> Type -> Term -> m Term
    forall (m :: * -> *). Action m -> Type -> Term -> m Term
    preAction Action m
    action Type
    t Term
    v
        postAction action t =<< case v of
          Var Int
    i Elims
    es   -> do
            d <- Int -> m (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    i
            n <- nameOfBV i

            -- Lucas, 23-11-2022:
            -- For now we only check if pure modalities are respected.
            -- In the future we SHOULD also be doing the same checks for every modality, as in Rules/Applications.hs
            -- (commented below)
            -- but this will break stuff that is allowed right now

            unless (usableCohesion d) $
              typeError $ VariableIsOfUnusableCohesion n (getCohesion d)

            unless (usablePolarity d) $
              typeError $ VariableIsOfUnusablePolarity n (getModalPolarity d)

            reportSDoc "tc.check.internal" 30 $ fsep
              [ "variable" , prettyTCM (var i) , "has type" , prettyTCM (unDom d)
              , "and modality", pretty (getModality d) ]
            checkSpine action (unDom d) (Var i) es cmp t
          Def QName
    f Elims
    es   -> do  -- f is not projection(-like)!
            -- There is no "implicitely applied module telescope" at this stage, so no
            -- need to check it for modal errors, everything is covered by the
            -- variable rule!
            a <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
            checkSpine action a (Def f) es cmp t
          MetaV MetaId
    x Elims
    es -> do -- we assume meta instantiations to be well-typed
            a <- MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x
            reportSDoc "tc.check.internal" 30 $ "metavariable" <+> prettyTCM x <+> "has type" <+> prettyTCM a
            checkSpine action a (MetaV x) es cmp t
          Con ConHead
    c ConInfo
    ci Elims
    vs -> do
            -- We need to fully apply the constructor to make getConType work!
            ConHead
    -> Elims
    -> Type
    -> (QName
        -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m Term)
    -> m Term
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    ConHead
    -> Elims
    -> Type
    -> (QName
        -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
    -> m a
    fullyApplyCon ConHead
    c Elims
    vs Type
    t ((QName
      -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m Term)
     -> m Term)
    -> (QName
        -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m Term)
    -> m Term
    forall a b. (a -> b) -> a -> b
    $ \ QName
    _d Type
    _dt Args
    _pars Type
    a Elims
    vs' Telescope
    tel Type
    t -> do
              Action m
    -> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
    checkSpine Action m
    action Type
    a (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) Elims
    vs' Comparison
    cmp Type
    t m Term -> (Term -> m Term) -> m Term
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Con ConHead
    c ConInfo
    ci Elims
    vs2 ->
                  -- Strip away the extra arguments
                  Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Impossible -> Int -> Substitution' Term
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel))
                    (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Elims
    forall a. Int -> [a] -> [a]
    take (Elims -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Elims
    vs) Elims
    vs2
                Term
    _ -> m Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lit Literal
    l      -> do
            lt <- Literal -> m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    Literal -> m Type
    litType Literal
    l
            compareType cmp lt t
            return $ Lit l
          Lam ArgInfo
    ai Abs Term
    vb  -> do
            (a, b) <- Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    Type -> m (Dom Type, Abs Type)
    shouldBePiOrPath Type
    t
            ai <- checkArgInfo action ai $ domInfo a
            let name = [Suggestion] -> String
    suggests [ Abs Term -> Suggestion
    forall a. Suggest a => a -> Suggestion
    Suggestion Abs Term
    vb , Abs Type -> Suggestion
    forall a. Suggest a => a -> Suggestion
    Suggestion Abs Type
    b ]
            addContext (name, a) $ do
              Lam ai . Abs (absName vb) <$> checkInternal' action (absBody vb) cmp (absBody b)
          Pi Dom Type
    a Abs Type
    b     -> do
            s <- Type -> m (Sort' Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadError TCErr m) =>
    Type -> m (Sort' Term)
    shouldBeSort Type
    t
            reportSDoc "tc.check.internal" 30 $ "pi type should have sort" <+> prettyTCM s
            when (s == SizeUniv) $ typeError $ FunctionTypeInSizeUniv v
            experimental <- optExperimentalIrrelevance <$> pragmaOptions
            let sa  = Dom Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort Dom Type
    a
                sb  = Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b)
                mkDom Term
    v = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    sa Term
    v Type -> Dom Type -> Dom Type
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type
    a
                mkRng Term
    v = (Type -> Type) -> Abs Type -> Abs Type
    forall a b. (a -> b) -> Abs a -> Abs b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term
    v Term -> Type -> Type
    forall a b. a -> Type'' Term b -> Type'' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) Abs Type
    b
                -- Preserve NoAbs
                goInside = case Abs Type
    b of
                  Abs{}   -> (String, Dom Type) -> m Term -> m Term
    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 Term -> m Term)
    -> (String, Dom Type) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b,) (Dom Type -> (String, Dom Type)) -> Dom Type -> (String, Dom Type)
    forall a b. (a -> b) -> a -> b
    $
                    PolarityModality -> Dom Type -> Dom Type
    forall a. LensModalPolarity a => PolarityModality -> a -> a
    inverseApplyPolarity (ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    UnusedPolarity) (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $
                    Bool -> (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    experimental ((Relevance -> Relevance) -> Dom Type -> Dom Type
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance Relevance -> Relevance
    irrelevantToShapeIrrelevant) Dom Type
    a
                  NoAbs{} -> m Term -> m Term
    forall a. a -> a
    id
            a <- applyWhenM (optPolarity <$> pragmaOptions) (applyPolarityToContext negativePolarity) $
                   mkDom <$> checkInternal' action (unEl $ unDom a) CmpLeq (sort sa)
            v' <- goInside $ Pi a . mkRng <$> checkInternal' action (unEl $ unAbs b) CmpLeq (sort sb)
            s' <- sortOf v -- Issue #6205: do not use v' since it might not be valid syntax
            compareSort cmp s' s
            return v'
          Sort Sort' Term
    s     -> do
            String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.check.internal" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checking sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort' Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort' Term -> m Doc
    prettyTCM Sort' Term
    s
            s <- Action m -> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf (Sort' Term) ~ ()) =>
    Action m -> Sort' Term -> m (Sort' Term)
    inferInternal' Action m
    action Sort' Term
    s
            s' <- inferUnivSort s
            s'' <- shouldBeSort t
            compareSort cmp s' s''
            return $ Sort s
          Level Level
    l    -> do
            l <- Action m -> Level -> m Level
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf Level ~ ()) =>
    Action m -> Level -> m Level
    inferInternal' Action m
    action Level
    l
            lt <- levelType'
            compareType cmp lt t
            return $ Level l
          DontCare Term
    v -> Term -> Term
    DontCare (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Term -> Comparison -> TypeOf Term -> m Term
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    Action m -> a -> Comparison -> TypeOf a -> m a
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> TypeOf Term -> m Term
    checkInternal' Action m
    action Term
    v Comparison
    cmp TypeOf Term
    Type
    t
          -- Jesper, 2023-02-23: these can appear because of eta-expansion of
          -- records with irrelevant fields
          Dummy String
    s Elims
    _ -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v -- __IMPOSSIBLE_VERBOSE__ s

    -- | @checkArgInfo actual expected@.
    --
    --   The @expected@ 'ArgInfo' comes from the type.
    --   The @actual@ 'ArgInfo' comes from the term and can be updated
    --   by an action.
    checkArgInfo :: (MonadCheckInternal m) => Action m -> ArgInfo -> ArgInfo -> m ArgInfo
    checkArgInfo :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> ArgInfo -> ArgInfo -> m ArgInfo
    checkArgInfo Action m
    action ArgInfo
    ai ArgInfo
    ai' = do
      Hiding -> Hiding -> m ()
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Hiding -> Hiding -> m ()
    checkHiding    (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    ai)     (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    ai')
      mod <- Action m -> Modality -> Modality -> m Modality
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Modality -> Modality -> m Modality
    checkModality Action m
    action (ArgInfo -> Modality
    forall a. LensModality a => a -> Modality
    getModality ArgInfo
    ai)  (ArgInfo -> Modality
    forall a. LensModality a => a -> Modality
    getModality ArgInfo
    ai')
      return $ setModality mod ai

    checkHiding :: (MonadCheckInternal m) => Hiding -> Hiding -> m ()
    checkHiding :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Hiding -> Hiding -> m ()
    checkHiding Hiding
    h Hiding
    h' = Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Hiding -> Hiding -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding Hiding
    h Hiding
    h') (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ Hiding -> Hiding -> TypeError
    HidingMismatch Hiding
    h Hiding
    h'

    -- | @checkRelevance action term type@.
    --
    --   The @term@ 'Relevance' can be updated by the @action@.
    checkModality :: (MonadCheckInternal m) => Action m -> Modality -> Modality -> m Modality
    checkModality :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Modality -> Modality -> m Modality
    checkModality Action m
    action Modality
    mod Modality
    mod' = do
      let (Relevance
    r,Relevance
    r') = (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod, Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod')
          (Quantity
    q,Quantity
    q') = (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  Modality
    mod, Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  Modality
    mod')
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Modality -> Modality -> Bool
    forall a b. (LensModality a, LensModality b) => a -> b -> Bool
    sameModality Modality
    mod Modality
    mod') (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ if
        | Bool -> Bool
    not (Relevance -> Relevance -> Bool
    sameRelevance Relevance
    r Relevance
    r') -> Relevance -> Relevance -> TypeError
    RelevanceMismatch Relevance
    r Relevance
    r'
        | Bool -> Bool
    not (Quantity -> Quantity -> Bool
    sameQuantity Quantity
    q Quantity
    q')  -> Quantity -> Quantity -> TypeError
    QuantityMismatch  Quantity
    q Quantity
    q'
        | Bool
    otherwise -> TypeError
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- add more cases when adding new modalities
      Modality -> m Modality
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Modality -> m Modality) -> Modality -> m Modality
    forall a b. (a -> b) -> a -> b
    $ Action m -> Modality -> Modality -> Modality
    forall (m :: * -> *). Action m -> Modality -> Modality -> Modality
    modalityAction Action m
    action Modality
    mod' Modality
    mod  -- Argument order for actions: @type@ @term@

    {-# SPECIALIZE infer :: Term -> TCM Type #-}
    -- | Infer type of a neutral term.
    infer :: (MonadCheckInternal m) => Term -> m Type
    infer :: forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
    infer Term
    u = do
      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.check.internal" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "CheckInternal.infer" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
      case Term
    u of
        Var Int
    i Elims
    es -> do
          a <- Int -> m Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
          fst <$> inferSpine defaultAction a (Var i) es
        Def QName
    f Elims
    es -> do
          m (Maybe Projection) -> (Projection -> m ()) -> m ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (QName -> m (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f) ((Projection -> m ()) -> m ()) -> (Projection -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \Projection
    _ -> m ()
    forall (m :: * -> *) a. MonadDebug m => m a
    nonInferable
          a <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
          fst <$> inferSpine defaultAction a (Def f) es
        MetaV MetaId
    x Elims
    es -> do -- we assume meta instantiations to be well-typed
          a <- MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x
          fst <$> inferSpine defaultAction a (MetaV x) es
        Term
    _ -> m Type
    forall (m :: * -> *) a. MonadDebug m => m a
    nonInferable
      where
        nonInferable :: MonadDebug m => m a
        nonInferable :: forall (m :: * -> *) a. MonadDebug m => m a
    nonInferable = String -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
          [ String
    "CheckInternal.infer: non-inferable term:"
          , String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Term -> String
    forall a. Pretty a => a -> String
    prettyShow Term
    u
          ]

    instance CheckInternal Elims where
      checkInternal' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims
    checkInternal' Action m
    action Elims
    es Comparison
    cmp (Type
    t , Elims -> Term
    hd) = (Type, Elims) -> Elims
    forall a b. (a, b) -> b
    snd ((Type, Elims) -> Elims) -> m (Type, Elims) -> m Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
    inferSpine Action m
    action Type
    t Elims -> Term
    hd Elims
    es

    {-# SPECIALIZE inferSpine :: Action TCM -> Type -> (Elims -> Term) -> Elims -> TCM (Type, Elims) #-}
    -- | @inferSpine action t hd es@ checks that spine @es@ eliminates
    --   value @hd []@ of type @t@ and returns the remaining type
    --   (target of elimination) and the transformed eliminations.
    inferSpine :: (MonadCheckInternal m) => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
    inferSpine :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
    inferSpine Action m
    action Type
    t Elims -> Term
    hd Elims
    es = Type
    -> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
    loop Type
    t Elims -> Term
    hd Elims -> Elims
    forall a. a -> a
    id Elims
    es
      where
      loop :: Type
    -> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
    loop Type
    t Elims -> Term
    hd Elims -> Elims
    acc = \case
        [] -> (Type, Elims) -> m (Type, Elims)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    t , Elims -> Elims
    acc [])
        (Elim
    e : Elims
    es) -> do
          let self :: Term
    self = Elims -> Term
    hd []
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.check.internal" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "inferring spine: "
            , TCMT IO Doc
    "type t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
            , TCMT IO Doc
    "self  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    self
            , TCMT IO Doc
    "eliminated by e = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM Elim
    e
            ]
          case Elim
    e of
            IApply Term
    x Term
    y Term
    r -> do
              (a, b) <- Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    Type -> m (Dom Type, Abs Type)
    shouldBePath Type
    t
              r' <- checkInternal' action r CmpLeq (unDom a)
              izero <- primIZero
              ione  <- primIOne
              x' <- checkInternal' action x CmpLeq (b `absApp` izero)
              y' <- checkInternal' action y CmpLeq (b `absApp` ione)
              let e' = Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply Term
    x' Term
    y' Term
    r'
              loop (b `absApp` r) (hd . (e:)) (acc . (e':)) es
            Apply (Arg ArgInfo
    ai Term
    v) -> do
              (a, b) <- Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    Type -> m (Dom Type, Abs Type)
    shouldBePi Type
    t
              ai <- checkArgInfo action ai $ domInfo a
              v' <- applyModalityToContext (getModality a) $ checkInternal' action v CmpLeq $ unDom a
              let e' = Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    v')
              loop (b `absApp` v) (hd . (e:)) (acc . (e':)) es
            -- case: projection or projection-like
            Proj ProjOrigin
    o QName
    f -> do
              t' <- Term -> Type -> ProjOrigin -> QName -> m Type
    forall (m :: * -> *).
    (PureTCM m, MonadTCError m, MonadBlock m) =>
    Term -> Type -> ProjOrigin -> QName -> m Type
    shouldBeProjectible Term
    self Type
    t ProjOrigin
    o QName
    f
              loop t' (hd . (e:)) (acc . (e:)) es

    {-# SPECIALIZE checkSpine :: Action TCM -> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> TCM Term #-}
    checkSpine
      :: (MonadCheckInternal m)
      => Action m
      -> Type       -- ^ Type of the head @self@.
      -> (Elims -> Term) -- ^ The head @hd@.
      -> Elims      -- ^ The eliminations @es@.
      -> Comparison -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the final type.
      -> Type       -- ^ Expected type of the application @self es@.
      -> m Term     -- ^ The application after modification by the @Action@.
    checkSpine :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
    checkSpine Action m
    action Type
    a Elims -> Term
    hd Elims
    es Comparison
    cmp Type
    t = do
      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.check.internal" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ TCMT IO Doc
    "checking spine "
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Elims -> Term
    hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                                     , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a ])
                       , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Elims -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elims -> m Doc
    prettyTCM Elims
    es TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                       , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t ] ]
      (t' , es') <- Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
    inferSpine Action m
    action Type
    a Elims -> Term
    hd Elims
    es
      coerceSize (compareType cmp) (hd es) t' t
      return $ hd es'

    instance CheckInternal Sort where
      checkInternal' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Sort' Term
    -> Comparison
    -> TypeOf (Sort' Term)
    -> m (Sort' Term)
    checkInternal' Action m
    action Sort' Term
    s Comparison
    cmp TypeOf (Sort' Term)
    _ = case Sort' Term
    s of
        Univ Univ
    u Level
    l -> Univ -> Level -> Sort' Term
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (Level -> Sort' Term) -> m Level -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Level -> m Level
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf Level ~ ()) =>
    Action m -> Level -> m Level
    inferInternal' Action m
    action Level
    l
        Inf Univ
    u Integer
    n  -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort' Term -> m (Sort' Term)) -> Sort' Term -> m (Sort' Term)
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort' Term
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    u Integer
    n
        Sort' Term
    SizeUniv -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    forall t. Sort' t
    SizeUniv
        Sort' Term
    LockUniv -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    forall t. Sort' t
    LockUniv
        Sort' Term
    LevelUniv -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    forall t. Sort' t
    LevelUniv
        Sort' Term
    IntervalUniv -> Sort' Term -> m (Sort' Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort' Term
    forall t. Sort' t
    IntervalUniv
        PiSort Dom' Term Term
    dom Sort' Term
    s1 Abs (Sort' Term)
    s2 -> do
          let a :: Term
    a = Dom' Term Term -> Term
    forall t e. Dom' t e -> e
    unDom Dom' Term Term
    dom
          s1' <- Action m -> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf (Sort' Term) ~ ()) =>
    Action m -> Sort' Term -> m (Sort' Term)
    inferInternal' Action m
    action Sort' Term
    s1
          a' <- checkInternal' action a CmpLeq $ sort s1'
          let dom' = Dom' Term Term
    dom Dom' Term Term -> Term -> Dom' Term Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    a'
          s2' <- mapAbstraction (El s1' <$> dom') (inferInternal' action) s2
          return $ PiSort dom' s1' s2'
        FunSort Sort' Term
    s1 Sort' Term
    s2 -> do
          s1' <- Action m -> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf (Sort' Term) ~ ()) =>
    Action m -> Sort' Term -> m (Sort' Term)
    inferInternal' Action m
    action Sort' Term
    s1
          s2' <- inferInternal' action s2
          return $ FunSort s1' s2'
        UnivSort Sort' Term
    s -> Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t
    UnivSort (Sort' Term -> Sort' Term) -> m (Sort' Term) -> m (Sort' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Sort' Term -> m (Sort' Term)
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf (Sort' Term) ~ ()) =>
    Action m -> Sort' Term -> m (Sort' Term)
    inferInternal' Action m
    action Sort' Term
    s
        MetaS MetaId
    x Elims
    es -> do -- we assume sort meta instantiations to be well-formed
          a <- MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x
          MetaS x <$> checkInternal' action es cmp (a , Sort . MetaS x)
        DefS QName
    d Elims
    es -> do
          a <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
          DefS d <$> checkInternal' action es cmp (a , Sort . DefS d)
        DummyS String
    s -> String -> m (Sort' Term)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s

    instance CheckInternal Level where
      checkInternal' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Level -> Comparison -> TypeOf Level -> m Level
    checkInternal' Action m
    action (Max Integer
    n [PlusLevel' Term]
    ls) Comparison
    _ TypeOf Level
    _ = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (PlusLevel' Term -> m (PlusLevel' Term))
    -> [PlusLevel' Term] -> m [PlusLevel' Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Action m -> PlusLevel' Term -> m (PlusLevel' Term)
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
    Action m -> a -> m a
    forall (m :: * -> *).
    (MonadCheckInternal m, TypeOf (PlusLevel' Term) ~ ()) =>
    Action m -> PlusLevel' Term -> m (PlusLevel' Term)
    inferInternal' Action m
    action) [PlusLevel' Term]
    ls

    instance CheckInternal PlusLevel where
      checkInternal' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> PlusLevel' Term
    -> Comparison
    -> TypeOf (PlusLevel' Term)
    -> m (PlusLevel' Term)
    checkInternal' Action m
    action (Plus Integer
    k Term
    l) Comparison
    _ TypeOf (PlusLevel' Term)
    _ = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    k (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    checkLevelAtom Term
    l
        where
        checkLevelAtom :: Term -> m Term
    checkLevelAtom Term
    l = do
          lvl <- m Type
    forall (m :: * -> *). HasBuiltins m => m Type
    levelType'
          checkInternal' action l CmpLeq lvl