-- 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'
  , Action(..), defaultAction, eraseUnusedAction
  , infer
  , inferSort
  , 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.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.ProjectionLike (elimView)
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.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 :: Type -> m ()
checkType Type
t = m Sort -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m Sort -> m ()) -> m Sort -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> m Sort
forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
checkType' Type
t

-- | 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' :: Type -> m Sort
checkType' Type
t = do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"checking internal type "
    , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  Term
v <- Bool -> Term -> m Term
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasConstInfo m) =>
Bool -> Term -> m Term
elimView Bool
True (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
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 <- Type -> m Sort
forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
checkType' (Type -> m Sort) -> Type -> m Sort
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a
      Abs Sort
s2 <- (Abs Type
b Abs Type -> Sort -> Abs Sort
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (Sort -> Abs Sort) -> m Sort -> m (Abs Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        let goInside :: m a -> m a
goInside = case Abs Type
b of Abs{}   -> (VerboseKey, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b, Dom Type
a)
                                 NoAbs{} -> m a -> m a
forall a. a -> a
id
        m Sort -> m Sort
forall a. m a -> m a
goInside (m Sort -> m Sort) -> m Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Type -> m Sort
forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
checkType' (Type -> m Sort) -> Type -> m Sort
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b
      Dom Type -> Abs Sort -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, MonadDebug m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
s2
    Sort Sort
s -> do
      Sort
_ <- Action m -> Sort -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action m
forall (m :: * -> *). Monad m => Action m
defaultAction Sort
s
      Sort -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadConstraint m, HasOptions m) =>
Sort -> m Sort
inferUnivSort Sort
s
    Var VerboseLevel
i Elims
es   -> do
      Type
a <- VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
      Type -> Term -> Elims -> m Sort
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 (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 -> Term -> Elims -> m Sort
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 <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      Type -> Term -> Elims -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> Term -> Elims -> m Sort
checkTypeSpine Type
a (MetaId -> Elims -> Term
MetaV MetaId
x []) Elims
es
    v :: Term
v@Lam{}    -> TypeError -> m Sort
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m Sort) -> TypeError -> m Sort
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
InvalidType Term
v
    v :: Term
v@Con{}    -> TypeError -> m Sort
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m Sort) -> TypeError -> m Sort
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
InvalidType Term
v
    v :: Term
v@Lit{}    -> TypeError -> m Sort
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m Sort) -> TypeError -> m Sort
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
InvalidType Term
v
    v :: Term
v@Level{}  -> TypeError -> m Sort
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m Sort) -> TypeError -> m Sort
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
InvalidType Term
v
    DontCare Term
v -> Type -> m Sort
forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
checkType' (Type -> m Sort) -> Type -> m Sort
forall a b. (a -> b) -> a -> b
$ Type
t Type -> Term -> Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
v
    Dummy VerboseKey
s Elims
_  -> VerboseKey -> m Sort
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s

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


-- | 'checkInternal' traverses the whole 'Term', and we can use this
--   traversal to modify the term.
data Action m = Action
  { Action m -> Type -> Term -> m Term
preAction  :: Type -> Term -> m Term
    -- ^ Called on each subterm before the checker runs.
  , Action m -> Type -> Term -> m Term
postAction :: Type -> Term -> m Term
    -- ^ Called on each subterm after the type checking.
  , Action m -> Relevance -> Relevance -> Relevance
relevanceAction :: Relevance -> Relevance -> Relevance
    -- ^ Called for each @ArgInfo@.
    --   The first 'Relevance' is from the type,
    --   the second from the term.
  }

-- | The default action is to not change the 'Term' at all.
defaultAction :: Monad m => Action m
defaultAction :: Action m
defaultAction = Action :: forall (m :: * -> *).
(Type -> Term -> m Term)
-> (Type -> Term -> m Term)
-> (Relevance -> Relevance -> Relevance)
-> Action m
Action
  { preAction :: Type -> Term -> m Term
preAction       = \ Type
_ -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return
  , postAction :: Type -> Term -> m Term
postAction      = \ Type
_ -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return
  , relevanceAction :: Relevance -> Relevance -> Relevance
relevanceAction = \ Relevance
_ -> Relevance -> Relevance
forall a. a -> a
id
  }

eraseUnusedAction :: Action TCM
eraseUnusedAction :: Action TCM
eraseUnusedAction = Action TCM
forall (m :: * -> *). Monad m => Action m
defaultAction { postAction :: Type -> Term -> TCM Term
postAction = Type -> Term -> TCM Term
eraseUnused }
  where
    eraseUnused :: Type -> Term -> TCM Term
    eraseUnused :: Type -> Term -> TCM Term
eraseUnused Type
t Term
v = case Term
v of
      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 (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
_        -> Term -> TCM Term
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 (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

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

checkInternal' :: (MonadCheckInternal m) => Action m -> Term -> Comparison -> Type -> m Term
checkInternal' :: Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
cmp Type
t = VerboseKey -> VerboseLevel -> VerboseKey -> m Term -> m Term
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.check.internal" VerboseLevel
20 VerboseKey
"" (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"checking internal "
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]
  -- Bring projection-like funs in post-fix form,
  -- even lone ones (True).
  Term
v <- Bool -> Term -> m Term
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasConstInfo m) =>
Bool -> Term -> m Term
elimView Bool
True (Term -> m Term) -> m Term -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Action m -> Type -> Term -> m Term
forall (m :: * -> *). Action m -> Type -> Term -> m Term
preAction Action m
action Type
t Term
v
  Action m -> Type -> Term -> m Term
forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction Action m
action Type
t (Term -> m Term) -> m Term -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Term
v of
    Var VerboseLevel
i Elims
es   -> do
      Type
a <- VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
      VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
        [ TCM Doc
"variable" , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i) , TCM Doc
"has type" , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
      Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
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 (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 -> Term -> Elims -> Comparison -> Type -> m Term
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 <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"metavariable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"has type" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
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!
      ConHead
-> Elims
-> Type
-> (QName
    -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m Term)
-> m Term
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 ((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 -> Term -> Elims -> Comparison -> Type -> m Term
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
        Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Empty -> VerboseLevel -> Substitution' Term
forall a. Empty -> VerboseLevel -> Substitution' a
strengthenS Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel))
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Elims -> Elims
forall a. VerboseLevel -> [a] -> [a]
take (Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
vs) Elims
vs2
    Lit Literal
l      -> do
      Type
lt <- Literal -> m Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
l
      Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Comparison -> Type -> Type -> m ()
cmptype Comparison
cmp Type
lt Type
t
      Term -> m Term
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) <- m (Dom Type, Abs Type)
-> ((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
-> Maybe (Dom Type, Abs Type)
-> m (Dom Type, Abs Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> m (Dom Type, Abs Type)
shouldBePi Type
t) (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Dom Type, Abs Type) -> m (Dom Type, Abs Type))
-> m (Maybe (Dom Type, Abs Type)) -> m (Dom Type, Abs Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m (Maybe (Dom Type, Abs Type))
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath 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 :: VerboseKey
name = [Suggestion] -> VerboseKey
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 ]
      (VerboseKey, Dom Type) -> m Term -> m Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (VerboseKey
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
. VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs (Abs Term -> VerboseKey
forall a. Abs a -> VerboseKey
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 -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action (Abs Term -> Term
forall t a. Subst t a => Abs a -> a
absBody Abs Term
vb) Comparison
cmp (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b)
    Pi Dom Type
a Abs Type
b     -> do
      Sort
s <- Type -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall t. Sort' t
SizeUniv) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
FunctionTypeInSizeUniv Term
v
      let sa :: Sort
sa  = Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a
          sb :: Sort
sb  = Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)
          mkDom :: a -> Dom' Term (Type'' Term a)
mkDom a
v = Sort -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El Sort
sa a
v Type'' Term a -> Dom Type -> Dom' Term (Type'' Term a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a
          mkRng :: a -> Abs (Type'' Term a)
mkRng a
v = (Type -> Type'' Term a) -> Abs Type -> Abs (Type'' Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a
v a -> Type -> Type'' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Abs Type
b
          -- Preserve NoAbs
          goInside :: m a -> m a
goInside = case Abs Type
b of Abs{}   -> (VerboseKey, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b, Dom Type
a)
                               NoAbs{} -> m a -> m a
forall a. a -> a
id
      Dom Type
a <- Term -> Dom Type
forall a. a -> Dom' Term (Type'' Term a)
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 -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> 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 -> Type
sort Sort
sa)
      Term
v' <- m Term -> m Term
forall a. m a -> m a
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
forall a. a -> Abs (Type'' Term a)
mkRng (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> 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 -> Type
sort Sort
sb)
      Sort
s' <- Term -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m) =>
Term -> m Sort
sortOf Term
v'
      Comparison -> Sort -> Sort -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s
      Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v'
    Sort Sort
s     -> do
      VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checking sort" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s
      Sort
s <- Action m -> Sort -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action m
action Sort
s
      Sort
s' <- Sort -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadConstraint m, HasOptions m) =>
Sort -> m Sort
inferUnivSort Sort
s
      Sort
s'' <- Type -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t
      Comparison -> Sort -> Sort -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s''
      Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
s
    Level Level
l    -> do
      Level
l <- Action m -> Level -> m Level
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Level -> m Level
checkLevel Action m
action Level
l
      Type
lt <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
      Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Comparison -> Type -> Type -> m ()
cmptype Comparison
cmp Type
lt Type
t
      Term -> m Term
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 -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
cmp Type
t
    Dummy VerboseKey
s Elims
_ -> VerboseKey -> m Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
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 :: 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) <- Type -> m (TelView, Boundary)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins 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.
  Telescope -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Type
-> (MetaId -> Type -> m a) -> (NotBlocked -> Type -> m a) -> m a
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\MetaId
m Type
t -> m a
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation) ((NotBlocked -> Type -> m a) -> m a)
-> (NotBlocked -> Type -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \NotBlocked
_ Type
t -> do
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t m (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe ((QName, Type, Args), Type)
Nothing ->
        TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
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 (VerboseLevel -> Elims -> Elims
forall t a. Subst t a => VerboseLevel -> a -> a
raise (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel) Elims
vs Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Telescope -> Boundary -> Elims
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 :: Action m -> Type -> Term -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a Term
self Elims
es Comparison
cmp Type
t = do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.check.internal" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"checking spine "
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
                                 , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ])
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Elims -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]
  ((Term
v, Term
v'), Type
t') <- Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), 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
  Type
t' <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t'
  Term
v' Term -> m () -> m Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (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 :: * -> *).
MonadCheckInternal m =>
Comparison -> Type -> Type -> m ()
cmptype 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 :: 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')
  Relevance
r <- Action m -> Relevance -> Relevance -> m Relevance
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Relevance -> Relevance -> m Relevance
checkRelevance Action m
action (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai)  (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai')
  ArgInfo -> m ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
forall a b. (a -> b) -> a -> b
$ Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
r ArgInfo
ai

checkHiding    :: (MonadCheckInternal m) => Hiding -> Hiding -> m ()
checkHiding :: 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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@.
checkRelevance :: (MonadCheckInternal m) => Action m -> Relevance -> Relevance -> m Relevance
checkRelevance :: Action m -> Relevance -> Relevance -> m Relevance
checkRelevance Action m
action Relevance
r Relevance
r' = do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
r') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Relevance -> Relevance -> TypeError
RelevanceMismatch Relevance
r Relevance
r'
  Relevance -> m Relevance
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance -> m Relevance) -> Relevance -> m Relevance
forall a b. (a -> b) -> a -> b
$ Action m -> Relevance -> Relevance -> Relevance
forall (m :: * -> *).
Action m -> Relevance -> Relevance -> Relevance
relevanceAction Action m
action Relevance
r' Relevance
r  -- Argument order for actions: @type@ @term@

-- | Infer type of a neutral term.
infer :: (MonadCheckInternal m) => Term -> m Type
infer :: Term -> m Type
infer Term
v = do
  case Term
v of
    Var VerboseLevel
i Elims
es   -> do
      Type
a <- VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
      (Term, Type) -> Type
forall a b. (a, b) -> b
snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> m (Term, Type)
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) -> QName -> Arg Term -> Elims -> m Type
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             -> QName -> Elims -> m Type
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 <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      (Term, Type) -> Type
forall a b. (a, b) -> b
snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> Term -> Elims -> m (Term, Type)
inferSpine Type
a (MetaId -> Elims -> Term
MetaV MetaId
x []) Elims
es
    Term
_ -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Infer ordinary function application.
inferDef :: (MonadCheckInternal m) => QName -> Elims -> m Type
inferDef :: QName -> Elims -> m Type
inferDef QName
f 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
f
  (Term, Type) -> Type
forall a b. (a, b) -> b
snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> m (Term, Type)
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' :: QName -> Arg Term -> Elims -> m Type
inferDef' QName
f Arg Term
a Elims
es = do
  Maybe Projection
isProj <- QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
f
  case Maybe Projection
isProj of
    Just Projection{ projIndex :: Projection -> VerboseLevel
projIndex = VerboseLevel
n } | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 -> do
      let self :: Term
self = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a
      Type
b <- Term -> m Type
forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer Term
self
      (Term, Type) -> Type
forall a b. (a, b) -> b
snd ((Term, Type) -> Type) -> m (Term, Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> Term -> Elims -> m (Term, Type)
inferSpine Type
b Term
self (ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es)
    Maybe Projection
_ -> QName -> Elims -> m Type
forall (m :: * -> *).
MonadCheckInternal m =>
QName -> Elims -> m Type
inferDef QName
f (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
a Elim -> Elims -> Elims
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 :: Type -> Term -> Elims -> m (Term, Type)
inferSpine Type
a Term
v Elims
es = ((Term, Term) -> Term) -> ((Term, Term), Type) -> (Term, Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Term, Term) -> Term
forall a b. (a, b) -> a
fst (((Term, Term), Type) -> (Term, Type))
-> m ((Term, Term), Type) -> m (Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
inferSpine' Action m
forall (m :: * -> *). Monad 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' :: Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
inferSpine' Action m
action Type
t Term
self Term
self' [] = ((Term, Term), Type) -> m ((Term, Term), Type)
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
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.infer.internal" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"inferSpine': "
    , TCM Doc
"type t = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , TCM Doc
"self  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self
    , TCM Doc
"self' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self'
    , TCM Doc
"eliminated by e = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
e
    ]
  case Elim
e of
    IApply Term
x Term
y Term
r -> do
      (Dom Type
a, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> m (Dom Type, Abs Type)
shouldBePath Type
t
      Term
r' <- Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> 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 -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
x Comparison
CmpLeq (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
izero)
      Term
y' <- Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
y Comparison
CmpLeq (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
ione)
      Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
inferSpine' Action m
action (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
r) (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim
e]) (Term
self' Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Term -> Term -> Term -> Elim
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) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
MonadCheckInternal 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' <- Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
CmpLeq (Type -> m Term) -> Type -> m Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a
      Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
inferSpine' Action m
action (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
v) (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim
e]) (Term
self' Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [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')]) Elims
es
    -- case: projection or projection-like
    Proj ProjOrigin
o QName
f -> do
      (Dom Type
a, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> m (Dom Type, Abs Type)
shouldBePi (Type -> m (Dom Type, Abs Type))
-> m Type -> m (Dom Type, Abs Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> QName -> m Type
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> QName -> m Type
shouldBeProjectible Type
t QName
f
      Term
u  <- ProjOrigin -> QName -> Arg Term -> m Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
self)
      Term
u' <- ProjOrigin -> QName -> Arg Term -> m Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
self')
      Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
inferSpine' Action m
action (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> 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 :: Type -> QName -> m Type
shouldBeProjectible Type
t QName
f = Type
-> (MetaId -> Type -> m Type)
-> (NotBlocked -> Type -> m Type)
-> m Type
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t
  (\MetaId
m Type
t -> m Type
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation)
  (\NotBlocked
_ Type
t -> m Type -> (Type -> m Type) -> Maybe Type -> m Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Type
forall a. m a
failure Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> m Type) -> m (Maybe Type) -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> Type -> m (Maybe Type)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t)
  where failure :: m a
failure = TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
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 :: Type -> m (Dom Type, Abs Type)
shouldBePath Type
t = Type
-> (MetaId -> Type -> m (Dom Type, Abs Type))
-> (NotBlocked -> Type -> m (Dom Type, Abs Type))
-> m (Dom Type, Abs Type)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t
  (\MetaId
m Type
t -> m (Dom Type, Abs Type)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation)
  (\NotBlocked
_ Type
t -> do
      Maybe (Dom Type, Abs Type)
m <- Type -> m (Maybe (Dom Type, Abs Type))
forall (m :: * -> *).
(MonadReduce m, HasBuiltins 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  -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type, Abs Type)
p
        Maybe (Dom Type, Abs Type)
Nothing -> TypeError -> m (Dom Type, Abs Type)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m (Dom Type, Abs Type))
-> TypeError -> m (Dom Type, Abs Type)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePath Type
t)

