{-# LANGUAGE ScopedTypeVariables #-}

-- | This module contains the rules for Agda's sort system viewed as a pure
--   type system (pts). The specification of a pts consists of a set
--   of axioms of the form @s1 : s2@ specifying when a sort fits in
--   another sort, and a set of rules of the form @(s1,s2,s3)@
--   specifying that a pi type with domain in @s1@ and codomain in
--   @s2@ itself fits into sort @s3@.
--
--   To ensure unique principal types, the axioms and rules of Agda's
--   pts are given by two partial functions @univSort'@ and @piSort'@
--   (see @Agda.TypeChecking.Substitute@). If these functions return
--   @Nothing@, a constraint is added to ensure that the sort will be
--   computed eventually.
--
--   One 'upgrade' over the standard definition of a pts is that in a
--   rule @(s1,s2,s3)@, in Agda the sort @s2@ can depend on a variable
--   of some type in @s1@. This is needed to support Agda's universe
--   polymorphism where we can have e.g. a function of type @∀ {ℓ} →
--   Set ℓ@.

module Agda.TypeChecking.Sort where

import Control.Monad

import Data.Functor
import Data.Maybe

import Agda.Interaction.Options (optCumulativity)

import Agda.Syntax.Common
import Agda.Syntax.Internal

import {-# SOURCE #-} Agda.TypeChecking.Constraints () -- instance only
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.MetaVars () -- instance only

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.Signature (HasConstInfo(..), applyDef)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.ProjectionLike (elimView)
import Agda.TypeChecking.Records (getDefType)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Except
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.Monad

-- | Infer the sort of another sort. If we can compute the bigger sort
--   straight away, return that. Otherwise, return @UnivSort s@ and add a
--   constraint to ensure we can compute the sort eventually.
inferUnivSort
  :: (MonadReduce m, MonadConstraint m, HasOptions 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
  Maybe Sort
ui <- m (Maybe Sort)
forall (m :: * -> *). HasOptions m => m (Maybe Sort)
univInf
  case Maybe Sort -> Sort -> Maybe Sort
univSort' Maybe Sort
ui Sort
s of
    Just Sort
s' -> Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s'
    Maybe Sort
Nothing -> do
      Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Sort -> Constraint
HasBiggerSort 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
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 :: * -> *).
(MonadReduce m, MonadConstraint m, HasOptions 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 :: * -> *).
(MonadReduce m, MonadConstraint m, HasOptions m) =>
Sort -> m Sort
inferUnivSort

-- | Infer the sort of a pi type. If we can compute the sort straight away,
--   return that. Otherwise, return @PiSort a s2@ and add a constraint to
--   ensure we can compute the sort eventually.
inferPiSort
  :: (MonadReduce m, MonadAddContext m, MonadDebug 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
  let a' :: Dom Type
a' = Lens' Sort (Dom Type) -> LensSet Sort (Dom Type)
forall i o. Lens' i o -> LensSet i o
set forall a. LensSort a => Lens' Sort a
Lens' Sort (Dom Type)
lensSort Sort
s1' Dom Type
a
  Abs Sort
s2' <- Dom Type -> (Sort -> m Sort) -> Abs Sort -> m (Abs Sort)
forall t a t' b (m :: * -> *).
(Subst t a, Subst t' b, Free 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
  -- we do instantiateFull here to perhaps remove some (flexible)
  -- dependencies of s2 on var 0, thus allowing piSort' to reduce
  Abs Sort
s2' <- Abs Sort -> m (Abs Sort)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Abs Sort
s2'

  --Jesper, 2018-04-23: disabled PTS constraints for now,
  --this assumes that piSort can only be blocked by unsolved metas.

  --case piSort' s1 s2 of
  --  Just s -> return s
  --  Nothing -> do
  --    addConstraint $ HasPTSRule s1 s2
  --    return $ PiSort s1 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 Type -> Abs Sort -> Sort
piSort Dom Type
a' Abs Sort
s2'

-- | As @inferPiSort@, but for a nondependent function type.
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 :: * -> *).
(MonadReduce m, MonadAddContext m, MonadDebug 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)

-- | Non-dependent version of ptsRule
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 :: * -> *).
(MonadReduce m, MonadAddContext m, MonadDebug m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort Dom Type
a Abs Sort
b

-- | Recursively check that an iterated function type constructed by @telePi@
--   is well-sorted.
checkTelePiSort :: Type -> TCM ()
-- Jesper, 2019-07-27: This is currently doing nothing (see comment in inferPiSort)
--checkTelePiSort (El s (Pi a b)) = do
--  -- Since the function type is assumed to be constructed by @telePi@,
--  -- we already know that @s == piSort (getSort a) (getSort <$> b)@,
--  -- so we just check that this sort is well-formed.
--  hasPTSRule a (getSort <$> b)
--  underAbstraction a b checkTelePiSort
checkTelePiSort :: Type -> TCM ()
checkTelePiSort Type
_ = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

ifIsSort :: (MonadReduce 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
  Type
t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Sort Sort
s -> Sort -> m a
yes Sort
s
    Term
_      -> m a
no

-- | Result is in reduced form.
shouldBeSort
  :: (MonadReduce m, MonadTCEnv m, ReadTCState 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 =>
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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m Sort) -> TypeError -> m Sort
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort Type
t)

-- | Reconstruct the sort of a type.
--
--   Precondition: given term is a well-sorted type.
sortOf
  :: forall m. (MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m, HasConstInfo 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
=<< Bool -> Term -> m Term
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasConstInfo m) =>
Bool -> Term -> m Term
elimView Bool
True 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 :: * -> *).
(MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m) =>
Term -> m Sort
sortOf Term
a
        Abs Sort
sb <- Dom Type -> (Type -> m Sort) -> Abs Type -> m (Abs Sort)
forall t a t' b (m :: * -> *).
(Subst t a, Subst t' b, Free b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
adom (Term -> m Sort
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m,
 HasConstInfo 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 Type -> Abs Sort -> Sort
piSort (Dom Type
adom Dom Type -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
sa Term
a) Abs Sort
sb
      Sort Sort
s     -> do
        Maybe Sort
ui <- m (Maybe Sort)
forall (m :: * -> *). HasOptions m => m (Maybe Sort)
univInf
        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
$ Maybe Sort -> Sort -> Sort
univSort Maybe Sort
ui 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 =>
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) = case Elim
e of
      Apply (Arg ArgInfo
ai Term
v) -> Type
-> (Type -> m Sort) -> (Dom Type -> Abs Type -> m Sort) -> m Sort
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
a Type -> m Sort
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Dom Type -> Abs Type -> m Sort) -> m Sort)
-> (Dom Type -> Abs Type -> m Sort) -> m Sort
forall a b. (a -> b) -> a -> b
$ \Dom Type
b Abs Type
c -> do
        Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
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
      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 :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug 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 -> Term -> Type
forall t a. Subst t a => Abs a -> t -> 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 :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath Type
a
        Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE (Abs Type
c Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
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