    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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.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

    {-# SPECIALIZE inferUnivSort :: Sort -> TCM Sort #-}
    -- | 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
      s <- Sort -> m Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Sort
    s
      case univSort' s of
        Right Sort
    s' -> Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s'
        Left Blocker
    _ -> 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 a. a -> m a
    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

    {-# SPECIALIZE sortFitsIn :: Sort -> Sort -> TCM () #-}
    sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
    sortFitsIn :: forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    sortFitsIn Sort
    a Sort
    b = do
      b' <- Sort -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    Sort -> m Sort
    inferUnivSort Sort
    a
      ifM (optCumulativity <$> pragmaOptions)
        (leqSort b' b)
        (equalSort b' 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

    {-# SPECIALIZE inferPiSort :: Dom Type -> Abs Sort -> TCM Sort #-}
    -- | Infer the sort of a Pi type.
    --   If we can compute the sort straight away, return that.
    --   Otherwise, return a 'PiSort' and add a constraint to ensure we can compute the sort eventually.
    --
    inferPiSort :: (PureTCM m, MonadConstraint m)
      => Dom Type  -- ^ Domain of the Pi type.
      -> Abs Sort  -- ^ (Dependent) sort of the codomain of the Pi type.
      -> m Sort    -- ^ Sort of the Pi type.
    inferPiSort :: forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    Dom Type -> Abs Sort -> m Sort
    inferPiSort Dom Type
    a Abs Sort
    s = do
      s1' <- Sort -> m (Blocked Sort)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB (Sort -> m (Blocked Sort)) -> Sort -> m (Blocked Sort)
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Dom Type
    a
      s2' <- mapAbstraction a reduceB s
      let s1 = Blocked Sort -> Sort
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Sort
    s1'
      let s2 = Blocked Sort -> Sort
    forall t a. Blocked' t a -> a
    ignoreBlocking (Blocked Sort -> Sort) -> Abs (Blocked Sort) -> Abs Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (Blocked Sort)
    s2'
      --Jesper, 2018-04-23: disabled PTS constraints for now,
      --this assumes that piSort can only be blocked by unsolved metas.
      --Arthur Adjedj, 2023-02-27, Turned PTS back on,
      --piSort can now be blocked by Leveluniv
      case piSort' (unEl <$> a) s1 s2 of
        Right Sort
    s -> Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
        Left Blocker
    b -> do
          let b' :: Blocker
    b' = Blocker -> Blocker -> Blocker
    unblockOnEither (Blocked Sort -> Blocker
    forall t a. Blocked' t a -> Blocker
    getBlocker Blocked Sort
    s1') (Blocked Sort -> Blocker
    forall t a. Blocked' t a -> Blocker
    getBlocker (Blocked Sort -> Blocker) -> Blocked Sort -> Blocker
    forall a b. (a -> b) -> a -> b
    $ Abs (Blocked Sort) -> Blocked Sort
    forall a. Abs a -> a
    unAbs Abs (Blocked Sort)
    s2')
          Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint (Blocker -> Blocker -> Blocker
    unblockOnEither Blocker
    b Blocker
    b') (Constraint -> m ()) -> Constraint -> m ()
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Sort -> Constraint
    HasPTSRule Dom Type
    a Abs Sort
    s2
          Sort -> m Sort
    forall a. a -> m a
    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
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    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

    {-# SPECIALIZE inferFunSort :: Dom Type -> Sort -> TCM Sort #-}
    -- | As @inferPiSort@, but for a nondependent function type.
    --
    inferFunSort :: (PureTCM m, MonadConstraint m)
      => Dom Type  -- ^ Domain of the function type.
      -> Sort      -- ^ Sort of the codomain of the function type.
      -> m Sort    -- ^ Sort of the function type.
    inferFunSort :: forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    Dom Type -> Sort -> m Sort
    inferFunSort Dom Type
    a Sort
    s = do
      s1' <- Sort -> m (Blocked Sort)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB (Sort -> m (Blocked Sort)) -> Sort -> m (Blocked Sort)
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Dom Type
    a
      s2' <- reduceB s
      let s1 = Blocked Sort -> Sort
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Sort
    s1'
      let s2 = Blocked Sort -> Sort
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Sort
    s2'
      case funSort' s1 s2 of
        Right Sort
    s -> Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
        Left Blocker
    b -> do
          let b' :: Blocker
    b' = Blocker -> Blocker -> Blocker
    unblockOnEither (Blocked Sort -> Blocker
    forall t a. Blocked' t a -> Blocker
    getBlocker Blocked Sort
    s1') (Blocked Sort -> Blocker
    forall t a. Blocked' t a -> Blocker
    getBlocker Blocked Sort
    s2')
          Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint (Blocker -> Blocker -> Blocker
    unblockOnEither Blocker
    b Blocker
    b') (Constraint -> m ()) -> Constraint -> m ()
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Sort -> Constraint
    HasPTSRule Dom Type
    a (ArgName -> Sort -> Abs Sort
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    "_" Sort
    s2)
          Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    s1 Sort
    s2
      -- Andreas, 2023-05-20:  I made inferFunSort step-by-step analogous to inferPiSort.
      -- Unifying them seems unfeasible, though; too much parametrization...

    -- | @hasPTSRule a x.s@ checks that we can form a Pi-type @(x : a) -> b@ where @b : s@.
    --
    hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
    hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
    hasPTSRule Dom Type
    a Abs Sort
    s = do
      ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.conv.sort" Int
    35 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    "hasPTSRule"
        , TCMT IO Doc
    "a =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
    prettyTCM Dom Type
    a
        , TCMT IO Doc
    "s =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM (Abs Sort -> Sort
    forall a. Abs a -> a
    unAbs Abs Sort
    s)
        ]
      if Sort -> Bool
    forall {t}. Sort' t -> Bool
    alwaysValidCodomain (Sort -> Bool) -> Sort -> Bool
    forall a b. (a -> b) -> a -> b
    $ Abs Sort -> Sort
    forall a. Abs a -> a
    unAbs Abs Sort
    s
      then TCM ()
    yes
      else do
        sb <- Sort -> TCMT IO (Blocked Sort)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB (Sort -> TCMT IO (Blocked Sort))
    -> TCMT IO Sort -> TCMT IO (Blocked Sort)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Dom Type -> Abs Sort -> TCMT IO Sort
    forall (m :: * -> *).
    (PureTCM m, MonadConstraint m) =>
    Dom Type -> Abs Sort -> m Sort
    inferPiSort Dom Type
    a Abs Sort
    s
        case sb of
          Blocked Blocker
    b Sort
    t | Blocker
    neverUnblock Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    b -> Blocked Sort -> Sort -> TCM ()
    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{}        -> Blocked Sort -> Sort -> TCM ()
    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{}         -> Blocked Sort -> Sort -> TCM ()
    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
        -- Do we end in a standard sort (Prop, Type, SSet)?
        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 (Sort' t -> Bool) -> Sort' t -> Bool
    forall a b. (a -> b) -> a -> b
    $ Abs (Sort' t) -> Sort' t
    forall a. Abs a -> a
    unAbs Abs (Sort' t)
    s
          Sort' t
    _ -> Bool
    False

        yes :: TCM ()
    yes = do
          ArgName -> Int -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> ArgName -> m ()
    reportSLn ArgName
    "tc.conv.sort" Int
    35 ArgName
    "hasPTSRule succeeded"
        no :: a -> Sort -> m b
    no a
    sb Sort
    t = do
          ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.conv.sort" Int
    35 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "hasPTSRule fails on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    sb
          TypeError -> m b
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m b) -> TypeError -> m b
    forall a b. (a -> b) -> a -> b
    $ Sort -> TypeError
    InvalidTypeSort Sort
    t

    -- | 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 :: Type -> TCM ()
    checkTelePiSort (El Sort
    s (Pi Dom Type
    a Abs Type
    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.
      Dom Type -> Abs Sort -> TCM ()
    hasPTSRule Dom Type
    a (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort (Type -> Sort) -> Abs Type -> Abs Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type
    b)
      Dom Type -> Abs Type -> (Type -> TCM ()) -> TCM ()
    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
    _ = () -> TCM ()
    forall a. a -> TCMT IO a
    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.
      bt <- Type -> m (Blocked Type)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Type
    t
      case unEl (ignoreBlocking bt) of
        Sort Sort
    s                     -> Sort -> m a
    yes Sort
    s
        Term
    _      | Blocked Blocker
    m Type
    _ <- Blocked Type
    bt -> Blocker -> m a
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    m
               | Bool
    otherwise         -> m a
    no

    {-# SPECIALIZE ifNotSort :: Type -> TCM a -> (Sort -> TCM a) -> TCM a #-}
    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

    {-# SPECIALIZE shouldBeSort :: Type -> TCM Sort #-}
    -- | 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 a. a -> m a
    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)

    {-# SPECIALIZE sortOf :: Term -> TCM Sort #-}
    -- | Reconstruct the sort of a term.
    --
    --   Precondition: given term is a well-sorted type.
    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
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.sort" Int
    60 (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
    forall (m :: * -> *). MonadPretty m => Term -> 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
            sa <- Term -> m Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadConstraint m) =>
    Term -> m Sort
    sortOf Term
    a
            sb <- mapAbstraction adom (sortOf . unEl) b
            inferPiSort (adom $> El sa a) sb
          Sort Sort
    s     -> Sort -> m Sort
    forall a. a -> m a
    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
            a <- Int -> m Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
            sortOfE a (Var i) es
          Def QName
    f Elims
    es   -> do
            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
            sortOfE a (Def f) es
          MetaV MetaId
    x Elims
    es -> do
            a <- MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x
            sortOfE a (MetaV x) 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 ArgName
    s Elims
    _  -> ArgName -> m Sort
    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 []     = 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 a. a -> m a
    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
          ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM Elim
    e
            ]

          ba <- Type -> m (Blocked Type)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Type
    a

          let
            a' = Blocked Type -> Type
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Type
    ba
            fallback = case Blocked Type
    ba of
              Blocked Blocker
    m Type
    _ -> Blocker -> m Sort
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    m

              -- Not IMPOSSIBLE because of possible non-confluent rewriting (see #5531)
              Blocked Type
    _ -> 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 a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock)
                {-else-} m Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          case e of
            Apply (Arg ArgInfo
    ai Term
    v) -> case Type -> Term
    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 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
    _ -> m Sort
    fallback

            Proj ProjOrigin
    o QName
    f -> case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a' of
              Def{} -> do
                ~(El _ (Pi b 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'
                hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
                sortOfE (c `absApp` (hd [])) hd' es
              Term
    _ -> m Sort
    fallback

            IApply Term
    x Term
    y Term
    r -> do
              (b , 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'
              sortOfE (c `absApp` r) (hd . (e:)) es

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