    {-# 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 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 () -- 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.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

    -- | 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
      :: (PureTCM m, MonadConstraint m)
      => Sort -> m Sort
    inferUnivSort :: forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    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
          -- Jesper, 2020-04-19: With the addition of Setωᵢ and the PTS
          -- rule SizeUniv : Setω, every sort (with no metas) now has a
          -- bigger sort, so we do not need to add a constraint.
          -- addConstraint $ HasBiggerSort 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 :: forall (m :: * -> *). MonadConversion m => 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

    -- | 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 :: 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' <- 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
      -- 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 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'

    -- | 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 :: * -> *). 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)

    -- | 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 :: * -> *). PureTCM 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, 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
      -- Jesper, 2020-09-06, subtle: do not use @abortIfBlocked@ here
      -- since we want to take the yes branch whenever the type is a sort,
      -- even if it is blocked.
      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 :: forall (m :: * -> *) a.
    (MonadReduce m, MonadBlock m) =>
    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

    -- | Result is in reduced form.
    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 = 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)

    -- | Reconstruct the sort of a term.
    --
    --   Precondition: given term is a well-sorted type.
    sortOf
      :: forall m. (PureTCM m, MonadBlock m)
      => Term -> m Sort
    sortOf :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
    sortOf Term
    t = do
      VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.sort" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "sortOf" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO 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 Int
    i Elims
    es   -> do
            Type
    a <- Int -> m Type
    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 (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 -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.sort" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
           [ TCMT IO Doc
    "sortOfE"
           , TCMT IO Doc
    "  a  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a
           , TCMT IO Doc
    "  hd = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd [])
           , TCMT IO Doc
    "  e  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elim -> TCMT IO 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)
                    {-then-} (Blocker -> m Sort
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock)  -- Not IMPOSSIBLE because of possible non-confluent rewriting (see #5531)
                    {-else-} 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

    -- | Reconstruct the minimal sort of a type (ignoring the sort annotation).
    sortOfType
      :: forall m. (PureTCM m, MonadBlock m)
      => Type -> m Sort
    sortOfType :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => 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