shouldBePi :: (MonadCheckInternal m) => Type -> m (Dom Type, Abs Type)
shouldBePi :: Type -> m (Dom Type, Abs Type)
shouldBePi Type
t = Type
-> (MetaId -> Type -> m (Dom Type, Abs Type))
-> (NotBlocked -> Type -> m (Dom Type, Abs Type))
-> m (Dom Type, Abs Type)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t
  (\MetaId
m Type
t -> m (Dom Type, Abs Type)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation)
  (\NotBlocked
_ Type
t -> case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
      Pi Dom Type
a Abs Type
b -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
a , Abs Type
b)
      Term
_      -> TypeError -> m (Dom Type, Abs Type)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m (Dom Type, Abs Type))
-> TypeError -> m (Dom Type, Abs Type)
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 :: Action m -> Sort -> m Sort
checkSort Action m
action Sort
s =
  case Sort
s of
    Type Level
l   -> Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Level -> m Level
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Level -> m Level
checkLevel Action m
action Level
l
    Prop Level
l   -> Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Level -> m Level
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Level -> m Level
checkLevel Action m
action Level
l
    Sort
Inf      -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
Inf
    Sort
SizeUniv -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
SizeUniv
    PiSort Dom Type
dom Abs Sort
s2 -> do
      let El Sort
