    -- 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
      , checkType'
      , checkSort
      , checkInternal
      , checkInternal'
      , checkInternalType'
      , Action(..), defaultAction, eraseUnusedAction
      , infer
      , inferSpine'
      , shouldBeSort
      ) where

    import Control.Arrow (first)
    import Control.Monad

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Datatypes -- (getConType, getFullyAppliedConType)
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.ProjectionLike (elimView, ProjEliminator(..))
    import Agda.TypeChecking.Records (getDefType)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Sort
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Functor (($>))
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- * Bidirectional rechecker

    type MonadCheckInternal m = MonadConversion m

    -- -- | Entry point for e.g. checking WithFunctionType.
    -- checkType :: Type -> TCM ()
    -- checkType t = -- dontAssignMetas $ ignoreSorts $
    --   checkInternal (unEl t) (sort Inf)

    -- | 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
    $ do
      Sort
    inferred <- Type -> m Sort
    forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
    checkType' Type
    t
      Sort -> Sort -> m ()
    forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    equalSort (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    t) Sort
    inferred

    -- | Check a type and infer its sort.
    --
    --   Necessary because of PTS rule @(SizeUniv, Set i, Set i)@
    --   but @SizeUniv@ is not included in any @Set i@.
    --
    --   This algorithm follows
    --     Abel, Coquand, Dybjer, MPC 08,
    --     Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
    --
    checkType' :: (MonadCheckInternal m) => Type -> m Sort
    checkType' :: forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
    checkType' Type
    t = do
      ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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 type "
        , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        ]
      Term
    v <- ProjEliminator -> Term -> m Term
    forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    EvenLone (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t -- bring projection-like funs in post-fix form
      case Term
    v of
        Pi Dom Type
    a Abs Type
    b -> do
          Sort
    s1 <- Type -> m Sort
    forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
    checkType' (Type -> m Sort) -> Type -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a
          Abs Sort
    s2 <- (Abs Type
    b Abs Type -> Sort -> Abs Sort
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>) (Sort -> Abs Sort) -> m Sort -> m (Abs Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            let goInside :: m Sort -> m Sort
    goInside = case Abs Type
    b of Abs{}   -> (ArgName, Dom Type) -> m Sort -> m Sort
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b, Dom Type
    a)
                                     NoAbs{} -> m Sort -> m Sort
    forall a. a -> a
    id
            m Sort -> m Sort
    goInside (m Sort -> m Sort) -> m Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Type -> m Sort
    forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
    checkType' (Type -> m Sort) -> Type -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b
          Dom Type -> Abs Sort -> m Sort
    forall (m :: * -> *). PureTCM m => Dom Type -> Abs Sort -> m Sort
    inferPiSort Dom Type
    a Abs Sort
    s2
        Sort Sort
    s -> do
          Sort
    _ <- Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction Sort
    s
          Sort -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    Sort -> m Sort
    inferUnivSort Sort
    s
        Var VerboseLevel
    i Elims
    es   -> do
          Type
    a <- VerboseLevel -> m Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    VerboseLevel -> m Type
    typeOfBV VerboseLevel
    i
          Type -> Term -> Elims -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m Sort
    checkTypeSpine Type
    a (VerboseLevel -> Elims -> Term
    Var VerboseLevel
    i   []) Elims
    es
        Def QName
    f Elims
    es   -> do  -- not a projection-like fun
          Type
    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
          Type -> Term -> Elims -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m Sort
    checkTypeSpine Type
    a (QName -> Elims -> Term
    Def QName
    f   []) Elims
    es
        MetaV MetaId
    x Elims
    es -> do -- we assume meta instantiations to be well-typed
          Type
    a <- MetaId -> m Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    x
          Type -> Term -> Elims -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m Sort
    checkTypeSpine Type
    a (MetaId -> Elims -> Term
    MetaV MetaId
    x []) Elims
    es
        v :: Term
    v@Lam{}    -> TypeError -> m Sort
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Sort) -> TypeError -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> TypeError
    InvalidType Term
    v
        v :: Term
    v@Con{}    -> TypeError -> m Sort
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Sort) -> TypeError -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> TypeError
    InvalidType Term
    v
        v :: Term
    v@Lit{}    -> TypeError -> m Sort
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Sort) -> TypeError -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> TypeError
    InvalidType Term
    v
        v :: Term
    v@Level{}  -> TypeError -> m Sort
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Sort) -> TypeError -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> TypeError
    InvalidType Term
    v
        DontCare Term
    v -> Type -> m Sort
    forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
    checkType' (Type -> m Sort) -> Type -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Type
    t Type -> Term -> Type
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    v
        Dummy ArgName
    s Elims
    _  -> ArgName -> m Sort
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s

    checkTypeSpine :: (MonadCheckInternal m) => Type -> Term -> Elims -> m Sort
    checkTypeSpine :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m Sort
    checkTypeSpine Type
    a Term
    self Elims
    es = Type -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadError TCErr m) =>
    Type -> m Sort
    shouldBeSort (Type -> m Sort) -> m Type -> m Sort
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do (Term, Type) -> Type
    forall a b. (a, b) -> b
    snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> m (Term, Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m (Term, Type)
    inferSpine Type
    a Term
    self Elims
    es

    checkInternalType' :: (MonadCheckInternal m) => Action m -> Type -> m Type
    checkInternalType' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> m Type
    checkInternalType' Action m
    act El{_getSort :: forall t a. Type'' t a -> Sort' t
    _getSort=Sort
    s, unEl :: forall t a. Type'' t a -> a
    unEl=Term
    t} = do
      Term
    tAfterAct <- Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    act Term
    t Comparison
    CmpLeq (Sort -> Type
    sort Sort
    s)
      Type -> m Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return El :: forall t a. Sort' t -> a -> Type'' t a
    El{_getSort :: Sort
    _getSort=Sort
    s, unEl :: Term
    unEl=Term
    tAfterAct}

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

    -- | Entry point for term checking.
    checkInternal :: (MonadCheckInternal m) => Term -> Comparison -> Type -> m ()
    checkInternal :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Term -> Comparison -> Type -> m ()
    checkInternal Term
    v Comparison
    cmp Type
    t = m Term -> m ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (m Term -> m ()) -> m Term -> m ()
    forall a b. (a -> b) -> a -> b
    $ Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction Term
    v Comparison
    cmp Type
    t

    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 = ArgName -> VerboseLevel -> ArgName -> m Term -> m Term
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> VerboseLevel -> ArgName -> m a -> m a
    verboseBracket ArgName
    "tc.check.internal" VerboseLevel
    20 ArgName
    "" (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ do
      ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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 "
        , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    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
    ":"
                       , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    prettyTCM Type
    t ] ]
      ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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
    "checking internal with DB indices"
        , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    ":"
                       , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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 ] ]
      Telescope
    ctx <- m Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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
    "In context"
        , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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 [ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    ctx ] ]
      -- Bring projection-like funs in post-fix form,
      -- (even lone ones by default).
      Term
    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
      Action m -> Type -> Term -> m Term
    forall (m :: * -> *). Action m -> Type -> Term -> m Term
    postAction Action m
    action Type
    t (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< case Term
    v of
        Var VerboseLevel
    i Elims
    es   -> do
          Type
    a <- VerboseLevel -> m Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    VerboseLevel -> m Type
    typeOfBV VerboseLevel
    i
          ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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
    fsep
            [ TCMT IO Doc
    "variable" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (VerboseLevel -> Term
    var VerboseLevel
    i) , TCMT IO Doc
    "has type" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ]
          Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    checkSpine Action m
    action Type
    a (VerboseLevel -> Elims -> Term
    Var VerboseLevel
    i []) Elims
    es Comparison
    cmp Type
    t
        Def QName
    f Elims
    es   -> do  -- f is not projection(-like)!
          Type
    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
          Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    checkSpine Action m
    action Type
    a (QName -> Elims -> Term
    Def QName
    f []) Elims
    es Comparison
    cmp Type
    t
        MetaV MetaId
    x Elims
    es -> do -- we assume meta instantiations to be well-typed
          Type
    a <- MetaId -> m Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    x
          ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "metavariable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "has type" 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
    prettyTCM Type
    a
          Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    checkSpine Action m
    action Type
    a (MetaId -> Elims -> Term
    MetaV MetaId
    x []) Elims
    es Comparison
    cmp Type
    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.
    MonadCheckInternal 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
            Con ConHead
    c ConInfo
    ci Elims
    vs2 <- Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> 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
            -- Strip away the extra arguments
            Term -> m Term
    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 -> VerboseLevel -> Substitution' Term
    forall a. Impossible -> VerboseLevel -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible (Telescope -> VerboseLevel
    forall a. Sized a => a -> VerboseLevel
    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
    $ VerboseLevel -> Elims -> Elims
    forall a. VerboseLevel -> [a] -> [a]
    take (Elims -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length Elims
    vs) Elims
    vs2
        Lit Literal
    l      -> do
          Type
    lt <- Literal -> m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    Literal -> m Type
    litType Literal
    l
          Comparison -> Type -> Type -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Type -> m ()
    compareType Comparison
    cmp Type
    lt Type
    t
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
        Lam ArgInfo
    ai Abs Term
    vb  -> do
          (Dom Type
    a, Abs Type
    b) <- m (Dom Type, Abs Type)
    -> ((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
    -> Maybe (Dom Type, Abs Type)
    -> m (Dom Type, Abs Type)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> m (Dom Type, Abs Type)
    shouldBePi Type
    t) (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Dom Type, Abs Type) -> m (Dom Type, Abs Type))
    -> m (Maybe (Dom Type, Abs Type)) -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> m (Maybe (Dom Type, Abs Type))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (Dom Type, Abs Type))
    isPath Type
    t
          ArgInfo
    ai <- Action m -> ArgInfo -> ArgInfo -> m ArgInfo
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> ArgInfo -> ArgInfo -> m ArgInfo
    checkArgInfo Action m
    action ArgInfo
    ai (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a
          let name :: ArgName
    name = [Suggestion] -> ArgName
    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 ]
          (ArgName, Dom Type) -> m Term -> m Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (ArgName
    name, Dom Type
    a) (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ do
            ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    ai (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs (Abs Term -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Term
    vb) (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action (Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    vb) Comparison
    cmp (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)
        Pi Dom Type
    a Abs Type
    b     -> do
          Sort
    s <- Type -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadError TCErr m) =>
    Type -> m Sort
    shouldBeSort Type
    t
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Sort
    s Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    forall t. Sort' t
    SizeUniv) (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
    $ Term -> TypeError
    FunctionTypeInSizeUniv Term
    v
          let sa :: Sort
    sa  = Dom Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Dom Type
    a
              sb :: Sort
    sb  = Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b)
              mkDom :: Term -> Dom Type
    mkDom Term
    v = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    sa Term
    v Type -> Dom Type -> Dom Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type
    a
              mkRng :: Term -> Abs Type
    mkRng Term
    v = (Type -> Type) -> Abs Type -> Abs Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term
    v Term -> Type -> Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) Abs Type
    b
              -- Preserve NoAbs
              goInside :: m Term -> m Term
    goInside = case Abs Type
    b of Abs{}   -> (ArgName, Dom Type) -> m Term -> m Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b, Dom Type
    a)
                                   NoAbs{} -> m Term -> m Term
    forall a. a -> a
    id
          Dom Type
    a <- Term -> Dom Type
    mkDom (Term -> Dom Type) -> m Term -> m (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) Comparison
    CmpLeq (Sort -> Type
    sort Sort
    sa)
          Term
    v' <- m Term -> m Term
    goInside (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Term
    Pi Dom Type
    a (Abs Type -> Term) -> (Term -> Abs Type) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Abs Type
    mkRng (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b) Comparison
    CmpLeq (Sort -> Type
    sort Sort
    sb)
          Sort
    s' <- Term -> m Sort
    forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
    sortOf Term
    v'
          Comparison -> Sort -> Sort -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Sort -> Sort -> m ()
    compareSort Comparison
    cmp Sort
    s' Sort
    s
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v'
        Sort Sort
    s     -> do
          ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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 -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    s
          Sort
    s <- Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action Sort
    s
          Sort
    s' <- Sort -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    Sort -> m Sort
    inferUnivSort Sort
    s
          Sort
    s'' <- Type -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadError TCErr m) =>
    Type -> m Sort
    shouldBeSort Type
    t
          Comparison -> Sort -> Sort -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Sort -> Sort -> m ()
    compareSort Comparison
    cmp Sort
    s' Sort
    s''
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term
    Sort Sort
    s
        Level Level
    l    -> do
          Level
    l <- Action m -> Level -> m Level
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Level -> m Level
    checkLevel Action m
    action Level
    l
          Type
    lt <- m Type
    forall (m :: * -> *). HasBuiltins m => m Type
    levelType
          Comparison -> Type -> Type -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Type -> m ()
    compareType Comparison
    cmp Type
    lt Type
    t
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Term
    Level 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 -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    v Comparison
    cmp Type
    t
        Dummy ArgName
    s Elims
    _ -> ArgName -> m Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s

    -- | Make sure a constructor is fully applied
    --   and infer the type of the constructor.
    --   Raises a type error if the constructor does not belong to the given type.
    fullyApplyCon
      :: (MonadCheckInternal m)
      => ConHead -- ^ Constructor.
      -> Elims    -- ^ Constructor arguments.
      -> Type    -- ^ Type of the constructor application.
      -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
           -- ^ Name of the data/record type,
           --   type of the data/record type,
           --   reconstructed parameters,
           --   type of the constructor (applied to parameters),
           --   full application arguments,
           --   types of missing arguments (already added to context),
           --   type of the full application.
      -> m a
    fullyApplyCon :: forall (m :: * -> *) a.
    MonadCheckInternal m =>
    ConHead
    -> Elims
    -> Type
    -> (QName
        -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
    -> m a
    fullyApplyCon ConHead
    c Elims
    vs Type
    t0 QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a
    ret = do
      (TelV Telescope
    tel Type
    t, Boundary
    boundary) <- Type -> m (TelView, Boundary)
    forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
    telViewPathBoundaryP Type
    t0
      -- The type of the constructor application may still be a function
      -- type.  In this case, we introduce the domains @tel@ into the context
      -- and apply the constructor to these fresh variables.
      Telescope -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ do
        Type
    t <- Type -> m Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t
        ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t m (Maybe ((QName, Type, Args), Type))
    -> (Maybe ((QName, Type, Args), Type) -> m a) -> m a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Maybe ((QName, Type, Args), Type)
    Nothing ->
            TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ QName -> Type -> TypeError
    DoesNotConstructAnElementOf (ConHead -> QName
    conName ConHead
    c) Type
    t
          Just ((QName
    d, Type
    dt, Args
    pars), Type
    a) ->
            QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a
    ret QName
    d Type
    dt Args
    pars Type
    a (VerboseLevel -> Elims -> Elims
    forall a. Subst a => VerboseLevel -> a -> a
    raise (Telescope -> VerboseLevel
    forall a. Sized a => a -> VerboseLevel
    size Telescope
    tel) Elims
    vs Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> Boundary -> Elims
    forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
    teleElims Telescope
    tel Boundary
    boundary) Telescope
    tel Type
    t

    checkSpine
      :: (MonadCheckInternal m)
      => Action m
      -> Type       -- ^ Type of the head @self@.
      -> Term       -- ^ The head @self@.
      -> 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 -> Term -> Elims -> Comparison -> Type -> m Term
    checkSpine Action m
    action Type
    a Term
    self Elims
    es Comparison
    cmp Type
    t = do
      ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.check.internal" VerboseLevel
    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 "
        , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    prettyTCM Term
    self TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                                     , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    prettyTCM Type
    a ])
                       , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    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
    ":"
                       , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    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
    prettyTCM Type
    t ] ]
      ((Term
    v, Term
    v'), Type
    t') <- Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action Type
    a Term
    self Term
    self Elims
    es
      Type
    t' <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t'
      Term
    v' Term -> m () -> m Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ (Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    (Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
    coerceSize (Comparison -> Type -> Type -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Type -> m ()
    compareType Comparison
    cmp) Term
    v Type
    t' Type
    t
    --UNUSED Liang-Ting Chen 2019-07-16
    --checkArgs
    --  :: (MonadCheckInternal m)
    --  => Action m
    --  -> Type      -- ^ Type of the head.
    --  -> Term      -- ^ The head.
    --  -> Args      -- ^ The arguments.
    --  -> Type      -- ^ Expected type of the application.
    --  -> m Term    -- ^ The application after modification by the @Action@.
    --checkArgs action a self vs t = checkSpine action a self (map Apply vs) t

    -- | @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')
      Modality
    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')
      ArgInfo -> m ArgInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
    forall a b. (a -> b) -> a -> b
    $ Modality -> ArgInfo -> ArgInfo
    forall a. LensModality a => Modality -> a -> a
    setModality Modality
    mod ArgInfo
    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 (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@

    -- | Infer type of a neutral term.
    infer :: (MonadCheckInternal m) => Term -> m Type
    infer :: forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
    infer Term
    v = do
      case Term
    v of
        Var VerboseLevel
    i Elims
    es   -> do
          Type
    a <- VerboseLevel -> m Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    VerboseLevel -> m Type
    typeOfBV VerboseLevel
    i
          (Term, Type) -> Type
    forall a b. (a, b) -> b
    snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> m (Term, Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m (Term, Type)
    inferSpine Type
    a (VerboseLevel -> Elims -> Term
    Var VerboseLevel
    i   []) Elims
    es
        Def QName
    f (Apply Arg Term
    a : Elims
    es) -> QName -> Arg Term -> Elims -> m Type
    forall (m :: * -> *).
    MonadCheckInternal m =>
    QName -> Arg Term -> Elims -> m Type
    inferDef' QName
    f Arg Term
    a Elims
    es -- possibly proj.like
        Def QName
    f Elims
    es             -> QName -> Elims -> m Type
    forall (m :: * -> *).
    MonadCheckInternal m =>
    QName -> Elims -> m Type
    inferDef  QName
    f   Elims
    es -- not a projection-like fun
        MetaV MetaId
    x Elims
    es -> do -- we assume meta instantiations to be well-typed
          Type
    a <- MetaId -> m Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    x
          (Term, Type) -> Type
    forall a b. (a, b) -> b
    snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> m (Term, Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m (Term, Type)
    inferSpine Type
    a (MetaId -> Elims -> Term
    MetaV MetaId
    x []) Elims
    es
        Term
    _ -> m Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Infer ordinary function application.
    inferDef :: (MonadCheckInternal m) => QName -> Elims -> m Type
    inferDef :: forall (m :: * -> *).
    MonadCheckInternal m =>
    QName -> Elims -> m Type
    inferDef QName
    f Elims
    es = do
      Type
    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
      (Term, Type) -> Type
    forall a b. (a, b) -> b
    snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> m (Term, Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m (Term, Type)
    inferSpine Type
    a (QName -> Elims -> Term
    Def QName
    f []) Elims
    es

    -- | Infer possibly projection-like function application
    inferDef' :: (MonadCheckInternal m) => QName -> Arg Term -> Elims -> m Type
    inferDef' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    QName -> Arg Term -> Elims -> m Type
    inferDef' QName
    f Arg Term
    a Elims
    es = do
      -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
      QName -> m (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f m (Maybe Projection) -> (Maybe Projection -> m Type) -> m Type
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just Projection{ projIndex :: Projection -> VerboseLevel
    projIndex = VerboseLevel
    n } | VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    > VerboseLevel
    0 -> do
          let self :: Term
    self = Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a
          Type
    b <- Term -> m Type
    forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
    infer Term
    self
          (Term, Type) -> Type
    forall a b. (a, b) -> b
    snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> m (Term, Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m (Term, Type)
    inferSpine Type
    b Term
    self (ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    es)
        Maybe Projection
    _ -> QName -> Elims -> m Type
    forall (m :: * -> *).
    MonadCheckInternal m =>
    QName -> Elims -> m Type
    inferDef QName
    f (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    a Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    es)

    -- | @inferSpine t self es@ checks that spine @es@ eliminates
    --   value @self@ of type @t@ and returns the remaining type
    --   (target of elimination) and the final self (has that type).
    inferSpine :: (MonadCheckInternal m) => Type -> Term -> Elims -> m (Term, Type)
    inferSpine :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> Term -> Elims -> m (Term, Type)
    inferSpine Type
    a Term
    v Elims
    es = ((Term, Term) -> Term) -> ((Term, Term), Type) -> (Term, Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (Term, Term) -> Term
    forall a b. (a, b) -> a
    fst (((Term, Term), Type) -> (Term, Type))
    -> m ((Term, Term), Type) -> m (Term, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction Type
    a Term
    v Term
    v Elims
    es

    -- | Returns both the real term (first) and the transformed term (second). The
    --   transformed term is not necessarily a valid term, so it must not be used
    --   in types.
    inferSpine' :: (MonadCheckInternal m)
                => Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action Type
    t Term
    self Term
    self' [] = ((Term, Term), Type) -> m ((Term, Term), Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Term
    self, Term
    self'), Type
    t)
    inferSpine' Action m
    action Type
    t Term
    self Term
    self' (Elim
    e : Elims
    es) = do
      ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.infer.internal" VerboseLevel
    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
    "inferSpine': "
        , 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    self
        , 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty 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
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Elim -> ArgName
    forall a. Show a => a -> ArgName
    show Elim
    e)
        ]
      case Elim
    e of
        IApply Term
    x Term
    y Term
    r -> do
          (Dom Type
    a, Abs Type
    b) <- Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> m (Dom Type, Abs Type)
    shouldBePath Type
    t
          Term
    r' <- Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    r Comparison
    CmpLeq (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)
          Term
    izero <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero
          Term
    ione  <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
          Term
    x' <- Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    x Comparison
    CmpLeq (Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    izero)
          Term
    y' <- Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    y Comparison
    CmpLeq (Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    ione)
          Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action (Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    r) (Term
    self Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [Elim
    e]) (Term
    self' Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply Term
    x' Term
    y' Term
    r']) Elims
    es
        Apply (Arg ArgInfo
    ai Term
    v) -> do
          (Dom Type
    a, Abs Type
    b) <- Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> m (Dom Type, Abs Type)
    shouldBePi Type
    t
          ArgInfo
    ai <- Action m -> ArgInfo -> ArgInfo -> m ArgInfo
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> ArgInfo -> ArgInfo -> m ArgInfo
    checkArgInfo Action m
    action ArgInfo
    ai (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a
          Term
    v' <- Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    v Comparison
    CmpLeq (Type -> m Term) -> Type -> m Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a
          Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action (Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    v) (Term
    self Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [Elim
    e]) (Term
    self' Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [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')]) Elims
    es
        -- case: projection or projection-like
        Proj ProjOrigin
    o QName
    f -> do
          (Dom Type
    a, Abs Type
    b) <- Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> m (Dom Type, Abs Type)
    shouldBePi (Type -> m (Dom Type, Abs Type))
    -> m Type -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> QName -> m Type
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> QName -> m Type
    shouldBeProjectible Type
    t QName
    f
          Term
    u  <- ProjOrigin -> QName -> Arg Term -> m Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    self)
          Term
    u' <- ProjOrigin -> QName -> Arg Term -> m Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    self')
          Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action (Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    self) Term
    u Term
    u' Elims
    es

    -- | Type should either be a record type of a type eligible for
    --   the principal argument of projection-like functions.
    shouldBeProjectible :: (MonadCheckInternal m) => Type -> QName -> m Type
    -- shouldBeProjectible t f = maybe failure return =<< projectionType t f
    shouldBeProjectible :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> QName -> m Type
    shouldBeProjectible Type
    t QName
    f = do
        Type
    t <- Type -> m Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t
        m Type -> (Type -> m Type) -> Maybe Type -> m Type
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m Type
    failure Type -> m Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Type -> m Type) -> m (Maybe Type) -> m Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> Type -> m (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f Type
    t
      where failure :: m Type
    failure = TypeError -> m Type
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Type) -> TypeError -> m Type
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBeRecordType Type
    t
        -- TODO: more accurate error that makes sense also for proj.-like funs.

    shouldBePath :: (MonadCheckInternal m) => Type -> m (Dom Type, Abs Type)
    shouldBePath :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> m (Dom Type, Abs Type)
    shouldBePath Type
    t = do
      Type
    t <- Type -> m Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t
      Maybe (Dom Type, Abs Type)
    m <- Type -> m (Maybe (Dom Type, Abs Type))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (Dom Type, Abs Type))
    isPath Type
    t
      case Maybe (Dom Type, Abs Type)
    m of
        Just (Dom Type, Abs Type)
    p  -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type, Abs Type)
    p
        Maybe (Dom Type, Abs Type)
    Nothing -> TypeError -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Dom Type, Abs Type))
    -> TypeError -> m (Dom Type, Abs Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBePath Type
    t

    shouldBePi :: (MonadCheckInternal m) => Type -> m (Dom Type, Abs Type)
    shouldBePi :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Type -> m (Dom Type, Abs Type)
    shouldBePi Type
    t = Type -> m Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t m Type
    -> (Type -> m (Dom Type, Abs Type)) -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
      El Sort
    _ (Pi Dom Type
    a Abs Type
    b) -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type
    a, Abs Type
    b)
      Type
    _             -> TypeError -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Dom Type, Abs Type))
    -> TypeError -> m (Dom Type, Abs Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBePi Type
    t

    -- | Check if sort is well-formed.
    checkSort :: (MonadCheckInternal m) => Action m -> Sort -> m Sort
    checkSort :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action Sort
    s =
      case Sort
    s of
        Type Level
    l   -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Level -> m Level
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Level -> m Level
    checkLevel Action m
    action Level
    l
        Prop Level
    l   -> Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Level -> m Level
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Level -> m Level
    checkLevel Action m
    action Level
    l
        Inf IsFibrant
    f Integer
    n  -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f Integer
    n
        SSet Level
    l   -> Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Level -> m Level
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Level -> m Level
    checkLevel Action m
    action Level
    l
        Sort
    SizeUniv -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    forall t. Sort' t
    SizeUniv
        Sort
    LockUniv -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    forall t. Sort' t
    LockUniv
        PiSort Dom' Term Term
    dom Sort
    s1 Abs Sort
    s2 -> do
          let a :: Term
    a = Dom' Term Term -> Term
    forall t e. Dom' t e -> e
    unDom Dom' Term Term
    dom
          Sort
    s1' <- Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action Sort
    s1
          Term
    a' <- Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    a Comparison
    CmpLeq (Type -> m Term) -> Type -> m Term
    forall a b. (a -> b) -> a -> b
    $ Sort -> Type
    sort Sort
    s1'
          let dom' :: Dom' Term Term
    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'
          Abs Sort
    s2' <- Dom Type -> (Sort -> m Sort) -> Abs Sort -> m (Abs Sort)
    forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s1' (Term -> Type) -> Dom' Term Term -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Term
    dom') (Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action) Abs Sort
    s2
          Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort Dom' Term Term
    dom' Sort
    s1' Abs Sort
    s2'
        FunSort Sort
    s1 Sort
    s2 -> do
          Sort
    s1' <- Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action Sort
    s1
          Sort
    s2' <- Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action Sort
    s2
          Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    s1' Sort
    s2'
        UnivSort Sort
    s -> Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort (Sort -> Sort) -> m Sort -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Action m -> Sort -> m Sort
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Sort -> m Sort
    checkSort Action m
    action Sort
    s
        MetaS MetaId
    x Elims
    es -> do -- we assume sort meta instantiations to be well-formed
          Type
    a <- MetaId -> m Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    x
          let self :: Term
    self = Sort -> Term
    Sort (Sort -> Term) -> Sort -> Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x []
          ((Term
    _,Term
    v),Type
    _) <- Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action Type
    a Term
    self Term
    self Elims
    es
          case Term
    v of
            Sort Sort
    s     -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
            MetaV MetaId
    x Elims
    es -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x Elims
    es
            Def QName
    d Elims
    es   -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d Elims
    es
            Term
    _          -> m Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        DefS QName
    d Elims
    es -> do
          Type
    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
          let self :: Term
    self = Sort -> Term
    Sort (Sort -> Term) -> Sort -> Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d []
          ((Term
    _,Term
    v),Type
    _) <- Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
    inferSpine' Action m
    action Type
    a Term
    self Term
    self Elims
    es
          case Term
    v of
            Sort Sort
    s     -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
            MetaV MetaId
    x Elims
    es -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x Elims
    es
            Def QName
    d Elims
    es   -> Sort -> m Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d Elims
    es
            Term
    _          -> m Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        DummyS ArgName
    s -> ArgName -> m Sort
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s

    -- | Check if level is well-formed.
    checkLevel :: (MonadCheckInternal m) => Action m -> Level -> m Level
    checkLevel :: forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Level -> m Level
    checkLevel Action m
    action (Max Integer
    n [PlusLevel' Term]
    ls) = 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)
    mapM PlusLevel' Term -> m (PlusLevel' Term)
    checkPlusLevel [PlusLevel' Term]
    ls
      where
        checkPlusLevel :: PlusLevel' Term -> m (PlusLevel' Term)
    checkPlusLevel (Plus Integer
    k Term
    l)      = 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

        checkLevelAtom :: Term -> m Term
    checkLevelAtom Term
    l = do
          Type
    lvl <- m Type
    forall (m :: * -> *). HasBuiltins m => m Type
    levelType
          Action m -> Term -> Comparison -> Type -> m Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action m
    action Term
    l Comparison
    CmpLeq Type
    lvl

    -- | Universe subsumption and type equality (subtyping for sizes, resp.).
    cmptype :: (MonadCheckInternal m) => Comparison -> Type -> Type -> m ()
    cmptype :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Type -> m ()
    cmptype Comparison
    cmp Type
    t1 Type
    t2 = do
        -- Andreas, 2017-03-09, issue #2493
        -- Only check subtyping, do not solve any metas!
        m () -> m ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Type -> Type -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Type -> m ()
    compareType Comparison
    cmp Type
    t1 Type
    t2