{-# 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.Options ( isLevelUniverseEnabled )
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 Type -> TCM Sort #-}
-- | Infer the sort of a Pi type.
--   If we can compute the sort straight away, return that.
--   Otherwise, return a 'PiSort'.
--   Note that this function does NOT check PTS constraints, use 'hasPTSRule' for that
inferPiSort :: (PureTCM m, MonadConstraint m)
  => Dom Type  -- ^ Domain of the Pi type.
  -> Abs Type  -- ^ (Dependent) codomain of the Pi type.
  -> m Sort    -- ^ Sort of the Pi type.
inferPiSort :: forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Abs Type -> m Sort
inferPiSort Dom Type
a Abs Type
b = Dom Term -> Sort -> Abs Sort -> m Sort
forall (m :: * -> *).
HasOptions m =>
Dom Term -> Sort -> Abs Sort -> m Sort
piSortM (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) (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort 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)

{-# SPECIALIZE inferFunSort :: Dom Type -> Type -> TCM Sort #-}
-- | As @inferPiSort@, but for a nondependent function type.
--
inferFunSort :: (PureTCM m, MonadConstraint m)
  => Dom Type  -- ^ Domain of the function type.
  -> Type      -- ^ Sort of the codomain of the function type.
  -> m Sort    -- ^ Sort of the function type.
inferFunSort :: forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Type -> m Sort
inferFunSort Dom Type
a Type
b = Sort -> Sort -> m Sort
forall (m :: * -> *). HasOptions m => Sort -> Sort -> m Sort
funSortM (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
b)

-- | @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
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
<+> Dom Type -> Abs Sort -> (Sort -> TCMT IO Doc) -> TCMT IO Doc
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Sort
s Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM
    ]
  -- If @LevelUniv@ is disabled then all pi sorts are valid.
  hasLevelUniv <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isLevelUniverseEnabled
  if not hasLevelUniv || alwaysValidCodomain (unAbs s)
  then yes
  else do
    sb <- reduceB =<< piSortM (unEl <$> a) (getSort a) 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
                  | Bool
otherwise         -> Blocker -> TCM ()
postpone Blocker
b
      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
      NotBlocked{}                    -> 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
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.conv.sort" Int
35 VerboseKey
"hasPTSRule succeeded"
    no :: a -> Sort -> m b
no a
sb Sort
t = do
      VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
    postpone :: Blocker -> TCM ()
postpone Blocker
b = Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
b (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Constraint
HasPTSRule Dom Type
a Abs Sort
s

-- | Recursively check that an iterated function type constructed by @telePi@
--   is well-sorted.
checkTelePiSort :: Telescope -> Sort -> TCM ()
checkTelePiSort :: Telescope -> Sort -> TCM ()
checkTelePiSort Telescope
tel Sort
s = 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
$ Telescope -> TCMT IO Sort
loop Telescope
tel
  where
    loop :: Telescope -> TCM Sort
    loop :: Telescope -> TCMT IO Sort
loop Telescope
EmptyTel = Sort -> TCMT IO Sort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
    loop (ExtendTel Dom Type
a Abs Telescope
atel) = do
      s' <- Dom Type
-> (Telescope -> TCMT IO Sort)
-> Abs Telescope
-> TCMT IO (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 Telescope -> TCMT IO Sort
loop Abs Telescope
atel
      hasPTSRule a s'
      piSortM (unEl <$> a) (getSort $ unDom a) s'

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
  VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
        sa <- Term -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf (Term -> m Sort) -> Term -> m Sort
forall a b. (a -> b) -> a -> b
$ 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
        sb <- mapAbstraction adom (sortOf . unEl) b
        piSortM (unEl <$> adom) sa 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 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 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
      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
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