s1 Term
a = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
      Sort
s1' <- Action m -> Sort -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action m
action Sort
s1
      Term
a' <- Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
a Comparison
CmpLeq (Type -> m Term) -> Type -> m Term
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
s1'
      let dom' :: Dom Type
dom' = Dom Type
dom Dom Type -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s1' Term
a'
      Abs Sort
s2' <- Dom Type -> (Sort -> m Sort) -> Abs Sort -> m (Abs Sort)
forall t a t' b (m :: * -> *).
(Subst t a, Subst t' b, Free b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
dom' (Action m -> Sort -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action m
action) Abs Sort
s2
      Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort Dom Type
dom' Abs Sort
s2'
    FunSort Sort
s1 Sort
s2 -> do
      Sort
s1' <- Action m -> Sort -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action m
action Sort
s1
      Sort
s2' <- Action m -> Sort -> m Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action m
action Sort
s2
      Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1' Sort
s2'
    UnivSort Sort
s -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort) -> m Sort -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Sort -> m Sort
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 <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      let self :: Term
self = Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x []
      ((Term
_,Term
v),Type
_) <- Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), 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     -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        MetaV MetaId
x Elims
es -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x Elims
es
        Def QName
d Elims
es   -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es
        Term
_          -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    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
      let self :: Term
self = Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d []
      ((Term
_,Term
v),Type
_) <- Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), 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     -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
        MetaV MetaId
x Elims
es -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x Elims
es
        Def QName
d Elims
es   -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es
        Term
_          -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    DummyS VerboseKey
s -> VerboseKey -> m Sort
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s

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

    checkLevelAtom :: LevelAtom' Term -> m (LevelAtom' Term)
checkLevelAtom LevelAtom' Term
l = do
      Type
