{-# 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 :: Sort -> m Sort
inferUnivSort Sort
s = do
Sort
s <- Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s
case Sort -> Maybe Sort
univSort' Sort
s of
Just Sort
s' -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s'
Maybe Sort
Nothing -> do
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
forall t. Sort' t -> Sort' t
UnivSort Sort
s
sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
sortFitsIn :: Sort -> Sort -> m ()
sortFitsIn Sort
a Sort
b = do
Sort
b' <- Sort -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort Sort
a
m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
b' Sort
b)
(Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
b' Sort
b)
hasBiggerSort :: Sort -> TCM ()
hasBiggerSort :: Sort -> TCM ()
hasBiggerSort = TCMT IO Sort -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCMT IO Sort -> TCM ())
-> (Sort -> TCMT IO Sort) -> Sort -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> TCMT IO Sort
forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Sort -> m Sort
inferUnivSort
inferPiSort :: PureTCM m => Dom Type -> Abs Sort -> m Sort
inferPiSort :: Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
s2 = do
Sort
s1' <- Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
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 Dom Type
a Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Abs Sort
s2
Abs Sort
s2' <- Abs Sort -> m (Abs Sort)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull 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 -> Sort -> Abs Sort -> Sort
piSort (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Dom Type -> Dom Term
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 -> TCMT IO Sort
inferFunSort Sort
s1 Sort
s2 = Sort -> Sort -> Sort
funSort (Sort -> Sort -> Sort) -> TCMT IO Sort -> TCMT IO (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s1 TCMT IO (Sort -> Sort) -> TCMT IO Sort -> TCMT IO Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> TCMT IO Sort
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' <- Dom Type -> Abs Sort -> TCMT IO Sort
forall (m :: * -> *). PureTCM m => Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
b
TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
c' Sort
c)
(Sort -> Sort -> TCM ()
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 -> TCMT IO Sort
inferFunSort Sort
a Sort
b
TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
c' Sort
c)
(Sort -> Sort -> TCM ()
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 = TCMT IO Sort -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCMT IO Sort -> TCM ()) -> TCMT IO Sort -> TCM ()
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> TCMT IO Sort
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
_ = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a
ifIsSort :: Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
t Sort -> m a
yes m a
no = do
Blocked Type
bt <- Type -> m (Blocked Type)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
t
case Type -> Term
forall t a. Type'' t a -> a
unEl (Blocked Type -> Type
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 -> Blocker -> m a
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 :: Type -> m a -> (Sort -> m a) -> m a
ifNotSort Type
t = ((Sort -> m a) -> m a -> m a) -> m a -> (Sort -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Sort -> m a) -> m a -> m a) -> m a -> (Sort -> m a) -> m a)
-> ((Sort -> m a) -> m a -> m a) -> m a -> (Sort -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ Type -> (Sort -> m a) -> m a -> m a
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 :: Type -> m Sort
shouldBeSort Type
t = Type -> (Sort -> m Sort) -> m Sort -> m Sort
forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
t Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (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
$ Type -> TypeError
ShouldBeASort Type
t)
sortOf
:: forall m. (PureTCM m, MonadBlock m)
=> Term -> m Sort
sortOf :: Term -> m Sort
sortOf Term
t = do
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sort" VerboseLevel
40 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"sortOf" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
Term -> m Sort
sortOfT (Term -> m Sort) -> m Term -> m Sort
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProjEliminator -> Term -> m Term
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 = 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
adom
Sort
sa <- Term -> m Sort
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf Term
a
Abs Sort
sb <- Dom Type -> (Type -> m Sort) -> Abs Type -> m (Abs Sort)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
adom (Term -> m Sort
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf (Term -> m Sort) -> (Type -> Term) -> Type -> m Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl) Abs Type
b
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 -> Sort -> Abs Sort -> Sort
piSort (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Dom Type -> Dom Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
adom) Sort
sa Abs Sort
sb
Sort Sort
s -> 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
univSort 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 -> (Elims -> Term) -> Elims -> m Sort
sortOfE Type
a (VerboseLevel -> Elims -> Term
Var VerboseLevel
i) Elims
es
Def 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
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 <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail 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{} -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
Con{} -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
Lit{} -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
Level{} -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
DontCare{} -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
Dummy VerboseKey
s Elims
_ -> VerboseKey -> m Sort
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s
sortOfE :: Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE :: Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE Type
a Elims -> Term
hd [] = Type -> (Sort -> m Sort) -> m Sort -> m Sort
forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
a Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
sortOfE Type
a Elims -> Term
hd (Elim
e:Elims
es) = do
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sort" VerboseLevel
50 (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
vcat
[ TCM Doc
"sortOfE"
, TCM Doc
" a = " 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
, TCM Doc
" hd = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd [])
, TCM Doc
" e = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
e
]
case Elim
e of
Apply (Arg ArgInfo
ai Term
v) -> do
Blocked Type
ba <- Type -> m (Blocked Type)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
a
case Type -> Term
forall t a. Type'' t a -> a
unEl (Blocked Type -> Type
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 Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v) (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
Term
_ | Blocked Blocker
m Type
_ <- Blocked Type
ba -> Blocker -> m Sort
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
m
| Bool
otherwise -> m Bool -> m Sort -> m Sort -> m Sort
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optRewriting (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(Blocker -> m Sort
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock)
m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
Proj ProjOrigin
o QName
f -> do
Type
a <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
~(El Sort
_ (Pi Dom Type
b Abs Type
c)) <- Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Type -> Type) -> m (Maybe Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Type -> m (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
a
Elims -> Term
hd' <- Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Term -> Elims -> Term) -> m Term -> m (Elims -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
b Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd [])
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c Abs Type -> SubstArg Type -> Type
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) <- (Dom Type, Abs Type)
-> Maybe (Dom Type, Abs Type) -> (Dom Type, Abs Type)
forall a. a -> Maybe a -> a
fromMaybe (Dom Type, Abs Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Dom Type, Abs Type) -> (Dom Type, Abs Type))
-> m (Maybe (Dom Type, Abs Type)) -> m (Dom Type, Abs Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Maybe (Dom Type, Abs Type))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath Type
a
Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
r) (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
sortOfType
:: forall m. (PureTCM m, MonadBlock m)
=> Type -> m Sort
sortOfType :: Type -> m Sort
sortOfType = Term -> m Sort
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf (Term -> m Sort) -> (Type -> Term) -> Type -> m Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl