{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.CheckInternal
( MonadCheckInternal
, checkType, infer, inferSpine
, CheckInternal(..)
, Action(..), defaultAction, eraseUnusedAction
) where
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.ProjectionLike (elimView, ProjEliminator(..))
import Agda.TypeChecking.Records (shouldBeProjectible)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Telescope
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor (($>))
import Agda.Utils.Maybe
import Agda.Utils.Size
import Agda.Utils.Impossible
import Agda.Interaction.Options
type MonadCheckInternal m = MonadConversion m
{-# SPECIALIZE checkType :: Type -> TCM () #-}
checkType :: (MonadCheckInternal m) => Type -> m ()
checkType :: forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
t = forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Type -> Constraint
CheckType Type
t) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
a -> m ()
inferInternal Type
t
data Action m = Action
{ forall (m :: * -> *). Action m -> Type -> Term -> m Term
preAction :: Type -> Term -> m Term
, forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction :: Type -> Term -> m Term
, forall (m :: * -> *). Action m -> Modality -> Modality -> Modality
modalityAction :: Modality -> Modality -> Modality
, forall (m :: * -> *). Action m -> Term -> m Term
elimViewAction :: Term -> m Term
}
defaultAction :: PureTCM m => Action m
defaultAction :: forall (m :: * -> *). PureTCM m => Action m
defaultAction = Action
{ preAction :: Type -> Term -> m Term
preAction = \ Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return
, postAction :: Type -> Term -> m Term
postAction = \ Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return
, modalityAction :: Modality -> Modality -> Modality
modalityAction = \ Modality
_ -> forall a. a -> a
id
, elimViewAction :: Term -> m Term
elimViewAction = forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone
}
eraseUnusedAction :: Action TCM
eraseUnusedAction :: Action TCM
eraseUnusedAction = forall (m :: * -> *). PureTCM m => Action m
defaultAction { postAction :: Type -> Term -> TCMT IO Term
postAction = Type -> Term -> TCMT IO Term
eraseUnused }
where
eraseUnused :: Type -> Term -> TCM Term
eraseUnused :: Type -> Term -> TCMT IO Term
eraseUnused Type
t = \case
Def QName
f Elims
es -> do
[Polarity]
pols <- forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
f
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f forall a b. (a -> b) -> a -> b
$ [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
eraseIfNonvariant :: [Polarity] -> Elims -> Elims
eraseIfNonvariant :: [Polarity] -> Elims -> Elims
eraseIfNonvariant [] Elims
es = Elims
es
eraseIfNonvariant [Polarity]
pols [] = []
eraseIfNonvariant (Polarity
Nonvariant : [Polarity]
pols) (Elim
e : Elims
es) = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare Elim
e) forall a. a -> [a] -> [a]
: [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
eraseIfNonvariant (Polarity
_ : [Polarity]
pols) (Elim
e : Elims
es) = Elim
e forall a. a -> [a] -> [a]
: [Polarity] -> Elims -> Elims
eraseIfNonvariant [Polarity]
pols Elims
es
class CheckInternal a where
checkInternal' :: (MonadCheckInternal m) => Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal :: (MonadCheckInternal m) => a -> Comparison -> TypeOf a -> m ()
checkInternal a
v Comparison
cmp TypeOf a
t = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' forall (m :: * -> *). PureTCM m => Action m
defaultAction a
v Comparison
cmp TypeOf a
t
inferInternal' :: (MonadCheckInternal m, TypeOf a ~ ()) => Action m -> a -> m a
inferInternal' Action m
act a
v = forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
act a
v Comparison
CmpEq ()
inferInternal :: (MonadCheckInternal m, TypeOf a ~ ()) => a -> m ()
inferInternal a
v = forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
a -> Comparison -> TypeOf a -> m ()
checkInternal a
v Comparison
CmpEq ()
{-# SPECIALIZE checkInternal' :: Action TCM -> Term -> Comparison -> TypeOf Term -> TCM Term #-}
{-# SPECIALIZE checkInternal' :: Action TCM -> Type -> Comparison -> TypeOf Type -> TCM Type #-}
{-# SPECIALIZE checkInternal' :: Action TCM -> Elims -> Comparison -> TypeOf Type -> TCM Elims #-}
{-# SPECIALIZE checkInternal :: Term -> Comparison -> TypeOf Term -> TCM () #-}
{-# SPECIALIZE checkInternal :: Type -> Comparison -> TypeOf Type -> TCM () #-}
instance CheckInternal Type where
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Comparison -> TypeOf Type -> m Type
checkInternal' Action m
action (El Sort
s Term
t) Comparison
cmp TypeOf Type
_ = do
Term
t' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
t Comparison
cmp (Sort -> Type
sort Sort
s)
Sort
s' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
t'
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t a. Sort' t -> a -> Type'' t a
El Sort
s Term
t')
instance CheckInternal Term where
checkInternal' :: (MonadCheckInternal m) => Action m -> Term -> Comparison -> Type -> m Term
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action m
action Term
v Comparison
cmp Type
t = forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.check.internal" Int
20 String
"" forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"checking internal "
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"checking internal with DB indices"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t ] ]
Telescope
ctx <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Telescope
ctx) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"In context"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ctx ] ]
Term
v <- forall (m :: * -> *). Action m -> Term -> m Term
elimViewAction Action m
action forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). Action m -> Type -> Term -> m Term
preAction Action m
action Type
t Term
v
forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction Action m
action Type
t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Term
v of
Var Int
i Elims
es -> do
Dom Type
d <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i
Name
n <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
i
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Bool
usableCohesion Dom Type
d) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Name -> Cohesion -> TypeError
VariableIsOfUnusableCohesion Name
n (forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
d)
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"variable" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i) , TCMT IO Doc
"has type" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t e. Dom' t e -> e
unDom Dom Type
d)
, TCMT IO Doc
"and modality", forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. LensModality a => a -> Modality
getModality Dom Type
d) ]
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action (forall t e. Dom' t e -> e
unDom Dom Type
d) (Int -> Elims -> Term
Var Int
i) Elims
es Comparison
cmp Type
t
Def QName
f Elims
es -> do
Type
a <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (QName -> Elims -> Term
Def QName
f) Elims
es Comparison
cmp Type
t
MetaV MetaId
x Elims
es -> do
Type
a <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"metavariable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (MetaId -> Elims -> Term
MetaV MetaId
x) Elims
es Comparison
cmp Type
t
Con ConHead
c ConInfo
ci Elims
vs -> do
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m, MonadTCError m) =>
ConHead
-> Elims
-> Type
-> (QName
-> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
-> m a
fullyApplyCon ConHead
c Elims
vs Type
t forall a b. (a -> b) -> a -> b
$ \ QName
_d Type
_dt Args
_pars Type
a Elims
vs' Telescope
tel Type
t -> do
Con ConHead
c ConInfo
ci Elims
vs2 <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
vs' Comparison
cmp Type
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Impossible -> Int -> Substitution' a
strengthenS HasCallStack => Impossible
impossible (forall a. Sized a => a -> Int
size Telescope
tel))
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
vs) Elims
vs2
Lit Literal
l -> do
Type
lt <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
l
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp Type
lt Type
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
Lam ArgInfo
ai Abs Term
vb -> do
(Dom Type
a, Abs Type
b) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePiOrPath Type
t
ArgInfo
ai <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
let name :: String
name = [Suggestion] -> String
suggests [ forall a. Suggest a => a -> Suggestion
Suggestion Abs Term
vb , forall a. Suggest a => a -> Suggestion
Suggestion Abs Type
b ]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
name, Dom Type
a) forall a b. (a -> b) -> a -> b
$ do
ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Term
vb) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action (forall a. Subst a => Abs a -> a
absBody Abs Term
vb) Comparison
cmp (forall a. Subst a => Abs a -> a
absBody Abs Type
b)
Pi Dom Type
a Abs Type
b -> do
Sort
s <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"pi type should have sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort
s forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Term -> TypeError
FunctionTypeInSizeUniv Term
v
Bool
experimental <- PragmaOptions -> Bool
optExperimentalIrrelevance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
let sa :: Sort
sa = forall a. LensSort a => a -> Sort
getSort Dom Type
a
sb :: Sort
sb = forall a. LensSort a => a -> Sort
getSort (forall a. Abs a -> a
unAbs Abs Type
b)
mkDom :: Term -> Dom Type
mkDom Term
v = forall t a. Sort' t -> a -> Type'' t a
El Sort
sa Term
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a
mkRng :: Term -> Abs Type
mkRng Term
v = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Abs Type
b
goInside :: m Term -> m Term
goInside = case Abs Type
b of
Abs{} -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext forall a b. (a -> b) -> a -> b
$ (forall a. Abs a -> String
absName Abs Type
b,) forall a b. (a -> b) -> a -> b
$
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
experimental (forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict) Dom Type
a
NoAbs{} -> forall a. a -> a
id
Dom Type
a <- Term -> Dom Type
mkDom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a) Comparison
CmpLeq (Sort -> Type
sort Sort
sa)
Term
v' <- m Term -> m Term
goInside forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Abs Type
mkRng forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Type
b) Comparison
CmpLeq (Sort -> Type
sort Sort
sb)
Sort
s' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
v
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v'
Sort Sort
s -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s
Sort
s <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Sort
s
Sort
s' <- forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort Sort
s
Sort
s'' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s''
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
s
Level Level
l -> do
Level
l <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Level
l
Type
lt <- forall (m :: * -> *). HasBuiltins m => m Type
levelType'
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp Type
lt Type
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
l
DontCare Term
v -> Term -> Term
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
v Comparison
cmp Type
t
Dummy String
s Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
checkArgInfo :: (MonadCheckInternal m) => Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai ArgInfo
ai' = do
forall (m :: * -> *).
MonadCheckInternal m =>
Hiding -> Hiding -> m ()
checkHiding (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai) (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai')
Modality
mod <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Modality -> Modality -> m Modality
checkModality Action m
action (forall a. LensModality a => a -> Modality
getModality ArgInfo
ai) (forall a. LensModality a => a -> Modality
getModality ArgInfo
ai')
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
ai
checkHiding :: (MonadCheckInternal m) => Hiding -> Hiding -> m ()
checkHiding :: forall (m :: * -> *).
MonadCheckInternal m =>
Hiding -> Hiding -> m ()
checkHiding Hiding
h Hiding
h' = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h Hiding
h') forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Hiding -> Hiding -> TypeError
HidingMismatch Hiding
h Hiding
h'
checkModality :: (MonadCheckInternal m) => Action m -> Modality -> Modality -> m Modality
checkModality :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Modality -> Modality -> m Modality
checkModality Action m
action Modality
mod Modality
mod' = do
let (Relevance
r,Relevance
r') = (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod, forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod')
(Quantity
q,Quantity
q') = (forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod, forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod')
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
mod Modality
mod') forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ if
| Bool -> Bool
not (Relevance -> Relevance -> Bool
sameRelevance Relevance
r Relevance
r') -> Relevance -> Relevance -> TypeError
RelevanceMismatch Relevance
r Relevance
r'
| Bool -> Bool
not (Quantity -> Quantity -> Bool
sameQuantity Quantity
q Quantity
q') -> Quantity -> Quantity -> TypeError
QuantityMismatch Quantity
q Quantity
q'
| Bool
otherwise -> forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Action m -> Modality -> Modality -> Modality
modalityAction Action m
action Modality
mod' Modality
mod
{-# SPECIALIZE infer :: Term -> TCM Type #-}
infer :: (MonadCheckInternal m) => Term -> m Type
infer :: forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer Term
u = do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"CheckInternal.infer" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
case Term
u of
Var Int
i Elims
es -> do
Type
a <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
a (Int -> Elims -> Term
Var Int
i) Elims
es
Def QName
f Elims
es -> do
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) forall a b. (a -> b) -> a -> b
$ \Projection
_ -> forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
Type
a <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
a (QName -> Elims -> Term
Def QName
f) Elims
es
MetaV MetaId
x Elims
es -> do
Type
a <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
a (MetaId -> Elims -> Term
MetaV MetaId
x) Elims
es
Term
_ -> forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
where
nonInferable :: MonadDebug m => m a
nonInferable :: forall (m :: * -> *) a. MonadDebug m => m a
nonInferable = forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"CheckInternal.infer: non-inferable term:"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Term
u
]
instance CheckInternal Elims where
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims
checkInternal' Action m
action Elims
es Comparison
cmp (Type
t , Elims -> Term
hd) = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
t Elims -> Term
hd Elims
es
{-# SPECIALIZE inferSpine :: Action TCM -> Type -> (Elims -> Term) -> Elims -> TCM (Type, Elims) #-}
inferSpine :: (MonadCheckInternal m) => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
t Elims -> Term
hd Elims
es = Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t Elims -> Term
hd forall a. a -> a
id Elims
es
where
loop :: Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t Elims -> Term
hd Elims -> Elims
acc = \case
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t , Elims -> Elims
acc [])
(Elim
e : Elims
es) -> do
let self :: Term
self = Elims -> Term
hd []
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"inferring spine: "
, TCMT IO Doc
"type t = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, TCMT IO Doc
"self = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self
, TCMT IO Doc
"eliminated by e = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
e
]
case Elim
e of
IApply Term
x Term
y Term
r -> do
(Dom Type
a, Abs Type
b) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePath Type
t
Term
r' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
r Comparison
CmpLeq (forall t e. Dom' t e -> e
unDom Dom Type
a)
Term
izero <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
Term
ione <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
Term
x' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
x Comparison
CmpLeq (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
izero)
Term
y' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
y Comparison
CmpLeq (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
ione)
let e' :: Elim
e' = forall a. a -> a -> a -> Elim' a
IApply Term
x' Term
y' Term
r'
Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
r) (Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
e'forall a. a -> [a] -> [a]
:)) Elims
es
Apply (Arg ArgInfo
ai Term
v) -> do
(Dom Type
a, Abs Type
b) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePi Type
t
ArgInfo
ai <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> ArgInfo -> ArgInfo -> m ArgInfo
checkArgInfo Action m
action ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
Term
v' <- forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext (forall a. LensModality a => a -> Modality
getModality Dom Type
a) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
v Comparison
CmpLeq forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a
let e' :: Elim
e' = forall a. Arg a -> Elim' a
Apply (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v')
Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
v) (Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
e'forall a. a -> [a] -> [a]
:)) Elims
es
Proj ProjOrigin
o QName
f -> do
Type
t' <- forall (m :: * -> *).
(PureTCM m, MonadTCError m, MonadBlock m) =>
Term -> Type -> ProjOrigin -> QName -> m Type
shouldBeProjectible Term
self Type
t ProjOrigin
o QName
f
Type
-> (Elims -> Term) -> (Elims -> Elims) -> Elims -> m (Type, Elims)
loop Type
t' (Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) (Elims -> Elims
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eforall a. a -> [a] -> [a]
:)) Elims
es
{-# SPECIALIZE checkSpine :: Action TCM -> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> TCM Term #-}
checkSpine
:: (MonadCheckInternal m)
=> Action m
-> Type
-> (Elims -> Term)
-> Elims
-> Comparison
-> Type
-> m Term
checkSpine :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> (Elims -> Term) -> Elims -> Comparison -> Type -> m Term
checkSpine Action m
action Type
a Elims -> Term
hd Elims
es Comparison
cmp Type
t = do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.check.internal" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"checking spine "
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ])
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] ]
(Type
t' , Elims
es') <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
inferSpine Action m
action Type
a Elims -> Term
hd Elims
es
forall (m :: * -> *).
MonadConversion m =>
(Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
coerceSize (forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp) (Elims -> Term
hd Elims
es) Type
t' Type
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd Elims
es'
instance CheckInternal Sort where
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort
checkInternal' Action m
action Sort
s Comparison
cmp TypeOf Sort
_ = case Sort
s of
Univ Univ
u Level
l -> forall t. Univ -> Level' t -> Sort' t
Univ Univ
u forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Level
l
Inf Univ
u Integer
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
Sort
SizeUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
SizeUniv
Sort
LockUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
LockUniv
Sort
LevelUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
LevelUniv
Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. Sort' t
IntervalUniv
PiSort Dom' Term Term
dom Sort
s1 Abs Sort
s2 -> do
let a :: Term
a = forall t e. Dom' t e -> e
unDom Dom' Term Term
dom
Sort
s1' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Sort
s1
Term
a' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
a Comparison
CmpLeq forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
s1'
let dom' :: Dom' Term Term
dom' = Dom' Term Term
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
a'
Abs Sort
s2' <- forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction (forall t a. Sort' t -> a -> Type'' t a
El Sort
s1' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term
dom') (forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action) Abs Sort
s2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
dom' Sort
s1' Abs Sort
s2'
FunSort Sort
s1 Sort
s2 -> do
Sort
s1' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Sort
s1
Sort
s2' <- forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Sort
s2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1' Sort
s2'
UnivSort Sort
s -> forall t. Sort' t -> Sort' t
UnivSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action Sort
s
MetaS MetaId
x Elims
es -> do
Type
a <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Elims
es Comparison
cmp (Type
a , Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x)
DefS QName
d Elims
es -> do
Type
a <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Elims
es Comparison
cmp (Type
a , Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d)
DummyS String
s -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s
instance CheckInternal Level where
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Level -> Comparison -> TypeOf Level -> m Level
checkInternal' Action m
action (Max Integer
n [PlusLevel]
ls) Comparison
_ TypeOf Level
_ = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m, TypeOf a ~ ()) =>
Action m -> a -> m a
inferInternal' Action m
action) [PlusLevel]
ls
instance CheckInternal PlusLevel where
checkInternal' :: forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel
checkInternal' Action m
action (Plus Integer
k Term
l) Comparison
_ TypeOf PlusLevel
_ = forall t. Integer -> t -> PlusLevel' t
Plus Integer
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
checkLevelAtom Term
l
where
checkLevelAtom :: Term -> m Term
checkLevelAtom Term
l = do
Type
lvl <- forall (m :: * -> *). HasBuiltins m => m Type
levelType'
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' Action m
action Term
l Comparison
CmpLeq Type
lvl