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

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

module Agda.TypeChecking.CheckInternal
  ( MonadCheckInternal
  , checkType
  , checkType'
  , checkSort
  , checkInternal
  , checkInternal'
  , checkInternalType'
  , Action(..), defaultAction, eraseUnusedAction
  , infer
  , inferSpine'
  , shouldBeSort
  ) where

import Control.Arrow (first)
import Control.Monad

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

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


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

import Agda.Utils.Impossible

-- * Bidirectional rechecker

type MonadCheckInternal m = MonadConversion m

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

-- | Entry point for e.g. checking WithFunctionType.
checkType :: (MonadCheckInternal m) => Type -> m ()
checkType :: forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
t = forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Type -> Constraint
CheckType Type
t) forall a b. (a -> b) -> a -> b
$ do
  Sort
inferred <- forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
checkType' Type
t
  forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (forall a. LensSort a => a -> Sort
getSort Type
t) Sort
inferred

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

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

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

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

-- | The default action is to not change the 'Term' at all.
defaultAction :: PureTCM m => Action m
--(MonadReduce m, MonadTCEnv m, HasConstInfo m) => Action m
defaultAction :: forall (m :: * -> *). PureTCM m => Action m
defaultAction = Action
  { 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

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

checkInternal' :: (MonadCheckInternal m) => Action m -> Term -> Comparison -> Type -> m Term
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
cmp Type
t = forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.check.internal" VerboseLevel
20 ArgName
"" forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
      Type
a <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 Type
a ]
      forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (VerboseLevel -> Elims -> Term
Var VerboseLevel
i []) Elims
es Comparison
cmp Type
t
    Def QName
f Elims
es   -> do  -- f is not projection(-like)!
      Type
a <- Definition -> Type
defType 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 -> 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 =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 -> 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.
MonadCheckInternal 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 -> 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 b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *).
MonadCheckInternal m =>
Type -> m (Dom Type, Abs Type)
shouldBePi Type
t) forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath 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 :: ArgName
name = [Suggestion] -> ArgName
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 (ArgName
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. ArgName -> a -> Abs a
Abs (forall a. Abs a -> ArgName
absName Abs Term
vb) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
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 (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
      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. Abs a -> ArgName
absName Abs Type
b, 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 (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
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 (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
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) => 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 =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort 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 (m :: * -> *).
MonadCheckInternal m =>
Action m -> Level -> m Level
checkLevel 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 (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
cmp Type
t
    Dummy ArgName
s Elims
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s

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

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

-- | @checkArgInfo actual expected@.
--
--   The @expected@ 'ArgInfo' comes from the type.
--   The @actual@ 'ArgInfo' comes from the term and can be updated
--   by an action.
checkArgInfo :: (MonadCheckInternal m) => Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai ArgInfo
ai' = do
  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 = \case
    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) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Type -> Term -> Elims -> m (Term, Type)
inferSpine Type
a (VerboseLevel -> Elims -> Term
Var VerboseLevel
i   []) Elims
es
    Def QName
f (Apply Arg Term
a : Elims
es) -> forall (m :: * -> *).
MonadCheckInternal m =>
QName -> Arg Term -> Elims -> m Type
inferDef' QName
f Arg Term
a Elims
es -- possibly proj.like
    Def QName
f Elims
es             -> forall (m :: * -> *).
MonadCheckInternal m =>
QName -> Elims -> m Type
inferDef  QName
f   Elims
es -- not a projection-like fun
    MetaV MetaId
x Elims
es -> do -- we assume meta instantiations to be well-typed
      Type
a <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
      forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Type -> Term -> Elims -> m (Term, Type)
inferSpine Type
a (MetaId -> Elims -> Term
MetaV MetaId
x []) Elims
es
    Term
v -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ forall a b. (a -> b) -> a -> b
$ [ArgName] -> ArgName
unlines
      [ ArgName
"CheckInternal.infer: non-inferable term:"
      , ArgName
"  " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow Term
v
      ]

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

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


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

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

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

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

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

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

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

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

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