{-# 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
  ( 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, LoneProjectionLikeToLambda(..))
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

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

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

-- | The default action is to not change the 'Term' at all.
defaultAction :: Action
defaultAction :: Action
defaultAction = Action
  { preAction :: Type'' Term Term -> Term -> TCM Term
preAction       = \ Type'' Term Term
_ -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  , postAction :: Type'' Term Term -> Term -> TCM Term
postAction      = \ Type'' Term Term
_ -> Term -> TCM Term
forall a. a -> TCMT IO 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 -> TCM Term
elimViewAction  = LoneProjectionLikeToLambda -> Term -> TCM Term
forall (m :: * -> *).
PureTCM m =>
LoneProjectionLikeToLambda -> Term -> m Term
elimView LoneProjectionLikeToLambda
LoneProjectionLikeToLambda
  }

eraseUnusedAction :: Action
eraseUnusedAction :: Action
eraseUnusedAction = Action
defaultAction { postAction = eraseUnused }
  where
    eraseUnused :: Type -> Term -> TCM Term
    eraseUnused :: Type'' Term Term -> Term -> TCM Term
eraseUnused Type'' Term Term
t = \case
      Def QName
f Elims
es -> do
        pols <- QName -> TCMT IO [Polarity]
forall (m :: * -> *).
(HasCallStack, 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' Term
e : Elims
es) = ((Term -> Term) -> Elim' Term -> Elim' Term
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' Term
e) Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
    eraseIfNonvariant (Polarity
_          : [Polarity]
pols) (Elim' Term
e : Elims
es) = Elim' Term
e Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es

class CheckInternal a where
  checkInternal' :: Action -> a -> Comparison -> TypeOf a -> TCM a

  checkInternal :: a -> Comparison -> TypeOf a -> TCM ()
  checkInternal a
v Comparison
cmp TypeOf a
t = TCMT IO a -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCMT IO a -> TCM ()) -> TCMT IO a -> TCM ()
forall a b. (a -> b) -> a -> b
$ Action -> a -> Comparison -> TypeOf a -> TCMT IO a
forall a.
CheckInternal a =>
Action -> a -> Comparison -> TypeOf a -> TCMT IO a
checkInternal' Action
defaultAction a
v Comparison
cmp TypeOf a
t

  inferInternal' :: (TypeOf a ~ ()) => Action -> a -> TCM a
  inferInternal' Action
act a
v = Action -> a -> Comparison -> TypeOf a -> TCMT IO a
forall a.
CheckInternal a =>
Action -> a -> Comparison -> TypeOf a -> TCMT IO a
checkInternal' Action
act a
v Comparison
CmpEq ()

  inferInternal :: (TypeOf a ~ ()) => a -> TCM ()
  inferInternal a
v = a -> Comparison -> TypeOf a -> TCM ()
forall a. CheckInternal a => a -> Comparison -> TypeOf a -> TCM ()
checkInternal a
v Comparison
CmpEq ()


instance CheckInternal Type where
  checkInternal' :: Action
-> Type'' Term Term
-> Comparison
-> TypeOf (Type'' Term Term)
-> TCM (Type'' Term Term)
checkInternal' Action
action (El Sort' Term
s Term
t) Comparison
cmp TypeOf (Type'' Term Term)
_ = do
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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 "
      , 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t 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
$ 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 ]
      ]
    t' <- Action -> Term -> Comparison -> TypeOf Term -> TCM Term
forall a.
CheckInternal a =>
Action -> a -> Comparison -> TypeOf a -> TCMT IO a
checkInternal' Action
action Term
t Comparison
cmp (Sort' Term -> Type'' Term Term
sort Sort' Term
s)
    s' <- sortOf t'
    reportSDoc "tc.check.internal" 30 $
      "checking if sort" <+> prettyTCM s' <+>
      "of" <+> prettyTCM t' <+>
      "fits in given sort" <+> prettyTCM s
    compareSort cmp s' s
    return (El s t')

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

    -- Debug print
    VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.check.internal" VerboseLevel
20 do
      VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
":"
                      , 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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t ] ]
      VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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'' Term Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type'' Term Term
t ] ]
      ctx <- TCMT IO 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 -> Term -> TCM Term
