-- 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.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 = Constraint -> m () -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Type -> Constraint
CheckType Type
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  Sort
inferred <- Type -> m Sort
forall (m :: * -> *). MonadCheckInternal m => Type -> m Sort
checkType' Type
t
  Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Type -> Sort
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' :: 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 <- ProjEliminator -> Term -> m Term
forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone (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 Sort -> m Sort
goInside = case Abs Type
b of Abs{}   -> (VerboseKey, Dom Type) -> m Sort -> m Sort
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 Sort -> m Sort
forall a. a -> a
id
        m Sort -> m Sort
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 :: * -> *). PureTCM 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 :: * -> *). PureTCM m => Action m
defaultAction Sort
s
      Sort -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadConstraint 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.
(HasCallStack, MonadTCError 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.
(HasCallStack, MonadTCError 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.
(HasCallStack, MonadTCError 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.
(HasCallStack, MonadTCError 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 :: * -> *).
(PureTCM m, MonadBlock 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

checkInternalType' :: (MonadCheckInternal m) => Action m -> Type -> m Type
checkInternalType' :: 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 <- Action m -> Term -> Comparison -> Type -> m Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
act Term
t Comparison
CmpLeq (Sort -> Type
sort Sort
s)
  Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return El :: forall t a. Sort' t -> a -> Type'' t a
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
  { 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 -> Modality -> Modality -> Modality
modalityAction :: Modality -> Modality -> Modality
    -- ^ Called for each @ArgInfo@.
    --   The first 'Modality' is from the type,
    --   the second from the term.
  , 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 :: Action m
defaultAction = Action :: forall (m :: * -> *).
(Type -> Term -> m Term)
-> (Type -> Term -> m Term)
-> (Modality -> Modality -> Modality)
-> (Term -> m Term)
-> 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
  , modalityAction :: Modality -> Modality -> Modality
modalityAction  = \ Modality
_ -> Modality -> Modality
forall a. a -> a
id
  , elimViewAction :: Term -> m Term
elimViewAction  = ProjEliminator -> Term -> m Term
forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone
  }

eraseUnusedAction :: Action TCM
eraseUnusedAction :: Action TCM
eraseUnusedAction = Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction { postAction :: Type -> Term -> TCM Term
postAction = Type -> Term -> TCM Term
eraseUnused }
  where
    eraseUnused :: Type -> Term -> TCM Term
    eraseUnused :: Type -> Term -> TCM Term
eraseUnused Type
t = \case
      Def QName
f Elims
es -> do
        [Polarity]
pols <- QName -> TCMT IO [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
f
        Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
      Term
v        -> Term -> TCM Term
forall (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 :: * -> *). PureTCM 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 ] ]
  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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCM Doc
"checking internal with DB indices"
    , 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t ] ]
  Telescope
ctx <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCM Doc
"In context"
    , 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Telescope -> TCM Doc
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 <- Action m -> Term -> m Term
forall (m :: * -> *). Action m -> Term -> m Term
elimViewAction Action m
action (Term -> m Term) -> m Term -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Action m -> Type -> Term -> m Term
forall (m :: * -> *). Action m -> Type -> Term -> m Term
preAction Action m
action Type
t Term
v
  Action m -> Type -> Term -> m Term
forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction Action m
action Type
t (Term -> m Term) -> m Term -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Term
v of
    Var VerboseLevel
i Elims
es   -> do
      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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> VerboseLevel -> Substitution' Term
forall a. Impossible -> VerboseLevel -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel))
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Elims -> Elims
forall a. VerboseLevel -> [a] -> [a]
take (Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
vs) Elims
vs2
    Lit Literal
l      -> do
      Type
lt <- Literal -> m Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
l
      Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp Type
lt Type
t
      Term -> m Term
