{-# OPTIONS_GHC -Wunused-imports #-}

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

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

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

import Control.Monad

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

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

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

import Agda.Utils.Impossible

import Agda.Interaction.Options

-- * Bidirectional rechecker

type MonadCheckInternal m = MonadConversion m

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

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

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

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

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

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

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

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

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

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

instance CheckInternal Term where
  checkInternal' :: (MonadCheckInternal m) => Action m -> Term -> Comparison -> Type -> m Term
  checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
cmp Type
t = String -> VerboseLevel -> String -> m Term -> m Term
forall a. String -> VerboseLevel -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> m a -> m a
verboseBracket String
"tc.check.internal" VerboseLevel
20 String
"" (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
    String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t ] ]
    String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking internal with DB indices"
      , 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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Bool
forall a. Tele a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Telescope
ctx) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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
forall (m :: * -> *). MonadPretty m => Telescope -> 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
        Dom Type
d <- VerboseLevel -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m (Dom Type)
domOfBV VerboseLevel
i
        Name
n <- VerboseLevel -> m Name
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Name
nameOfBV VerboseLevel
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

        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dom Type -> Bool
forall a. LensCohesion a => a -> Bool
usableCohesion Dom Type
d) (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
$ Name -> Cohesion -> TypeError
VariableIsOfUnusableCohesion Name
n (Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
d)

        String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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
forall (m :: * -> *). MonadPretty m => Term -> 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
d)
          , TCMT IO Doc
"and modality", Modality -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
d) ]
        Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
