{-# OPTIONS_GHC -Wunused-imports #-}

{-# 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.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
  Sort
s <- Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s
  case Sort -> Either Blocker Sort
univSort' Sort
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
  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

{-# 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
  Blocked Sort
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
  Abs (Blocked Sort)
s2' <- Dom Type
-> (Sort -> m (Blocked Sort)) -> Abs Sort -> m (Abs (Blocked 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 (Blocked Sort)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Abs Sort
s
  let s1 :: Sort
s1 = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s1'
  let s2 :: Abs Sort
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 Dom Term -> Sort -> Abs Sort -> Either Blocker 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 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
  Blocked Sort
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
  Blocked Sort
s2' <- Sort -> m (Blocked Sort)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort
s
  let s1 :: Sort
s1 = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s1'
  let s2 :: Sort
s2 = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s2'
  case Sort -> Sort -> Either Blocker Sort
funSort' Sort
s1 Sort
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
    Blocked Sort
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 Blocked Sort
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.
  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 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
        Sort
sa <- Term -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint 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, 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) Abs Type
b
        Dom Type -> Abs Sort -> m Sort
forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Dom Type -> Abs Sort -> m Sort
inferPiSort (Dom Type
adom Dom Type -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
sa Term
a) Abs Sort
sb
      Sort Sort
s     -> 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
        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 :: * -> *). 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 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
        ]

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

      let
        a' :: Type
a' = Blocked Type -> Type
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
ba
        fallback :: m Sort
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 Elim
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 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
          Term
_ -> m Sort
fallback

        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

{-# 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