{-# 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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
=<< 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 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, 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 -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sort" VerboseLevel
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
       [ TCM Doc
"sortOfE"
       , TCM Doc
"  a  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
       , TCM Doc
"  hd = " 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 (Elims -> Term
hd [])
       , TCM Doc
"  e  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim -> TCM 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 :: 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