d) (VerboseLevel -> Elims -> Term
Var VerboseLevel
i) Elims
es Comparison
cmp Type
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!
        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 -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (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 :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
        String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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
forall (m :: * -> *). MonadPretty m => MetaId -> 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
        Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (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.
(PureTCM m, MonadBlock m, MonadTCError m) =>
ConHead
-> Elims
-> Type
-> (QName
    -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
-> m a
fullyApplyCon ConHead
c Elims
vs Type
t ((QName
  -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m Term)
 -> m Term)
-> (QName
    -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m Term)
-> m Term
forall a b. (a -> b) -> a -> b
$ \ QName
_d Type
_dt Args
_pars Type
a Elims
vs' Telescope
tel Type
t -> do
          Con ConHead
c ConInfo
ci Elims
vs2 <- Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
vs' Comparison
cmp Type
t
          -- Strip away the extra arguments
          Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> 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
      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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
      Lam ArgInfo
ai Abs Term
vb  -> do
        (Dom Type
a, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePiOrPath 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 :: String
name = [Suggestion] -> String
suggests [ Abs Term -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs Term
vb , Abs Type -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs Type
b ]
        (String, Dom Type) -> m Term -> m Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
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
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs (Abs Term -> String
forall a. Abs a -> String
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 -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action (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' Term
s <- Type -> m (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m (Sort' Term)
shouldBeSort Type
t
        String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"pi type should have 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
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort' Term
s Sort' Term -> Sort' Term -> Bool
forall a. Eq a => a -> a -> Bool
== Sort' Term
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
        Bool
experimental <- PragmaOptions -> Bool
optExperimentalIrrelevance (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        let sa :: Sort' Term
sa  = Dom Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Dom Type
a
            sb :: Sort' Term
sb  = Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)
            mkDom :: Term -> Dom Type
mkDom Term
v = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
sa Term
v Type -> Dom Type -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a
            mkRng :: Term -> Abs Type
mkRng Term
v = (Type -> Type) -> Abs Type -> Abs Type
forall a b. (a -> b) -> Abs a -> Abs b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term
v Term -> Type -> Type
forall a b. a -> Type'' Term b -> Type'' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Abs Type
b
            -- Preserve NoAbs
            goInside :: m Term -> m Term
goInside = case Abs Type
b of
              Abs{}   -> (String, Dom Type) -> m Term -> m Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext ((String, Dom Type) -> m Term -> m Term)
-> (String, Dom Type) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b,) (Dom Type -> (String, Dom Type)) -> Dom Type -> (String, Dom Type)
forall a b. (a -> b) -> a -> b
$
                Bool -> (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
experimental ((Relevance -> Relevance) -> Dom Type -> Dom Type
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict) 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 -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action (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' Term -> Type
sort Sort' Term
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 -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action (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' Term -> Type
sort Sort' Term
sb)
        Sort' Term
s' <- Term -> m (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m (Sort' Term)
sortOf Term
v -- Issue #6205: do not use v' since it might not be valid syntax
        Comparison -> Sort' Term -> Sort' Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort' Term -> Sort' Term -> m ()
compareSort Comparison
cmp Sort' Term
s' Sort' Term
s
        Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v'
      Sort Sort' Term
s     -> do
        String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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' 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
        Sort' Term
s <- Action m -> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
forall (m :: * -> *).
(MonadCheckInternal m, TypeOf (Sort' Term) ~ ()) =>
Action m -> Sort' Term -> m (Sort' Term)
inferInternal' Action m
action Sort' Term
s
        Sort' Term
s' <- Sort' Term -> m (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort' Term -> m (Sort' Term)
inferUnivSort Sort' Term
s
        Sort' Term
s'' <- Type -> m (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m (Sort' Term)
shouldBeSort Type
t
        Comparison -> Sort' Term -> Sort' Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort' Term -> Sort' Term -> m ()
compareSort Comparison
cmp Sort' Term
s' Sort' Term
s''
        Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
Sort Sort' Term
s
      Level Level
l    -> do
        Level
l <- Action m -> Level -> m Level
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
forall (m :: * -> *).
(MonadCheckInternal m, TypeOf Level ~ ()) =>
Action m -> Level -> m Level
inferInternal' Action m
action Level
l
        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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ 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 -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action Term
v Comparison
cmp TypeOf Term
Type
t
      -- Jesper, 2023-02-23: these can appear because of eta-expansion of
      -- records with irrelevant fields
      Dummy String
s Elims
_ -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v -- __IMPOSSIBLE_VERBOSE__ s

-- | @checkArgInfo actual expected@.
--
--   The @expected@ 'ArgInfo' comes from the type.
--   The @actual@ 'ArgInfo' comes from the term and can be updated
--   by an action.
checkArgInfo :: (MonadCheckInternal m) => Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai ArgInfo
ai' = do
  Hiding -> Hiding -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Hiding -> Hiding -> m ()
checkHiding    (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai)     (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai')
  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 a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Modality -> m Modality) -> Modality -> m Modality
forall a b. (a -> b) -> a -> b
$ Action m -> Modality -> Modality -> Modality
forall (m :: * -> *). Action m -> Modality -> Modality -> Modality
modalityAction Action m
action Modality
mod' Modality
mod  -- Argument order for actions: @type@ @term@

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

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

-- | @inferSpine action t hd es@ checks that spine @es@ eliminates
--   value @hd []@ of type @t@ and returns the remaining type
--   (target of elimination) and the transformed eliminations.
inferSpine :: (MonadCheckInternal m) => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
t Elims -> Term
hd Elims
es = Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t Elims -> Term
hd Elims -> Elims
forall a. a -> a
id Elims
es
  where
  loop :: Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t Elims -> Term
hd Elims -> Elims
acc = \case
    [] -> (Type, Elims) -> m (Type, Elims)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t , Elims -> Elims
acc [])
    (Elim
e : Elims
es) -> do
      let self :: Term
self = Elims -> Term
hd []
      String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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
"inferring spine: "
        , TCMT IO Doc
"type t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        , TCMT IO Doc
"self  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
self
        , TCMT IO Doc
"eliminated by e = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elim
e
        ]
      case Elim
e of
        IApply Term
x Term
y Term
r -> do
          (Dom Type
a, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePath Type
t
          Term
r' <- Action m -> Term -> Comparison -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action Term
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 -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action Term
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 -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action Term
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)
          let e' :: Elim
e' = Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply Term
x' Term
y' Term
r'
          Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop (Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
r) (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc (Elims -> Elims) -> (Elims -> Elims) -> Elims -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
e'Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
        Apply (Arg ArgInfo
ai Term
v) -> do
          (Dom Type
a, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError 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' <- Modality -> m Term -> m Term
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext (Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
a) (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ Action m -> Term -> Comparison -> TypeOf Term -> m Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' Action m
action Term
v Comparison
CmpLeq (TypeOf Term -> m Term) -> TypeOf Term -> m Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a
          let e' :: Elim
e' = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v')
          Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop (Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v) (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc (Elims -> Elims) -> (Elims -> Elims) -> Elims -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
e'Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
        -- case: projection or projection-like
        Proj ProjOrigin
o QName
f -> do
          Type
t' <- Term -> Type -> ProjOrigin -> QName -> m Type
forall (m :: * -> *).
(PureTCM m, MonadTCError m, MonadBlock m) =>
Term -> Type -> ProjOrigin -> QName -> m Type
shouldBeProjectible Term
self Type
t ProjOrigin
o QName
f
          Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t' (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc (Elims -> Elims) -> (Elims -> Elims) -> Elims -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es

checkSpine
  :: (MonadCheckInternal m)
  => Action m
  -> Type       -- ^ Type of the head @self@.
  -> (Elims -> Term) -- ^ The head @hd@.
  -> Elims      -- ^ The eliminations @es@.
  -> Comparison -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the final type.
  -> Type       -- ^ Expected type of the application @self es@.
  -> m Term     -- ^ The application after modification by the @Action@.
checkSpine :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a Elims -> Term
hd Elims
es Comparison
cmp Type
t = do
  String -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"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
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t ] ]
  (Type
t' , Elims
es') <- Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
a Elims -> Term
hd Elims
es
  (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) (Elims -> Term
hd Elims
es) Type
t' Type
t
  Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd Elims
es'

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

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

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