elimViewAction Action
action (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Action -> Type'' Term Term -> Term -> TCM Term
preAction Action
action Type'' Term Term
t Term
v
    postAction action t =<< case v of
      Var VerboseLevel
i Elims
es   -> do
        d <- VerboseLevel -> TCMT IO (Dom (Type'' Term Term))
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
VerboseLevel -> m (Dom (Type'' Term Term))
domOfBV VerboseLevel
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

        reportSDoc "tc.check.internal" 30 $ fsep
          [ "variable" , prettyTCM (var i) , "has type" , prettyTCM (unDom d)
          , "and modality", pretty (getModality d)
          ]

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

        unless (usablePolarity d) $
          typeError $ VariableIsOfUnusablePolarity n (getModalPolarity 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'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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 -> TCM (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
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'' Term Term
-> (QName
    -> Type'' Term Term
    -> Args
    -> Type'' Term Term
    -> Elims
    -> Telescope
    -> Type'' Term Term
    -> TCM Term)
-> TCM Term
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m, MonadTCError m) =>
ConHead
-> Elims
-> Type'' Term Term
-> (QName
    -> Type'' Term Term
    -> Args
    -> Type'' Term Term
    -> Elims
    -> Telescope
    -> Type'' Term Term
    -> m a)
-> m a
fullyApplyCon ConHead
c Elims
vs Type'' Term Term
t ((QName
  -> Type'' Term Term
  -> Args
  -> Type'' Term Term
  -> Elims
  -> Telescope
  -> Type'' Term Term
  -> TCM Term)
 -> TCM Term)
-> (QName
    -> Type'' Term Term
    -> Args
    -> Type'' Term Term
    -> Elims
    -> Telescope
    -> Type'' Term Term
    -> TCM Term)
-> TCM Term
forall a b. (a -> b) -> a -> b
$ \ QName
_d Type'' Term Term
_dt Args
_pars Type'' Term Term
a Elims
vs' Telescope
tel Type'' Term Term
t -> do
          Action
-> Type'' Term Term
-> (Elims -> Term)
-> Elims
-> Comparison
-> Type'' Term Term
-> TCM Term
checkSpine Action
action Type'' Term Term
a (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
vs' Comparison
cmp Type'' Term Term
t TCM Term -> (Term -> TCM Term) -> TCM Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Con ConHead
c ConInfo
ci Elims
vs2 ->
              -- Strip away the extra arguments
              Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM 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 a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
vs) Elims
vs2
            Term
_ -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit Literal
l      -> do
        lt <- Literal -> TCM (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m (Type'' Term Term)
litType Literal
l
        compareType cmp lt t
        return $ Lit l
      Lam ArgInfo
ai Abs Term
vb  -> do
        (a, b) <- Type'' Term Term
-> TCMT IO (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
shouldBePiOrPath Type'' Term Term
t
        ai <- checkArgInfo action ai $ domInfo a
        let name = [Suggestion] -> VerboseKey
suggests [ Abs Term -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs Term
vb , Abs (Type'' Term Term) -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs (Type'' Term Term)
b ]
        addContext (name, a) $ do
          Lam ai . Abs (absName vb) <$> checkInternal' action (absBody vb) cmp (absBody b)
      Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b     -> do
        s <- Type'' Term Term -> TCMT IO (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type'' Term Term -> m (Sort' Term)
shouldBeSort Type'' Term Term
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'' Term Term) -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Dom (Type'' Term Term)
a
            sb  = Type'' Term Term -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Abs a -> a
unAbs Abs (Type'' Term Term)
b)
            mkDom Term
v = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
sa Term
v Type'' Term Term
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (Type'' Term Term)
a
            mkRng Term
v = (Type'' Term Term -> Type'' Term Term)
-> Abs (Type'' Term Term) -> Abs (Type'' Term Term)
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'' Term Term -> Type'' Term Term
forall a b. a -> Type'' Term b -> Type'' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Abs (Type'' Term Term)
b
            -- Preserve NoAbs
            goInside = case Abs (Type'' Term Term)
b of
              Abs{}   -> (VerboseKey, Dom (Type'' Term Term)) -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(VerboseKey, Dom (Type'' Term Term)) -> m a -> m a
addContext ((VerboseKey, Dom (Type'' Term Term)) -> TCM Term -> TCM Term)
-> (VerboseKey, Dom (Type'' Term Term)) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ (Abs (Type'' Term Term) -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs (Type'' Term Term)
b,) (Dom (Type'' Term Term) -> (VerboseKey, Dom (Type'' Term Term)))
-> Dom (Type'' Term Term) -> (VerboseKey, Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$
                PolarityModality
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a. LensModalPolarity a => PolarityModality -> a -> a
inverseApplyPolarity (ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
UnusedPolarity) (Dom (Type'' Term Term) -> Dom (Type'' Term Term))
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
                Bool
-> (Dom (Type'' Term Term) -> Dom (Type'' Term Term))
-> Dom (Type'' Term Term)
-> Dom (Type'' Term Term)
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
experimental ((Relevance -> Relevance)
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrelevantToShapeIrrelevant) Dom (Type'' Term Term)
a
              NoAbs{} -> TCM Term -> TCM 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
        reportSDoc "tc.check.internal" 30 $
          "checking if sort" <+> prettyTCM s' <+>
          "of pi type" <+> prettyTCM v <+>
          "fits in given sort" <+> prettyTCM s
        compareSort cmp s' s
        return v'
      Sort Sort' Term
s     -> do
        VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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 -> Sort' Term -> TCMT IO (Sort' Term)
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
action Sort' Term
s
        s' <- inferUnivSort s
        s'' <- shouldBeSort t
        reportSDoc "tc.check.internal" 30 $
          "checking if sort" <+> prettyTCM s' <+>
          "of universe type" <+> prettyTCM v <+>
          "fits in" <+> prettyTCM t
        compareSort cmp s' s''
        return $ Sort s
      Level Level
l    -> do
        l <- Action -> Level -> TCM Level
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
action Level
l
        lt <- levelType'
        compareType cmp lt t
        return $ Level l
      DontCare Term
v -> Term -> Term
DontCare (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action -> Term -> Comparison -> TypeOf Term -> TCM Term
forall a.
CheckInternal a =>
Action -> a -> Comparison -> TypeOf a -> TCMT IO a
checkInternal' Action
action Term
v Comparison
cmp TypeOf Term
Type'' Term Term
t
      -- Jesper, 2023-02-23: these can appear because of eta-expansion of
      -- records with irrelevant fields
      Dummy DummyTermKind
s Elims
_ -> Term -> TCM Term
forall a. a -> TCMT IO 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 :: Action -> ArgInfo -> ArgInfo -> TCM ArgInfo
checkArgInfo :: Action -> ArgInfo -> ArgInfo -> TCM ArgInfo
checkArgInfo Action
action ArgInfo
ai ArgInfo
ai' = do
  Hiding -> Hiding -> TCM ()
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 -> Modality -> Modality -> TCM Modality
checkModality Action
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 :: Hiding -> Hiding -> TCM ()
checkHiding :: Hiding -> Hiding -> TCM ()
checkHiding Hiding
h Hiding
h' = Bool -> TCM () -> TCM ()
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') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
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 :: Action -> Modality -> Modality -> TCM Modality
checkModality :: Action -> Modality -> Modality -> TCM Modality
checkModality Action
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 -> TCM () -> TCM ()
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') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
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 -> TCM Modality
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Modality -> TCM Modality) -> Modality -> TCM Modality
forall a b. (a -> b) -> a -> b
$ Action -> Modality -> Modality -> Modality
modalityAction Action
action Modality
mod' Modality
mod  -- Argument order for actions: @type@ @term@

-- | Infer type of a neutral term.
infer :: Term -> TCM Type
infer :: Term -> TCM (Type'' Term Term)
infer Term
u = do
  VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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 VerboseLevel
i Elims
es -> do
      a <- VerboseLevel -> TCM (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
VerboseLevel -> m (Type'' Term Term)
typeOfBV VerboseLevel
i
      fst <$> inferSpine defaultAction a (Var i) es
    Def QName
f Elims
es -> do
      TCMT IO (Maybe Projection) -> (Projection -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) ((Projection -> TCM ()) -> TCM ())
-> (Projection -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Projection
_ -> TCM ()
forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
      a <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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 -> TCM (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
metaType MetaId
x
      fst <$> inferSpine defaultAction a (MetaV x) es
    Term
_ -> TCM (Type'' Term Term)
forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
  where
    nonInferable :: MonadDebug m => m a
    nonInferable :: forall (m :: * -> *) a. MonadDebug m => m a
nonInferable = VerboseKey -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ (VerboseKey -> m a) -> VerboseKey -> m a
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> VerboseKey
unlines
      [ VerboseKey
"CheckInternal.infer: non-inferable term:"
      , VerboseKey
"  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Term
u
      ]

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

-- | @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 :: Action -> Type -> (Elims -> Term) -> Elims -> TCM (Type, Elims)
inferSpine :: Action
-> Type'' Term Term
-> (Elims -> Term)
-> Elims
-> TCMT IO (Type'' Term Term, Elims)
inferSpine Action
action Type'' Term Term
t Elims -> Term
hd Elims
es = Type'' Term Term
-> (Elims -> Term)
-> (Elims -> Elims)
-> Elims
-> TCMT IO (Type'' Term Term, Elims)
loop Type'' Term Term
t Elims -> Term
hd Elims -> Elims
forall a. a -> a
id Elims
es
  where
  loop :: Type'' Term Term
-> (Elims -> Term)
-> (Elims -> Elims)
-> Elims
-> TCMT IO (Type'' Term Term, Elims)
loop Type'' Term Term
t Elims -> Term
hd Elims -> Elims
acc = \case
    [] -> (Type'' Term Term, Elims) -> TCMT IO (Type'' Term Term, Elims)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term
t , Elims -> Elims
acc [])
    (Elim' Term
e : Elims
es) -> do
      let self :: Term
self = Elims -> Term
hd []
      VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
prettyTCM Elim' Term
e
        ]
      case Elim' Term
e of
        IApply Term
x Term
y Term
r -> do
          (a, b) <- Type'' Term Term
-> TCMT IO (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
shouldBePath Type'' Term Term
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' Term
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'' Term Term
-> TCMT IO (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
shouldBePi Type'' Term Term
t
          ai <- checkArgInfo action ai $ domInfo a
          v' <- applyDomToContext a $ checkInternal' action v CmpLeq $ unDom a
          let e' = Arg Term -> Elim' Term
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'' Term Term
-> ProjOrigin
-> QName
-> TCM (Type'' Term Term)
forall (m :: * -> *).
(PureTCM m, MonadTCError m, MonadBlock m) =>
Term
-> Type'' Term Term -> ProjOrigin -> QName -> m (Type'' Term Term)
shouldBeProjectible Term
self Type'' Term Term
t ProjOrigin
o QName
f
          loop t' (hd . (e:)) (acc . (e:)) es

checkSpine ::
     Action
  -> 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@.
  -> TCM Term   -- ^ The application after modification by the @Action@.
checkSpine :: Action
-> Type'' Term Term
-> (Elims -> Term)
-> Elims
-> Comparison
-> Type'' Term Term
-> TCM Term
checkSpine Action
action Type'' Term Term
a Elims -> Term
hd Elims
es Comparison
cmp Type'' Term Term
t = do
  VerboseKey -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
":"
                                 , 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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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
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
":"
                   , 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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t ] ]
  (t' , es') <- Action
-> Type'' Term Term
-> (Elims -> Term)
-> Elims
-> TCMT IO (Type'' Term Term, Elims)
inferSpine Action
action Type'' Term Term
a Elims -> Term
hd Elims
es
  reportSDoc "tc.check.internal" 30 $ sep
    [ "checking if "
    , prettyTCM t'
    , "is a subtype of"
    , prettyTCM t
    ]
  coerceSize cmp (hd es) t' t
  return $ hd es'

instance CheckInternal Sort where
  checkInternal' :: Action
-> Sort' Term
-> Comparison
-> TypeOf (Sort' Term)
-> TCMT IO (Sort' Term)
checkInternal' Action
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) -> TCM Level -> TCMT IO (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action -> Level -> TCM Level
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
action Level
l
    Inf Univ
u Integer
n  -> Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort' Term -> TCMT IO (Sort' Term))
-> Sort' Term -> TCMT IO (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 -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
forall t. Sort' t
SizeUniv
    Sort' Term
LockUniv -> Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
forall t. Sort' t
LockUniv
    Sort' Term
LevelUniv -> Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
forall t. Sort' t
LevelUniv
    Sort' Term
IntervalUniv -> Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO 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 -> Sort' Term -> TCMT IO (Sort' Term)
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
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 -> Sort' Term -> TCMT IO (Sort' Term)
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
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)
-> TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action -> Sort' Term -> TCMT IO (Sort' Term)
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
action Sort' Term
s
    MetaS MetaId