forall (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 :: * -> *).
PureTCM 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 a. Subst a => Abs a -> a
absBody Abs Term
vb) Comparison
cmp (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Pi Dom Type
a Abs Type
b     -> do
      Sort
s <- Type -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock 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.
(HasCallStack, MonadTCError 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 :: Term -> Dom Type
mkDom Term
v = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
sa Term
v Type -> Dom Type -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a
          mkRng :: Term -> Abs Type
mkRng Term
v = (Type -> Type) -> Abs Type -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term
v Term -> Type -> Type
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{}   -> (VerboseKey, Dom Type) -> m Term -> m Term
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 Term -> m Term
forall a. a -> a
id
      Dom Type
a <- Term -> Dom Type
mkDom (Term -> Dom Type) -> m Term -> m (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Term -> Comparison -> 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
goInside (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a (Abs Type -> Term) -> (Term -> Abs Type) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Abs Type
mkRng (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Action m -> Term -> Comparison -> 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 :: * -> *). (PureTCM m, MonadBlock 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 :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort Sort
s
      Sort
s'' <- Type -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock 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 :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType 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 :: * -> *). 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.
  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
$ do
    Type
t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM 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.
(HasCallStack, MonadTCError 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 a. Subst 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *).
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 :: Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai ArgInfo
ai' = do
  Hiding -> Hiding -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Hiding -> Hiding -> m ()
checkHiding    (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai)     (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai')
  Modality
mod <- Action m -> Modality -> Modality -> m Modality
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Modality -> Modality -> m Modality
checkModality Action m
action (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
ai)  (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
ai')
  ArgInfo -> m ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
forall a b. (a -> b) -> a -> b
$ Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
ai

checkHiding    :: (MonadCheckInternal m) => Hiding -> Hiding -> m ()
checkHiding :: Hiding -> Hiding -> m ()
checkHiding    Hiding
h Hiding
h' = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Hiding -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h Hiding
h') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Hiding -> Hiding -> TypeError
HidingMismatch Hiding
h Hiding
h'

-- | @checkRelevance action term type@.
--
--   The @term@ 'Relevance' can be updated by the @action@.
checkModality :: (MonadCheckInternal m) => Action m -> Modality -> Modality -> m Modality
checkModality :: Action m -> Modality -> Modality -> m Modality
checkModality Action m
action Modality
mod Modality
mod' = do
  let (Relevance
r,Relevance
r') = (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod, Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod')
      (Quantity
q,Quantity
q') = (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Modality
mod, Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Modality
mod')
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Modality -> Modality -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
mod Modality
mod') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ if
    | Bool -> Bool
not (Relevance -> Relevance -> Bool
sameRelevance Relevance
r Relevance
r') -> Relevance -> Relevance -> TypeError
RelevanceMismatch Relevance
r Relevance
r'
    | Bool -> Bool
not (Quantity -> Quantity -> Bool
sameQuantity Quantity
q Quantity
q')  -> Quantity -> Quantity -> TypeError
QuantityMismatch  Quantity
q Quantity
q'
    | Bool
otherwise -> TypeError
forall a. HasCallStack => a
__IMPOSSIBLE__ -- add more cases when adding new modalities
  Modality -> m Modality
forall (m :: * -> *) a. Monad m => a -> m a
return (Modality -> m Modality) -> Modality -> m Modality
forall a b. (a -> b) -> a -> b
$ Action m -> Modality -> Modality -> Modality
forall (m :: * -> *). Action m -> Modality -> Modality -> Modality
modalityAction Action m
action Modality
mod' Modality
mod  -- Argument order for actions: @type@ @term@

-- | Infer type of a neutral term.
infer :: (MonadCheckInternal m) => Term -> m Type
infer :: 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
  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
  QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f m (Maybe Projection) -> (Maybe Projection -> m Type) -> m Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    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 :: * -> *). 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' :: 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
self'
    , TCM Doc
"eliminated by e = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Elim -> VerboseKey
forall a. Show a => a -> VerboseKey
show 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 -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
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 -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
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 -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
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 -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
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 -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
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 = do
    Type
t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
    m Type -> (Type -> m Type) -> Maybe Type -> m Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Type
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 :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t
  where failure :: m Type
failure = TypeError -> m Type
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m Type) -> TypeError -> m Type
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 = do
  Type
t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  Maybe (Dom Type, Abs Type)
m <- Type -> m (Maybe (Dom Type, Abs Type))
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  -> (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.
(HasCallStack, MonadTCError 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 -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t m Type
-> (Type -> m (Dom Type, Abs Type)) -> m (Dom Type, Abs Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
  El Sort
_ (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)
  Type
_             -> TypeError -> m (Dom Type, Abs Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError 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
    Inf IsFibrant
f Integer
n  -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
    SSet Level
l   -> Level -> Sort
forall t. Level' t -> Sort' t
SSet (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
SizeUniv -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
SizeUniv
    Sort
LockUniv -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
LockUniv
    PiSort Dom' Term Term
dom Sort
s1 Abs Sort
s2 -> do
      let a :: Term
a = Dom' Term Term -> Term
forall t e. Dom' t e -> e
unDom Dom' Term Term
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' Term Term
dom' = Dom' Term Term
dom Dom' Term Term -> Term -> Dom' Term Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
a'
      Abs Sort
s2' <- Dom Type -> (Sort -> m Sort) -> Abs Sort -> m (Abs Sort)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s1' (Term -> Type) -> Dom' Term Term -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term
dom') (Action m -> Sort -> 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' Term Term -> Sort -> Abs Sort -> Sort
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' <- 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 Term
l)      = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
k (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
checkLevelAtom Term
l

    checkLevelAtom :: Term -> m Term
checkLevelAtom Term
l = do
      Type
lvl <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
      Action m -> Term -> Comparison -> Type -> m Term
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 :: 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!
    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 :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp Type
t1 Type
t2