lvl <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
      Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case LevelAtom' Term
l of
        MetaLevel MetaId
x Elims
es   -> Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) Comparison
CmpLeq Type
lvl
        BlockedLevel MetaId
_ Term
v -> Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
CmpLeq Type
lvl
        NeutralLevel NotBlocked
_ Term
v -> Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
CmpLeq Type
lvl
        UnreducedLevel Term
v -> Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
CmpLeq Type
lvl

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

-- | Compute the sort of a type.

inferSort :: (MonadCheckInternal m) => Term -> m Sort
inferSort :: Term -> m Sort
inferSort Term
t = case Term
t of
    Var VerboseLevel
i Elims
es   -> do
      Type
a <- VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
      (Term
_, Type
s) <- Term -> Type -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Type -> Elims -> m (Term, Type)
eliminate (VerboseLevel -> Elims -> Term
Var VerboseLevel
i []) Type
a Elims
es
      Type -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
s
    Def QName
f Elims
es   -> do  -- f is not projection(-like)!
      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
      (Term
_, Type
s) <- Term -> Type -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Type -> Elims -> m (Term, Type)
eliminate (QName -> Elims -> Term
Def QName
f []) Type
a Elims
es
      Type -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
s
    MetaV MetaId
x Elims
es -> do
      Type
a <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      (Term
_, Type
s) <- Term -> Type -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Type -> Elims -> m (Term, Type)
eliminate (MetaId -> Elims -> Term
MetaV MetaId
x []) Type
a Elims
es
      Type -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
s
    Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Sort -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, MonadDebug m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a (Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> Abs Type -> Abs Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
    Sort Sort
s     -> Sort -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadConstraint m, HasOptions m) =>
Sort -> m Sort
inferUnivSort Sort
s
    Con{}      -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit{}      -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lam{}      -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    Level{}    -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{} -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy VerboseKey
s Elims
_  -> VerboseKey -> m Sort
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s

-- | @eliminate t self es@ eliminates value @self@ of type @t@ by spine @es@
--   and returns the remaining value and its type.
eliminate :: (MonadCheckInternal m) => Term -> Type -> Elims -> m (Term, Type)
eliminate :: Term -> Type -> Elims -> m (Term, Type)
eliminate Term
self Type
t [] = (Term, Type) -> m (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
self, Type
t)
eliminate Term
self Type
t (Elim
e : Elims
es) = case Elim
e of
    Apply (Arg ArgInfo
_ Term
v) -> Type
-> (Type -> m (Term, Type))
-> (Dom Type -> Abs Type -> m (Term, Type))
-> m (Term, Type)
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
t Type -> m (Term, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ {-else-} ((Dom Type -> Abs Type -> m (Term, Type)) -> m (Term, Type))
-> (Dom Type -> Abs Type -> m (Term, Type)) -> m (Term, Type)
forall a b. (a -> b) -> a -> b
$ \ Dom Type
_ Abs Type
b ->
      Term -> Type -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Type -> Elims -> m (Term, Type)
eliminate (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim
e]) (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
v) Elims
es
    IApply Term
_ Term
_ Term
v -> do
      (Dom Type
_, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> m (Dom Type, Abs Type)
shouldBePath Type
t
      Term -> Type -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Type -> Elims -> m (Term, Type)
eliminate (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim
e]) (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
v) Elims
es
    -- case: projection or projection-like
    Proj ProjOrigin
o QName
f -> do
      (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai}, Abs Type
b) <- Type -> m (Dom Type, Abs Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> m (Dom Type, Abs Type)
shouldBePi (Type -> m (Dom Type, Abs Type))
-> m Type -> m (Dom Type, Abs Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> QName -> m Type
forall (m :: * -> *).
MonadCheckInternal m =>
Type -> QName -> m Type
shouldBeProjectible Type
t QName
f
      Term
u  <- ProjOrigin -> QName -> Arg Term -> m Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Arg Term -> m Term) -> Arg Term -> m Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
self
      Term -> Type -> Elims -> m (Term, Type)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Type -> Elims -> m (Term, Type)
eliminate Term
u (Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
self) Elims
es