{-# OPTIONS_GHC -Wunused-imports #-}

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

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

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

import Control.Monad

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

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

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

import Agda.Utils.Impossible

import Agda.Interaction.Options

-- * Bidirectional rechecker

type MonadCheckInternal m = MonadConversion m

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

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

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

eraseUnusedAction :: Action TCM
eraseUnusedAction :: Action TCM
eraseUnusedAction = Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction { postAction = eraseUnused }
  where
    eraseUnused :: Type -> Term -> TCM Term
    eraseUnused :: Type -> Term -> TCM Term
eraseUnused Type
t = \case
      Def QName
f Elims
es -> do
        [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 ()

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

instance CheckInternal Type where
  checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Comparison -> TypeOf Type -> m Type
checkInternal' Action m
action (El Sort' Term
s Term
t) Comparison
cmp TypeOf Type
_ = do
    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 -> Int -> String -> m Term -> m Term
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.check.internal" Int
20 String
"" (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking internal "
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t ] ]
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking internal with DB indices"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t ] ]
    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 -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"In context"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ 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 Int
i Elims
es   -> do
        Dom Type
d <- Int -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i
        Name
n <- Int -> m Name
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
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 -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
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 (Int -> Term
var Int
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) (Int -> Elims -> Term
Var Int
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 -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"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 -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel))
            (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
take (Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
vs) Elims
vs2
      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 -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"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 -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort' Term -> m Doc
prettyTCM Sort' Term
s
        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@

{-# SPECIALIZE infer :: Term -> TCM Type #-}
-- | Infer type of a neutral term.
infer :: (MonadCheckInternal m) => Term -> m Type
infer :: forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer Term
u = do
  String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"CheckInternal.infer" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
  case Term
u of
    Var Int
i Elims
es -> do
      Type
a <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
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 (Int -> Elims -> Term
Var Int
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

{-# SPECIALIZE inferSpine :: Action TCM -> Type -> (Elims -> Term) -> Elims -> TCM (Type, Elims) #-}
-- | @inferSpine action t hd es@ checks that spine @es@ eliminates
--   value @hd []@ of type @t@ and returns the remaining type
--   (target of elimination) and the transformed eliminations.
inferSpine :: (MonadCheckInternal m) => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
t Elims -> Term
hd Elims
es = Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t Elims -> Term
hd Elims -> Elims
forall a. a -> a
id Elims
es
  where
  loop :: Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t Elims -> Term
hd Elims -> Elims
acc = \case
    [] -> (Type, Elims) -> m (Type, Elims)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t , Elims -> Elims
acc [])
    (Elim
e : Elims
es) -> do
      let self :: Term
self = Elims -> Term
hd []
      String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"inferring spine: "
        , TCMT IO Doc
"type t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        , TCMT IO Doc
"self  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
self
        , TCMT IO Doc
"eliminated by e = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elim
e
        ]
      case Elim
e of
        IApply Term
x Term
y Term
r -> do
          (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

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