x Elims
es -> do -- we assume sort meta instantiations to be well-formed
      a <- MetaId -> TCM (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
metaType MetaId
x
      MetaS x <$> checkInternal' action es cmp (a , Sort . MetaS x)
    DefS QName
d Elims
es -> do
      a <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
      DefS d <$> checkInternal' action es cmp (a , Sort . DefS d)
    DummyS VerboseKey
s -> VerboseKey -> TCMT IO (Sort' Term)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s

instance CheckInternal Level where
  checkInternal' :: Action -> Level -> Comparison -> TypeOf Level -> TCM Level
checkInternal' Action
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)
-> TCMT IO [PlusLevel' Term] -> TCM Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PlusLevel' Term -> TCMT IO (PlusLevel' Term))
-> [PlusLevel' Term] -> TCMT IO [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 -> PlusLevel' Term -> TCMT IO (PlusLevel' Term)
forall a.
(CheckInternal a, TypeOf a ~ ()) =>
Action -> a -> TCMT IO a
inferInternal' Action
action) [PlusLevel' Term]
ls

instance CheckInternal PlusLevel where
  checkInternal' :: Action
-> PlusLevel' Term
-> Comparison
-> TypeOf (PlusLevel' Term)
-> TCMT IO (PlusLevel' Term)
checkInternal' Action
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) -> TCM Term -> TCMT IO (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM Term
checkLevelAtom Term
l
    where
    checkLevelAtom :: Term -> TCM Term
checkLevelAtom Term
l = do
      lvl <- TCM (Type'' Term Term)
forall (m :: * -> *). HasBuiltins m => m (Type'' Term Term)
levelType'
      checkInternal' action l CmpLeq lvl