{-# OPTIONS_GHC -Wunused-imports #-}
{-# 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.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.Monad
import Agda.Utils.Impossible
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, MonadConstraint m)
=> Dom Type
-> Abs Sort
-> m Sort
inferPiSort :: forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
s = do
Blocked Sort
s1' <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Dom Type
a
Abs (Blocked 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 (Blocked a)
reduceB Abs Sort
s
let s1 :: Sort
s1 = forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s1'
let s2 :: Abs Sort
s2 = forall t a. Blocked' t a -> a
ignoreBlocking forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Blocked Sort)
s2'
case Dom Term -> Sort -> Abs Sort -> Either Blocker 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 of
Right Sort
s -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
Left Blocker
b -> do
let b' :: Blocker
b' = Blocker -> Blocker -> Blocker
unblockOnEither (forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s1') (forall t a. Blocked' t a -> Blocker
getBlocker forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs (Blocked Sort)
s2')
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (Blocker -> Blocker -> Blocker
unblockOnEither Blocker
b Blocker
b') forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Constraint
HasPTSRule Dom Type
a 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 (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 :: (PureTCM m, MonadConstraint m)
=> Dom Type
-> Sort
-> m Sort
inferFunSort :: forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Sort -> m Sort
inferFunSort Dom Type
a Sort
s = do
Blocked Sort
s1' <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Dom Type
a
Blocked Sort
s2' <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort
s
let s1 :: Sort
s1 = forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s1'
let s2 :: Sort
s2 = forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s2'
case Sort -> Sort -> Either Blocker Sort
funSort' Sort
s1 Sort
s2 of
Right Sort
s -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
Left Blocker
b -> do
let b' :: Blocker
b' = Blocker -> Blocker -> Blocker
unblockOnEither (forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s1') (forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s2')
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (Blocker -> Blocker -> Blocker
unblockOnEither Blocker
b Blocker
b') forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Constraint
HasPTSRule Dom Type
a (forall a. ArgName -> a -> Abs a
NoAbs ArgName
"_" 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
hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
hasPTSRule Dom Type
a Abs Sort
s = do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.conv.sort" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"hasPTSRule"
, 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 Dom Type
a
, TCMT IO Doc
"s =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Abs a -> a
unAbs Abs Sort
s)
]
if forall {t}. Sort' t -> Bool
alwaysValidCodomain forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Sort
s
then TCM ()
yes
else do
Blocked Sort
sb <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
s
case Blocked Sort
sb of
Blocked Blocker
b Sort
t | Blocker
neverUnblock forall a. Eq a => a -> a -> Bool
== Blocker
b -> forall {m :: * -> *} {a} {b}.
(MonadDebug m, PrettyTCM a, MonadTCEnv m, ReadTCState m,
MonadError TCErr m) =>
a -> Sort -> m b
no Blocked Sort
sb Sort
t
NotBlocked NotBlocked' Term
_ t :: Sort
t@FunSort{} -> forall {m :: * -> *} {a} {b}.
(MonadDebug m, PrettyTCM a, MonadTCEnv m, ReadTCState m,
MonadError TCErr m) =>
a -> Sort -> m b
no Blocked Sort
sb Sort
t
NotBlocked NotBlocked' Term
_ t :: Sort
t@PiSort{} -> forall {m :: * -> *} {a} {b}.
(MonadDebug m, PrettyTCM a, MonadTCEnv m, ReadTCState m,
MonadError TCErr m) =>
a -> Sort -> m b
no Blocked Sort
sb Sort
t
Blocked Sort
_ -> TCM ()
yes
where
alwaysValidCodomain :: Sort' t -> Bool
alwaysValidCodomain = \case
Inf{} -> Bool
True
Univ{} -> Bool
True
FunSort Sort' t
_ Sort' t
s -> Sort' t -> Bool
alwaysValidCodomain Sort' t
s
PiSort Dom' t t
_ Sort' t
_ Abs (Sort' t)
s -> Sort' t -> Bool
alwaysValidCodomain forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs (Sort' t)
s
Sort' t
_ -> Bool
False
yes :: TCM ()
yes = do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"tc.conv.sort" VerboseLevel
35 ArgName
"hasPTSRule succeeded"
no :: a -> Sort -> m b
no a
sb Sort
t = do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.conv.sort" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"hasPTSRule fails on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
sb
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Sort -> TypeError
InvalidTypeSort Sort
t
checkTelePiSort :: Type -> TCM ()
checkTelePiSort :: Type -> TCM ()
checkTelePiSort (El Sort
s (Pi Dom Type
a Abs Type
b)) = do
Dom Type -> Abs Sort -> TCM ()
hasPTSRule Dom Type
a (forall a. LensSort a => a -> Sort
getSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b Type -> TCM ()
checkTelePiSort
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,MonadConstraint m)
=> Term -> m Sort
sortOf :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
t = do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.sort" VerboseLevel
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, MonadConstraint 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, MonadConstraint 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 :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort (Dom Type
adom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall t a. Sort' t -> a -> Type'' t a
El Sort
sa Term
a) 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 VerboseLevel
i Elims
es -> do
Type
a <- 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 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 ArgName
s Elims
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
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 =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.sort" VerboseLevel
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
]
Blocked Type
ba <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
a
let
a' :: Type
a' = forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
ba
fallback :: m Sort
fallback = case Blocked Type
ba of
Blocked Blocker
m Type
_ -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
m
Blocked Type
_ -> 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__
case Elim
e of
Apply (Arg ArgInfo
ai Term
v) -> case forall t a. Type'' t a -> a
unEl Type
a' 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
_ -> m Sort
fallback
Proj ProjOrigin
o QName
f -> case forall t a. Type'' t a -> a
unEl Type
a' of
Def{} -> do
~(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
Term
_ -> m Sort
fallback
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,MonadConstraint m)
=> Type -> m Sort
sortOfType :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Type -> m Sort
sortOfType = forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl