{-# 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 = forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Type -> Constraint
CheckType Type
t) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
a -> 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return
  , postAction :: Type -> Term -> m Term
postAction      = \ Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return
  , modalityAction :: Modality -> Modality -> Modality
modalityAction  = \ Modality
_ -> forall a. a -> a
id
  , elimViewAction :: Term -> m Term
elimViewAction  = forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone
  }

eraseUnusedAction :: Action TCM
eraseUnusedAction :: Action (TCMT IO)
eraseUnusedAction = forall (m :: * -> *). PureTCM m => Action m
defaultAction { postAction :: Type -> Term -> TCMT IO Term
postAction = Type -> Term -> TCMT IO Term
eraseUnused }
  where
    eraseUnused :: Type -> Term -> TCM Term
    eraseUnused :: Type -> Term -> TCMT IO Term
eraseUnused Type
t = \case
      Def QName
f Elims
es -> do
        [Polarity]
pols <- forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
f
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f forall a b. (a -> b) -> a -> b
$ [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
      Term
v        -> 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) = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare Elim
e) forall a. a -> [a] -> [a]
: [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
    eraseIfNonvariant (Polarity
_          : [Polarity]
pols) (Elim
e : Elims
es) = Elim
e 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 = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' 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 = forall a (m :: * -> *).
(CheckInternal a, 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 = forall a (m :: * -> *).
(CheckInternal a, 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
s Term
t) Comparison
cmp TypeOf Type
_ = do
    Term
t' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
t Comparison
cmp (Sort -> Type
sort Sort
s)
    Sort
s' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
t'
    forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall t a. Sort' t -> a -> Type'' t a
El Sort
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 = forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> m a -> m a
verboseBracket String
"tc.check.internal" VerboseLevel
20 String
"" forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking internal "
      , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]
    forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking internal with DB indices"
      , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t ] ]
    Telescope
ctx <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Telescope
ctx) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"In context"
      , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ctx ] ]
    -- Bring projection-like funs in post-fix form,
    -- (even lone ones by default).
    Term
v <- forall (m :: * -> *). Action m -> Term -> m Term
elimViewAction Action m
action forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). Action m -> Type -> Term -> m Term
preAction Action m
action Type
t Term
v
    forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction Action m
action Type
t 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 <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m (Dom Type)
domOfBV VerboseLevel
i
        Name
n <- 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

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Bool
usableCohesion Dom Type
d) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Name -> Cohesion -> TypeError
VariableIsOfUnusableCohesion Name
n (forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
d)

        forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ TCMT IO Doc
"variable" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i) , TCMT IO Doc
"has type" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t e. Dom' t e -> e
unDom Dom Type
d)
          , TCMT IO Doc
"and modality", forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. LensModality a => a -> Modality
getModality Dom Type
d) ]
        forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
        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 <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
        forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"metavariable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
        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!
        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 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 <- 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
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Impossible -> VerboseLevel -> Substitution' a
strengthenS HasCallStack => Impossible
impossible (forall a. Sized a => a -> VerboseLevel
size Telescope
tel))
            forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a. VerboseLevel -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
vs) Elims
vs2
      Lit Literal
l      -> do
        Type
lt <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
l
        forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp Type
lt Type
t
        forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePiOrPath Type
t
        ArgInfo
ai <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
        let name :: String
name = [Suggestion] -> String
suggests [ forall a. Suggest a => a -> Suggestion
Suggestion Abs Term
vb , forall a. Suggest a => a -> Suggestion
Suggestion Abs Type
b ]
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
name, Dom Type
a) forall a b. (a -> b) -> a -> b
$ do
          ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Term
vb) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action (forall a. Subst a => Abs a -> a
absBody Abs Term
vb) Comparison
cmp (forall a. Subst a => Abs a -> a
absBody Abs Type
b)
      Pi Dom Type
a Abs Type
b     -> do
        Sort
s <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t
        forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"pi type should have sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort
s forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Term -> TypeError
FunctionTypeInSizeUniv Term
v
        Bool
experimental <- PragmaOptions -> Bool
optExperimentalIrrelevance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        let sa :: Sort
sa  = forall a. LensSort a => a -> Sort
getSort Dom Type
a
            sb :: Sort
sb  = forall a. LensSort a => a -> Sort
getSort (forall a. Abs a -> a
unAbs Abs Type
b)
            mkDom :: Term -> Dom Type
mkDom Term
v = forall t a. Sort' t -> a -> Type'' t a
El Sort
sa Term
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a
            mkRng :: Term -> Abs Type
mkRng Term
v = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term
v 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{}   -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext forall a b. (a -> b) -> a -> b
$ (forall a. Abs a -> String
absName Abs Type
b,) forall a b. (a -> b) -> a -> b
$
                forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
experimental (forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict) Dom Type
a
              NoAbs{} -> forall a. a -> a
id
        Dom Type
a <- Term -> Dom Type
mkDom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a) Comparison
CmpLeq (Sort -> Type
sort Sort
sa)
        Term
v' <- m Term -> m Term
goInside forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Abs Type
mkRng forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Type
b) Comparison
CmpLeq (Sort -> Type
sort Sort
sb)
        Sort
s' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
v -- Issue #6205: do not use v' since it might not be valid syntax
        forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s
        forall (m :: * -> *) a. Monad m => a -> m a
return Term
v'
      Sort Sort
s     -> do
        forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s
        Sort
s <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Sort
s
        Sort
s' <- forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort Sort
s
        Sort
s'' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t
        forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s''
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
s
      Level Level
l    -> do
        Level
l <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Level
l
        Type
lt <- forall (m :: * -> *). HasBuiltins m => m Type
levelType'
        forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp Type
lt Type
t
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
l
      DontCare Term
v -> Term -> Term
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
v Comparison
cmp Type
t
      -- Jesper, 2023-02-23: these can appear because of eta-expansion of
      -- records with irrelevant fields
      Dummy String
s Elims
_ -> 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
  forall (m :: * -> *).
MonadCheckInternal m =>
Hiding -> Hiding -> m ()
checkHiding    (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai)     (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai')
  Modality
mod <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Modality -> Modality -> m Modality
checkModality Action m
action (forall a. LensModality a => a -> Modality
getModality ArgInfo
ai)  (forall a. LensModality a => a -> Modality
getModality ArgInfo
ai')
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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' = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h Hiding
h') forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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') = (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod, forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod')
      (Quantity
q,Quantity
q') = (forall a. LensQuantity a => a -> Quantity
getQuantity  Modality
mod, forall a. LensQuantity a => a -> Quantity
getQuantity  Modality
mod')
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
mod Modality
mod') forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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 -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- add more cases when adding new modalities
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"CheckInternal.infer" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
  case Term
u of
    Var VerboseLevel
i Elims
es -> do
      Type
a <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
      forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
a (VerboseLevel -> Elims -> Term
Var VerboseLevel
i) Elims
es
    Def QName
f Elims
es -> do
      forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) forall a b. (a -> b) -> a -> b
$ \Projection
_ -> forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
      Type
a <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine 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 <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
      forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
a (MetaId -> Elims -> Term
MetaV MetaId
x) Elims
es
    Term
_ -> forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
  where
    nonInferable :: MonadDebug m => m a
    nonInferable :: forall (m :: * -> *) a. MonadDebug m => m a
nonInferable = forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"CheckInternal.infer: non-inferable term:"
      , String
"  " forall a. [a] -> [a] -> [a]
++ 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) = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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
    [] -> 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 []
      forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"inferring spine: "
        , TCMT IO Doc
"type t = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , TCMT IO Doc
"self  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self
        , TCMT IO Doc
"eliminated by e = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
e
        ]
      case Elim
e of
        IApply Term
x Term
y Term
r -> do
          (Dom Type
a, Abs Type
b) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePath Type
t
          Term
r' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
r Comparison
CmpLeq (forall t e. Dom' t e -> e
unDom Dom Type
a)
          Term
izero <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
          Term
ione  <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
          Term
x' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
x Comparison
CmpLeq (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
izero)
          Term
y' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
y Comparison
CmpLeq (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
ione)
          let e' :: Elim
e' = 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 forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
r) (Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
e'forall a. a -> [a] -> [a]
:)) Elims
es
        Apply (Arg ArgInfo
ai Term
v) -> do
          (Dom Type
a, Abs Type
b) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePi Type
t
          ArgInfo
ai <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
          Term
v' <- forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext (forall a. LensModality a => a -> Modality
getModality Dom Type
a) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
v Comparison
CmpLeq forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a
          let e' :: Elim
e' = forall a. Arg a -> Elim' a
Apply (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v')
          Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
v) (Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
e'forall a. a -> [a] -> [a]
:)) Elims
es
        -- case: projection or projection-like
        Proj ProjOrigin
o QName
f -> do
          Type
t' <- 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall 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
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" VerboseLevel
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"checking spine "
    , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                                 , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ])
                   , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                   , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]
  (Type
t' , Elims
es') <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
a Elims -> Term
hd Elims
es
  forall (m :: * -> *).
MonadConversion m =>
(Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
coerceSize (forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp) (Elims -> Term
hd Elims
es) Type
t' Type
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd Elims
es'

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

instance CheckInternal PlusLevel where
  checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel
checkInternal' Action m
action (Plus Integer
k Term
l) Comparison
_ TypeOf PlusLevel
_ = forall t. Integer -> t -> PlusLevel' t
Plus Integer
k 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 <- forall (m :: * -> *). HasBuiltins m => m Type
levelType'
      forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
l Comparison
CmpLeq Type
lvl