{-# LANGUAGE ScopedTypeVariables #-}
module Agda.TypeChecking.Sort where
import Control.Monad
import Control.Monad.Except
import Data.Functor
import Data.Maybe
import Agda.Interaction.Options (optCumulativity, optRewriting)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import {-# SOURCE #-} Agda.TypeChecking.Constraints ()
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.MetaVars ()
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin (HasBuiltins)
import Agda.TypeChecking.Monad.Constraints (addConstraint, MonadConstraint)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.MetaVars (metaType)
import Agda.TypeChecking.Monad.Pure
import Agda.TypeChecking.Monad.Signature (HasConstInfo(..), applyDef)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records (getDefType)
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.Monad
inferUnivSort
:: (PureTCM m, MonadConstraint m)
=> Sort -> m Sort
inferUnivSort :: forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort Sort
s = do
Sort
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s
case Sort -> Either Blocker Sort
univSort' Sort
s of
Right Sort
s' -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s'
Left Blocker
_ -> do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t
UnivSort Sort
s
sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
sortFitsIn :: forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
sortFitsIn Sort
a Sort
b = do
Sort
b' <- forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort Sort
a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
b' Sort
b)
(forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
b' Sort
b)
hasBiggerSort :: Sort -> TCM ()
hasBiggerSort :: Sort -> TCM ()
hasBiggerSort = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort
inferPiSort :: PureTCM m => Dom Type -> Abs Sort -> m Sort
inferPiSort :: forall (m :: * -> *). PureTCM m => Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
s2 = do
Sort
s1' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Dom Type
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 Dom Type
a forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Abs Sort
s2
Abs Sort
s2' <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Abs Sort
s2'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Sort
piSort (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a) Sort
s1' Abs Sort
s2'
inferFunSort :: Sort -> Sort -> TCM Sort
inferFunSort :: Sort -> Sort -> TCM Sort
inferFunSort Sort
s1 Sort
s2 = Sort -> Sort -> Sort
funSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s2
ptsRule :: Dom Type -> Abs Sort -> Sort -> TCM ()
ptsRule :: Dom Type -> Abs Sort -> Sort -> TCM ()
ptsRule Dom Type
a Abs Sort
b Sort
c = do
Sort
c' <- forall (m :: * -> *). PureTCM m => Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
b
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
c' Sort
c)
(forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
c' Sort
c)
ptsRule' :: Sort -> Sort -> Sort -> TCM ()
ptsRule' :: Sort -> Sort -> Sort -> TCM ()
ptsRule' Sort
a Sort
b Sort
c = do
Sort
c' <- Sort -> Sort -> TCM Sort
inferFunSort Sort
a Sort
b
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
c' Sort
c)
(forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
c' Sort
c)
hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
hasPTSRule Dom Type
a Abs Sort
b = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PureTCM m => Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
b
checkTelePiSort :: Type -> TCM ()
checkTelePiSort :: Type -> TCM ()
checkTelePiSort Type
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a
ifIsSort :: forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
t Sort -> m a
yes m a
no = do
Blocked Type
bt <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
t
case forall t a. Type'' t a -> a
unEl (forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
bt) of
Sort Sort
s -> Sort -> m a
yes Sort
s
Term
_ | Blocked Blocker
m Type
_ <- Blocked Type
bt -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
m
| Bool
otherwise -> m a
no
ifNotSort :: (MonadReduce m, MonadBlock m) => Type -> m a -> (Sort -> m a) -> m a
ifNotSort :: forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> m a -> (Sort -> m a) -> m a
ifNotSort Type
t = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
t
shouldBeSort
:: (PureTCM m, MonadBlock m, MonadError TCErr m)
=> Type -> m Sort
shouldBeSort :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t = forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
t forall (m :: * -> *) a. Monad m => a -> m a
return (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort Type
t)
sortOf
:: forall m. (PureTCM m, MonadBlock m)
=> Term -> m Sort
sortOf :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf Term
t = do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.sort" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sortOf" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
Term -> m Sort
sortOfT forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone Term
t
where
sortOfT :: Term -> m Sort
sortOfT :: Term -> m Sort
sortOfT = \case
Pi Dom Type
adom Abs Type
b -> do
let a :: Term
a = 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
adom
Sort
sa <- forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf Term
a
Abs Sort
sb <- forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
adom (forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl) Abs Type
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Sort
piSort (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
adom) Sort
sa Abs Sort
sb
Sort Sort
s -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Sort
univSort Sort
s
Var Int
i Elims
es -> do
Type
a <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE Type
a (Int -> Elims -> Term
Var Int
i) Elims
es
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
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE 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
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE Type
a (MetaId -> Elims -> Term
MetaV MetaId
x) Elims
es
Lam{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Con{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Lit{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Level{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Dummy VerboseKey
s Elims
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s
sortOfE :: Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE :: Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE Type
a Elims -> Term
hd [] = forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
a forall (m :: * -> *) a. Monad m => a -> m a
return forall a. HasCallStack => a
__IMPOSSIBLE__
sortOfE Type
a Elims -> Term
hd (Elim
e:Elims
es) = do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.sort" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"sortOfE"
, TCMT IO Doc
" a = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, TCMT IO Doc
" hd = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd [])
, TCMT IO Doc
" 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
Apply (Arg ArgInfo
ai Term
v) -> do
Blocked Type
ba <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
a
case forall t a. Type'' t a -> a
unEl (forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
ba) of
Pi Dom Type
b Abs Type
c -> Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c 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
es
Term
_ | Blocked Blocker
m Type
_ <- Blocked Type
ba -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
m
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optRewriting forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock)
forall a. HasCallStack => a
__IMPOSSIBLE__
Proj ProjOrigin
o QName
f -> do
Type
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
~(El Sort
_ (Pi Dom Type
b Abs Type
c)) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
a
Elims -> Term
hd' <- forall t. Apply t => t -> Elims -> t
applyE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (forall t a. Dom' t a -> Arg a
argFromDom Dom Type
b forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd [])
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` (Elims -> Term
hd [])) Elims -> Term
hd' Elims
es
IApply Term
x Term
y Term
r -> do
(Dom Type
b , Abs Type
c) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath Type
a
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c 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
es
sortOfType
:: forall m. (PureTCM m, MonadBlock m)
=> Type -> m Sort
sortOfType :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Sort
sortOfType = forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl