    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.SizedTypes where

    import Prelude hiding (null)

    import Control.Monad.Trans.Maybe ( MaybeT(..), runMaybeT )
    import Control.Monad.Except ( MonadError(..) )
    import Control.Monad.Writer ( MonadWriter(..), WriterT(..), runWriterT )

    import qualified Data.Foldable as Fold
    import qualified Data.List as List
    import qualified Data.Set as Set
    import Data.Set (Set)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Common.Pretty (Pretty)
    import qualified Agda.Syntax.Common.Pretty as P

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Pretty.Constraint () -- instance PrettyTCM Constraint
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (MonadCheckInternal, infer)
    import {-# SOURCE #-} Agda.TypeChecking.Constraints () -- instance MonadConstraint TCM
    import {-# SOURCE #-} Agda.TypeChecking.Conversion

    import Agda.Utils.Functor
    import Agda.Utils.List as List
    import Agda.Utils.List1 (pattern (:|))
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Utils.ProfileOptions as Profile
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- * SIZELT stuff
    ------------------------------------------------------------------------

    -- | Check whether a type is either not a SIZELT or a SIZELT that is non-empty.
    checkSizeLtSat :: Term -> TCM ()
    checkSizeLtSat :: Term -> TCM ()
    checkSizeLtSat Term
    t = TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO Bool
    haveSizeLt (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        tel <- TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
        sep
          [ "checking that " <+> prettyTCM t <+> " is not an empty type of sizes"
          , if null tel then empty else do
            "in context " <+> inTopContext (prettyTCM tel)
          ]
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size" Int
    60 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "- raw type = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Show a => a -> [Char]
    show Term
    t
      let postpone :: Blocker -> Term -> TCM ()
          postpone :: Blocker -> Term -> TCM ()
    postpone Blocker
    b Term
    t = do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.lt" Int
    20 (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
    sep
              [ TCMT IO Doc
    "- postponing `not empty type of sizes' check for " 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 ]
            Blocker -> Constraint -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    b (Constraint -> TCM ()) -> Constraint -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Constraint
    CheckSizeLtSat Term
    t
      let ok :: TCM ()
          ok :: TCM ()
    ok = [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.lt" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "- succeeded: not an empty type of sizes"
      Term
    -> (Blocker -> Term -> TCM ())
    -> (NotBlocked -> Term -> TCM ())
    -> TCM ()
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Term
    t Blocker -> Term -> TCM ()
    postpone ((NotBlocked -> Term -> TCM ()) -> TCM ())
    -> (NotBlocked -> Term -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    _ Term
    t -> do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.lt" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "- type is not blocked"
        TCMT IO (Maybe BoundedSize)
    -> TCM () -> (BoundedSize -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Term -> TCMT IO (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Term -> m (Maybe BoundedSize)
    isSizeType Term
    t) TCM ()
    ok ((BoundedSize -> TCM ()) -> TCM ())
    -> (BoundedSize -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ BoundedSize
    b -> do
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.lt" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    " - type is a size type"
          case BoundedSize
    b of
            BoundedSize
    BoundedNo -> TCM ()
    ok
            BoundedLt Term
    b -> do
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.lt" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    " - type is SIZELT" 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
    b
              Term
    -> (Blocker -> Term -> TCM ())
    -> (NotBlocked -> Term -> TCM ())
    -> TCM ()
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Term
    b (\ Blocker
    x Term
    _ -> Blocker -> Term -> TCM ()
    postpone Blocker
    x Term
    t) ((NotBlocked -> Term -> TCM ()) -> TCM ())
    -> (NotBlocked -> Term -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    _ Term
    b -> do
                [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.lt" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    " - size bound is not blocked"
                Constraint -> TCM () -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Constraint -> m () -> m ()
    catchConstraint (Term -> Constraint
    CheckSizeLtSat Term
    t) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                  TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Term -> TCMT IO Bool
    checkSizeNeverZero Term
    b) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                    TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> TypeError
    EmptyTypeOfSizes Term
    t

    -- | Precondition: Term is reduced and not blocked.
    --   Throws a 'patternViolation' if undecided
    checkSizeNeverZero :: Term -> TCM Bool
    checkSizeNeverZero :: Term -> TCMT IO Bool
    checkSizeNeverZero Term
    u = do
      v <- Term -> TCMT IO SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    u
      case v of
        SizeView
    SizeInf     -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True  -- OK, infty is never 0.
        SizeSuc{}   -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True  -- OK, a + 1 is never 0.
        OtherSize Term
    u ->
          case Term
    u of
            Var Int
    i [] -> Int -> TCMT IO Bool
    checkSizeVarNeverZero Int
    i
            -- neutral sizes cannot be guaranteed > 0
            Term
    _ -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- -- | A size variable is never zero if it is the strict upper bound of
    -- --   some other size variable in context.
    -- --   Eg. @i : Size, j : Size< i@ |- i is never zero.
    -- --   Throws a 'patternViolation' if undecided.
    -- checkSizeVarNeverZero :: Int -> TCM Bool
    -- checkSizeVarNeverZero i = do
    --   -- Looking for a variable j : Size< i, we can restrict to the last i
    --   -- entries, as this variable necessarily has been defined later than i.
    --   doms <- take i <$> getContext
    --   -- We raise each type to make sense in the current context.
    --   let ts = zipWith raise [1..] $ map (snd . unDom) doms
    --   reportSDoc "tc.size" 15 $ sep
    --     [ "checking that size " <+> prettyTCM (var i) <+> " is never 0"
    --     , "in context " <+> do sep $ map prettyTCM ts
    --     ]
    --   foldr f (return False) ts
    --   where
    --   f t cont = do
    --     -- If we encounter a blocked type in the context, we cannot
    --     -- definitely say no.
    --     let yes     = return True
    --         no      = cont
    --         perhaps = cont >>= \ res -> if res then return res else patternViolation
    --     ifBlocked t (\ _ _ -> perhaps) $ \ t -> do
    --       caseMaybeM (isSizeType t) no $ \ b -> do
    --         case b of
    --           BoundedNo -> no
    --           BoundedLt u -> ifBlocked u (\ _ _ -> perhaps) $ \ u -> do
    --             case u of
    --                Var i' [] | i == i' -> yes
    --                _ -> no

    -- | Checks that a size variable is ensured to be @> 0@.
    --   E.g. variable @i@ cannot be zero in context
    --   @(i : Size) (j : Size< ↑ ↑ i) (k : Size< j) (k' : Size< k)@.
    --   Throws a 'patternViolation' if undecided.
    checkSizeVarNeverZero :: Int -> TCM Bool
    checkSizeVarNeverZero :: Int -> TCMT IO Bool
    checkSizeVarNeverZero Int
    i = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checkSizeVarNeverZero" 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 (Int -> Term
    var Int
    i)
      -- Looking for the minimal value for size variable i,
      -- we can restrict to the last i
      -- entries, as only these can contain i in an upper bound.
      ts <- (ContextEntry -> Type) -> Context -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ContextEntry -> Type
    ctxEntryType (Context -> [Type]) -> (Context -> Context) -> Context -> [Type]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Context -> Context
    forall a. Int -> [a] -> [a]
    take Int
    i (Context -> [Type]) -> TCMT IO Context -> TCMT IO [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
      -- If we encountered a blocking meta in the context, we cannot
      -- say ``no'' for sure.
      (n, blockers) <- runWriterT $ minSizeValAux ts $ repeat 0
      let blocker = Set Blocker -> Blocker
    unblockOnAll Set Blocker
    blockers
      if n > 0 then return True else
        if blocker == alwaysUnblock
          then return False
          else patternViolation blocker
      where
      -- Compute the least valuation for size context ts above the
      -- given valuation and return its last value.
      minSizeValAux :: [Type] -> [Int] -> WriterT (Set Blocker) TCM Int
      minSizeValAux :: [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
    minSizeValAux [Type]
    _        []      = WriterT (Set Blocker) (TCMT IO) Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      minSizeValAux []       (Int
    n : [Int]
    _) = Int -> WriterT (Set Blocker) (TCMT IO) Int
    forall a. a -> WriterT (Set Blocker) (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    n
      minSizeValAux (Type
    t : [Type]
    ts) (Int
    n : [Int]
    ns) = do
        [Char] -> Int -> TCMT IO Doc -> WriterT (Set Blocker) (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size" Int
    60 (TCMT IO Doc -> WriterT (Set Blocker) (TCMT IO) ())
    -> TCMT IO Doc -> WriterT (Set Blocker) (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
           [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "minSizeVal (n:ns) = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [Char]
    forall a. Show a => a -> [Char]
    show (Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    take ([Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    ts Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    2) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int
    nInt -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    :[Int]
    ns) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                 [Char]
    " t =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> [Char]
    forall a. Show a => a -> [Char]
    show) Type
    t  -- prettyTCM t  -- Wrong context!
        -- n is the min. value for variable 0 which has type t.
        let cont :: WriterT (Set Blocker) (TCMT IO) Int
    cont = [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
    minSizeValAux [Type]
    ts [Int]
    ns
            perhaps :: Blocker -> WriterT (Set Blocker) (TCMT IO) Int
    perhaps Blocker
    x = Set Blocker -> WriterT (Set Blocker) (TCMT IO) ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Blocker -> Set Blocker
    forall a. a -> Set a
    Set.singleton Blocker
    x) WriterT (Set Blocker) (TCMT IO) ()
    -> WriterT (Set Blocker) (TCMT IO) Int
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall a b.
    WriterT (Set Blocker) (TCMT IO) a
    -> WriterT (Set Blocker) (TCMT IO) b
    -> WriterT (Set Blocker) (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> WriterT (Set Blocker) (TCMT IO) Int
    cont
        -- If we encounter a blocked type in the context, we cannot
        -- give a definite answer.
        Type
    -> (Blocker -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
    -> (NotBlocked -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Type
    t (\ Blocker
    x Type
    _ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
    perhaps Blocker
    x) ((NotBlocked -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
     -> WriterT (Set Blocker) (TCMT IO) Int)
    -> (NotBlocked -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    _ Type
    t -> do
          WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize)
    -> WriterT (Set Blocker) (TCMT IO) Int
    -> (BoundedSize -> WriterT (Set Blocker) (TCMT IO) Int)
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (TCMT IO (Maybe BoundedSize)
    -> WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize)
    forall a. TCM a -> WriterT (Set Blocker) (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO (Maybe BoundedSize)
     -> WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize))
    -> TCMT IO (Maybe BoundedSize)
    -> WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize)
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Type -> m (Maybe BoundedSize)
    isSizeType Type
    t) WriterT (Set Blocker) (TCMT IO) Int
    cont ((BoundedSize -> WriterT (Set Blocker) (TCMT IO) Int)
     -> WriterT (Set Blocker) (TCMT IO) Int)
    -> (BoundedSize -> WriterT (Set Blocker) (TCMT IO) Int)
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall a b. (a -> b) -> a -> b
    $ \ BoundedSize
    b -> do
            case BoundedSize
    b of
              BoundedSize
    BoundedNo -> WriterT (Set Blocker) (TCMT IO) Int
    cont
              BoundedLt Term
    u -> Term
    -> (Blocker -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
    -> (NotBlocked -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Term
    u (\ Blocker
    x Term
    _ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
    perhaps Blocker
    x) ((NotBlocked -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
     -> WriterT (Set Blocker) (TCMT IO) Int)
    -> (NotBlocked -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
    -> WriterT (Set Blocker) (TCMT IO) Int
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    _ Term
    u -> do
                [Char] -> Int -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size" Int
    60 ([Char] -> WriterT (Set Blocker) (TCMT IO) ())
    -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "minSizeVal upper bound u = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Show a => a -> [Char]
    show Term
    u
                v <- TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView
    forall a. TCM a -> WriterT (Set Blocker) (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView)
    -> TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM DeepSizeView
    forall (m :: * -> *).
    (PureTCM m, MonadTCError m) =>
    Term -> m DeepSizeView
    deepSizeView Term
    u
                case v of
                  -- Variable 0 has bound @(< j + m)@
                  -- meaning that @minval(j) > n - m@, i.e., @minval(j) >= n+1-m@.
                  -- Thus, we update the min value for @j@ with function @(max (n+1-m))@.
                  DSizeVar (ProjectedVar Int
    j []) Int
    m -> do
                    [Char] -> Int -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size" Int
    60 ([Char] -> WriterT (Set Blocker) (TCMT IO) ())
    -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "minSizeVal upper bound v = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ DeepSizeView -> [Char]
    forall a. Show a => a -> [Char]
    show DeepSizeView
    v
                    let ns' :: [Int]
    ns' = Int -> (Int -> Int) -> [Int] -> [Int]
    forall a. Int -> (a -> a) -> [a] -> [a]
    List.updateAt Int
    j (Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max (Int -> Int -> Int) -> Int -> Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    m) [Int]
    ns
                    [Char] -> Int -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size" Int
    60 ([Char] -> WriterT (Set Blocker) (TCMT IO) ())
    -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "minSizeVal ns' = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [Char]
    forall a. Show a => a -> [Char]
    show (Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    take ([Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    ts Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [Int]
    ns')
                    [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
    minSizeValAux [Type]
    ts [Int]
    ns'
                  DSizeMeta MetaId
    x [Elim]
    _ Int
    _ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
    perhaps (MetaId -> Blocker
    unblockOnMeta MetaId
    x)
                  DeepSizeView
    _ -> WriterT (Set Blocker) (TCMT IO) Int
    cont

    -- | Check whether a variable in the context is bounded by a size expression.
    --   If @x : Size< a@, then @a@ is returned.
    isBounded :: PureTCM m => Nat -> m BoundedSize
    isBounded :: forall (m :: * -> *). PureTCM m => Int -> m BoundedSize
    isBounded Int
    i = Type -> m BoundedSize
    forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
    isBoundedSizeType (Type -> m BoundedSize) -> m Type -> m BoundedSize
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> m Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i

    isBoundedProjVar
      :: (MonadCheckInternal m, PureTCM m)
      => ProjectedVar -> m BoundedSize
    isBoundedProjVar :: forall (m :: * -> *).
    (MonadCheckInternal m, PureTCM m) =>
    ProjectedVar -> m BoundedSize
    isBoundedProjVar ProjectedVar
    pv = Type -> m BoundedSize
    forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
    isBoundedSizeType (Type -> m BoundedSize) -> m Type -> m BoundedSize
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> m Type
    forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
    infer (ProjectedVar -> Term
    unviewProjectedVar ProjectedVar
    pv)

    isBoundedSizeType :: PureTCM m => Type -> m BoundedSize
    isBoundedSizeType :: forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
    isBoundedSizeType Type
    t =
      Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t) m Term -> (Term -> m BoundedSize) -> m BoundedSize
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Def QName
    x [Apply Arg Term
    u] -> do
          sizelt <- BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinSizeLt
          return $ if (Just (Def x []) == sizelt) then BoundedLt $ unArg u else BoundedNo
        Term
    _ -> BoundedSize -> m BoundedSize
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return BoundedSize
    BoundedNo

    -- | Whenever we create a bounded size meta, add a constraint
    --   expressing the bound. First argument is the new meta and must be a @MetaV{}@.
    --   In @boundedSizeMetaHook v tel a@, @tel@ includes the current context.
    boundedSizeMetaHook
      :: ( MonadConstraint m
         , MonadTCEnv m
         , ReadTCState m
         , MonadAddContext m
         , HasOptions m
         , HasBuiltins m
         )
      => Term -> Telescope -> Type -> m ()
    boundedSizeMetaHook :: forall (m :: * -> *).
    (MonadConstraint m, MonadTCEnv m, ReadTCState m, MonadAddContext m,
     HasOptions m, HasBuiltins m) =>
    Term -> Telescope -> Type -> m ()
    boundedSizeMetaHook v :: Term
    v@(MetaV MetaId
    x [Elim]
    _) Telescope
    tel0 Type
    a = do
      res <- Type -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Type -> m (Maybe BoundedSize)
    isSizeType Type
    a
      case res of
        Just (BoundedLt Term
    u) -> do
          n <- m Int
    forall (m :: * -> *). MonadTCEnv m => m Int
    getContextSize
          let tel | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0     = ListTel -> Telescope
    telFromList (ListTel -> Telescope) -> ListTel -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> ListTel -> ListTel
    forall a. Int -> [a] -> [a]
    drop Int
    n (ListTel -> ListTel) -> ListTel -> ListTel
    forall a b. (a -> b) -> a -> b
    $ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel0
                  | Bool
    otherwise = Telescope
    tel0
          addContext tel $ do
            v <- sizeSuc 1 $ raise (size tel) v `apply` teleArgs tel
            -- compareSizes CmpLeq v u
            addConstraint (unblockOnMeta x) $ ValueCmp CmpLeq AsSizes v u
        Maybe BoundedSize
    _ -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    boundedSizeMetaHook Term
    _ Telescope
    _ Type
    _ = m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | @trySizeUniv cmp t m n x els1 y els2@
    --   is called as a last resort when conversion checking @m `cmp` n : t@
    --   failed for definitions @m = x els1@ and @n = y els2@,
    --   where the heads @x@ and @y@ are not equal.
    --
    --   @trySizeUniv@ accounts for subtyping between SIZELT and SIZE,
    --   like @Size< i =< Size@.
    --
    --   If it does not succeed it reports failure of conversion check.
    trySizeUniv
      :: MonadConversion m
      => Comparison -> CompareAs -> Term -> Term
      -> QName -> Elims -> QName -> Elims -> m ()
    trySizeUniv :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison
    -> CompareAs
    -> Term
    -> Term
    -> QName
    -> [Elim]
    -> QName
    -> [Elim]
    -> m ()
    trySizeUniv Comparison
    cmp CompareAs
    t Term
    m Term
    n QName
    x [Elim]
    els1 QName
    y [Elim]
    els2 = do
      let failure :: forall m a. MonadTCError m => m a
          failure :: forall (m :: * -> *) a. MonadTCError m => m a
    failure = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Term -> Term -> CompareAs -> TypeError
    UnequalTerms Comparison
    cmp Term
    m Term
    n CompareAs
    t
          forceInfty :: Arg Term -> m ()
    forceInfty Arg Term
    u = Comparison -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Term -> Term -> m ()
    compareSizes Comparison
    CmpEq (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u) (Term -> m ()) -> m Term -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
      -- Get the SIZE built-ins.
      (size, sizelt) <- m (QName, QName)
    -> ((QName, QName) -> m (QName, QName))
    -> Maybe (QName, QName)
    -> m (QName, QName)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m (QName, QName)
    forall (m :: * -> *) a. MonadTCError m => m a
    failure (QName, QName) -> m (QName, QName)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe (QName, QName) -> m (QName, QName))
    -> m (Maybe (QName, QName)) -> m (QName, QName)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MaybeT m (QName, QName) -> m (Maybe (QName, QName))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT do
        size   <- m (Maybe QName) -> MaybeT m QName
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe QName) -> MaybeT m QName)
    -> m (Maybe QName) -> MaybeT m QName
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSize
        sizelt <- MaybeT $ getBuiltinName' builtinSizeLt
        pure (size, sizelt)
      case (cmp, els1, els2) of
         -- Case @Size< _ <= Size@: true.
         (Comparison
    CmpLeq, [Elim
    _], [])  | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    sizelt Bool -> Bool -> Bool
    && QName
    y QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    size -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         -- Case @Size< u = Size@: forces @u = ∞@.
         (Comparison
    _, [Apply Arg Term
    u], []) | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    sizelt Bool -> Bool -> Bool
    && QName
    y QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    size -> Arg Term -> m ()
    forall {m :: * -> *}.
    (MonadMetaSolver m, MonadWarning m, MonadStatistics m,
     MonadFresh ProblemId m, MonadFresh Int m) =>
    Arg Term -> m ()
    forceInfty Arg Term
    u
         (Comparison
    _, [], [Apply Arg Term
    u]) | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    size Bool -> Bool -> Bool
    && QName
    y QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    sizelt -> Arg Term -> m ()
    forall {m :: * -> *}.
    (MonadMetaSolver m, MonadWarning m, MonadStatistics m,
     MonadFresh ProblemId m, MonadFresh Int m) =>
    Arg Term -> m ()
    forceInfty Arg Term
    u
         -- This covers all cases for SIZE and SIZELT.
         -- The remaining case is for @x@ and @y@ which are not size built-ins.
         (Comparison, [Elim], [Elim])
    _                                             -> m ()
    forall (m :: * -> *) a. MonadTCError m => m a
    failure

    ------------------------------------------------------------------------
    -- * Size views that 'reduce'.
    ------------------------------------------------------------------------

    -- | Compute the deep size view of a term.
    --   Precondition: sized types are enabled.
    deepSizeView :: (PureTCM m, MonadTCError m) => Term -> m DeepSizeView
    deepSizeView :: forall (m :: * -> *).
    (PureTCM m, MonadTCError m) =>
    Term -> m DeepSizeView
    deepSizeView Term
    v = do
      inf <- BuiltinId -> m QName
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    builtinSizeInf
      suc <- getBuiltinName_ builtinSizeSuc
      let loop Term
    v =
            Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v m Term -> (Term -> m DeepSizeView) -> m DeepSizeView
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Def QName
    x []        | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    inf -> DeepSizeView -> m DeepSizeView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ DeepSizeView
    DSizeInf
              Def QName
    x [Apply Arg Term
    u] | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    suc -> QName -> DeepSizeView -> DeepSizeView
    sizeViewSuc_ QName
    suc (DeepSizeView -> DeepSizeView) -> m DeepSizeView -> m DeepSizeView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m DeepSizeView
    loop (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u)

              Var Int
    i [Elim]
    es | Just ProjectedVar
    pv <- Int -> [(ProjOrigin, QName)] -> ProjectedVar
    ProjectedVar Int
    i ([(ProjOrigin, QName)] -> ProjectedVar)
    -> Maybe [(ProjOrigin, QName)] -> Maybe ProjectedVar
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Elim -> Maybe (ProjOrigin, QName))
    -> [Elim] -> Maybe [(ProjOrigin, QName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim [Elim]
    es
                                         -> DeepSizeView -> m DeepSizeView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ ProjectedVar -> Int -> DeepSizeView
    DSizeVar ProjectedVar
    pv Int
    0
              MetaV MetaId
    x [Elim]
    us                 -> DeepSizeView -> m DeepSizeView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [Elim] -> Int -> DeepSizeView
    DSizeMeta MetaId
    x [Elim]
    us Int
    0
              Term
    v                          -> DeepSizeView -> m DeepSizeView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ Term -> DeepSizeView
    DOtherSize Term
    v
      loop v

    sizeMaxView :: PureTCM m => Term -> m SizeMaxView
    sizeMaxView :: forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
    sizeMaxView Term
    v = do
      inf <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSizeInf
      suc <- getBuiltinName' builtinSizeSuc
      max <- getBuiltinName' builtinSizeMax
      let loop Term
    v = do
            v <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
            case v of
              Def QName
    x []                   | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    inf -> SizeMaxView -> m SizeMaxView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ DeepSizeView
    DSizeInf
              Def QName
    x [Apply Arg Term
    u]            | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    suc -> QName -> SizeMaxView -> SizeMaxView
    maxViewSuc_ (Maybe QName -> QName
    forall a. HasCallStack => Maybe a -> a
    fromJust Maybe QName
    suc) (SizeMaxView -> SizeMaxView) -> m SizeMaxView -> m SizeMaxView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m SizeMaxView
    loop (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u)
              Def QName
    x [Apply Arg Term
    u1, Apply Arg Term
    u2] | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    max -> SizeMaxView -> SizeMaxView -> SizeMaxView
    maxViewMax (SizeMaxView -> SizeMaxView -> SizeMaxView)
    -> m SizeMaxView -> m (SizeMaxView -> SizeMaxView)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m SizeMaxView
    loop (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u1) m (SizeMaxView -> SizeMaxView) -> m SizeMaxView -> m SizeMaxView
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m SizeMaxView
    loop (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u2)
              Var Int
    i [Elim]
    es | Just ProjectedVar
    pv <- Int -> [(ProjOrigin, QName)] -> ProjectedVar
    ProjectedVar Int
    i ([(ProjOrigin, QName)] -> ProjectedVar)
    -> Maybe [(ProjOrigin, QName)] -> Maybe ProjectedVar
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Elim -> Maybe (ProjOrigin, QName))
    -> [Elim] -> Maybe [(ProjOrigin, QName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim [Elim]
    es
                                            -> SizeMaxView -> m SizeMaxView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ ProjectedVar -> Int -> DeepSizeView
    DSizeVar ProjectedVar
    pv Int
    0
              MetaV MetaId
    x [Elim]
    us                    -> SizeMaxView -> m SizeMaxView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [Elim] -> Int -> DeepSizeView
    DSizeMeta MetaId
    x [Elim]
    us Int
    0
              Term
    _                             -> SizeMaxView -> m SizeMaxView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
    forall a b. (a -> b) -> a -> b
    $ Term -> DeepSizeView
    DOtherSize Term
    v
      loop v

    ------------------------------------------------------------------------
    -- * Size comparison that might add constraints.
    ------------------------------------------------------------------------

    {-# SPECIALIZE compareSizes :: Comparison -> Term -> Term -> TCM () #-}
    -- | Compare two sizes.
    compareSizes :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
    compareSizes :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Term -> Term -> m ()
    compareSizes Comparison
    cmp Term
    u Term
    v = [Char] -> Int -> [Char] -> m () -> m ()
    forall a. [Char] -> Int -> [Char] -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.conv.size" Int
    10 [Char]
    "compareSizes" (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    10 (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
    "Comparing sizes"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Comparison -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
    prettyTCM Comparison
    cmp
                       , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
                       ]
        ]
      [Char] -> Int -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.conv.size" Int
    60 (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        u <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
        v <- reduce v
        reportSDoc "tc.conv.size" 60 $
          nest 2 $ sep [ pretty u <+> prettyTCM cmp
                       , pretty v
                       ]
      ProfileOption -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Conversion (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> m ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "compare sizes"
      us <- Term -> m SizeMaxView
    forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
    sizeMaxView Term
    u
      vs <- sizeMaxView v
      compareMaxViews cmp us vs

    -- | Compare two sizes in max view.
    compareMaxViews :: (MonadConversion m) => Comparison -> SizeMaxView -> SizeMaxView -> m ()
    compareMaxViews :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> SizeMaxView -> SizeMaxView -> m ()
    compareMaxViews Comparison
    cmp SizeMaxView
    us SizeMaxView
    vs = case (Comparison
    cmp, SizeMaxView
    us, SizeMaxView
    vs) of
      (Comparison
    CmpLeq, SizeMaxView
    _, (DeepSizeView
    DSizeInf :| [DeepSizeView]
    _)) -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      (Comparison
    cmp,    DeepSizeView
    u :| [], DeepSizeView
    v :| []) -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> DeepSizeView -> DeepSizeView -> m ()
    compareSizeViews Comparison
    cmp DeepSizeView
    u DeepSizeView
    v
      (Comparison
    CmpLeq, SizeMaxView
    us,      DeepSizeView
    v :| []) -> SizeMaxView -> (DeepSizeView -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    Fold.forM_ SizeMaxView
    us ((DeepSizeView -> m ()) -> m ()) -> (DeepSizeView -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ DeepSizeView
    u -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> DeepSizeView -> DeepSizeView -> m ()
    compareSizeViews Comparison
    cmp DeepSizeView
    u DeepSizeView
    v
      (Comparison
    CmpLeq, SizeMaxView
    us,      SizeMaxView
    vs)      -> SizeMaxView -> (DeepSizeView -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    Fold.forM_ SizeMaxView
    us ((DeepSizeView -> m ()) -> m ()) -> (DeepSizeView -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ DeepSizeView
    u -> DeepSizeView -> SizeMaxView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    DeepSizeView -> SizeMaxView -> m ()
    compareBelowMax DeepSizeView
    u SizeMaxView
    vs
      (Comparison
    CmpEq,  SizeMaxView
    us,      SizeMaxView
    vs)      -> do
        Comparison -> SizeMaxView -> SizeMaxView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> SizeMaxView -> SizeMaxView -> m ()
    compareMaxViews Comparison
    CmpLeq SizeMaxView
    us SizeMaxView
    vs
        Comparison -> SizeMaxView -> SizeMaxView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> SizeMaxView -> SizeMaxView -> m ()
    compareMaxViews Comparison
    CmpLeq SizeMaxView
    vs SizeMaxView
    us

    -- | @compareBelowMax u vs@ checks @u <= max vs@.  Precondition: @size vs >= 2@
    compareBelowMax :: (MonadConversion m) => DeepSizeView -> SizeMaxView -> m ()
    compareBelowMax :: forall (m :: * -> *).
    MonadConversion m =>
    DeepSizeView -> SizeMaxView -> m ()
    compareBelowMax DeepSizeView
    u SizeMaxView
    vs = [Char] -> Int -> [Char] -> m () -> m ()
    forall a. [Char] -> Int -> [Char] -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.conv.size" Int
    45 [Char]
    "compareBelowMax" (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    45 (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
    sep
        [ DeepSizeView -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty DeepSizeView
    u
        , Comparison -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Comparison
    CmpLeq
        , SizeMaxView -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty SizeMaxView
    vs
        ]
      -- When trying several alternatives, we do not assign metas
      -- and also do not produce constraints (see 'giveUp' below).
      -- Andreas, 2019-03-28, issue #3600.
      m () -> m () -> m ()
    forall {e} {m :: * -> *} {a}. MonadError e m => m a -> m a -> m a
    alt (m () -> m ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ (m () -> m () -> m ()) -> NonEmpty (m ()) -> m ()
    forall a. (a -> a -> a) -> NonEmpty a -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    Fold.foldr1 m () -> m () -> m ()
    forall {e} {m :: * -> *} {a}. MonadError e m => m a -> m a -> m a
    alt (NonEmpty (m ()) -> m ()) -> NonEmpty (m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (DeepSizeView -> m ()) -> SizeMaxView -> NonEmpty (m ())
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Comparison -> DeepSizeView -> DeepSizeView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> DeepSizeView -> DeepSizeView -> m ()
    compareSizeViews Comparison
    CmpLeq DeepSizeView
    u) SizeMaxView
    vs) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    45 (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
    "compareBelowMax: giving up"
          ]
        u <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    u
        v <- unMaxView vs
        size <- sizeType
        giveUp CmpLeq size u v
      where
      alt :: m a -> m a -> m a
    alt m a
    c1 m a
    c2 = m a
    c1 m a -> (e -> m a) -> m a
    forall a. m a -> (e -> m a) -> m a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` m a -> e -> m a
    forall a b. a -> b -> a
    const m a
    c2

    compareSizeViews :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
    compareSizeViews :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> DeepSizeView -> DeepSizeView -> m ()
    compareSizeViews Comparison
    cmp DeepSizeView
    s1' DeepSizeView
    s2' = do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    45 (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
    hsep
        [ TCMT IO Doc
    "compareSizeViews"
        , DeepSizeView -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty DeepSizeView
    s1'
        , Comparison -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Comparison
    cmp
        , DeepSizeView -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty DeepSizeView
    s2'
        ]
      size <- m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType
      let (s1, s2) = removeSucs (s1', s2')
          withUnView Term -> Term -> m ()
    cont = do
            u <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    s1
            v <- unDeepSizeView s2
            cont u v
          failure = (Term -> Term -> m ()) -> m ()
    withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Term
    u Term
    v -> TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Term -> Term -> CompareAs -> TypeError
    UnequalTerms Comparison
    cmp Term
    u Term
    v CompareAs
    AsSizes
          continue Comparison
    cmp = (Term -> Term -> m ()) -> m ()
    withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> CompareAs -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> CompareAs -> Term -> Term -> m ()
    compareAtom Comparison
    cmp CompareAs
    AsSizes
      case (cmp, s1, s2) of
        (Comparison
    CmpLeq, DeepSizeView
    _,            DeepSizeView
    DSizeInf)   -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        (Comparison
    CmpEq,  DeepSizeView
    DSizeInf,     DeepSizeView
    DSizeInf)   -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        (Comparison
    CmpEq,  DSizeVar{},   DeepSizeView
    DSizeInf)   -> m ()
    failure
        (Comparison
    _    ,  DeepSizeView
    DSizeInf,     DSizeVar{}) -> m ()
    failure
        (Comparison
    _    ,  DeepSizeView
    DSizeInf,     DeepSizeView
    _         ) -> Comparison -> m ()
    continue Comparison
    CmpEq
        (Comparison
    CmpLeq, DSizeVar ProjectedVar
    i Int
    n, DSizeVar ProjectedVar
    j Int
    m) | ProjectedVar
    i ProjectedVar -> ProjectedVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProjectedVar
    j -> Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    m) m ()
    failure
        (Comparison
    CmpLeq, DSizeVar ProjectedVar
    i Int
    n, DSizeVar ProjectedVar
    j Int
    m) | ProjectedVar
    i ProjectedVar -> ProjectedVar -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ProjectedVar
    j -> do
           res <- ProjectedVar -> m BoundedSize
    forall (m :: * -> *).
    (MonadCheckInternal m, PureTCM m) =>
    ProjectedVar -> m BoundedSize
    isBoundedProjVar ProjectedVar
    i
           case res of
             BoundedSize
    BoundedNo -> m ()
    failure
             BoundedLt Term
    u' -> do
                -- now we have i < u', in the worst case i+1 = u'
                -- and we want to check i+n <= v
                v <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    s2
                if n > 0 then do
                  u'' <- sizeSuc (n - 1) u'
                  compareSizes cmp u'' v
                 else compareSizes cmp u' =<< sizeSuc 1 v
        (Comparison
    CmpLeq, DeepSizeView
    s1,        DeepSizeView
    s2)         -> (Term -> Term -> m ()) -> m ()
    withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Term
    u Term
    v -> do
          m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Term -> Term -> m Bool
    forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
    trivial Term
    u Term
    v) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Type -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Term -> Term -> m ()
    giveUp Comparison
    CmpLeq Type
    size Term
    u Term
    v
        (Comparison
    CmpEq, DeepSizeView
    s1, DeepSizeView
    s2) -> Comparison -> m ()
    continue Comparison
    cmp

    -- | If 'envAssignMetas' then postpone as constraint, otherwise, fail hard.
    --   Failing is required if we speculatively test several alternatives.
    giveUp :: (MonadConversion m) => Comparison -> Type -> Term -> Term -> m ()
    giveUp :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Term -> Term -> m ()
    giveUp Comparison
    cmp Type
    size Term
    u Term
    v =
      m Bool -> m () -> m () -> m ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas)
        {-then-} (do
          -- TODO: compute proper blocker
          unblock <- [Term] -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn ([Term] -> Blocker) -> m [Term] -> m Blocker
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Term] -> m [Term]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull [Term
    u, Term
    v]
          addConstraint unblock $ ValueCmp CmpLeq AsSizes u v)
        {-else-} (TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Term -> Term -> CompareAs -> TypeError
    UnequalTerms Comparison
    cmp Term
    u Term
    v CompareAs
    AsSizes)

    -- | Checked whether a size constraint is trivial (like @X <= X+1@).
    trivial :: (MonadConversion m) => Term -> Term -> m Bool
    trivial :: forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
    trivial Term
    u Term
    v = do
        a@(e , n ) <- Term -> m (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    u
        b@(e', n') <- oldSizeExpr v
        let triv = OldSizeExpr
    e OldSizeExpr -> OldSizeExpr -> Bool
    forall a. Eq a => a -> a -> Bool
    == OldSizeExpr
    e' Bool -> Bool -> Bool
    && Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    n'
              -- Andreas, 2012-02-24  filtering out more trivial constraints fixes
              -- test/lib-succeed/SizeInconsistentMeta4.agda
        reportSDoc "tc.conv.size" 60 $
          nest 2 $ sep [ if triv then "trivial constraint" else empty
                       , pretty a <+> "<="
                       , pretty b
                       ]
        return triv
      m Bool -> (TCErr -> m Bool) -> m Bool
    forall a. m a -> (TCErr -> m a) -> m a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    ------------------------------------------------------------------------
    -- * Size constraints.
    ------------------------------------------------------------------------

    -- | Test whether a problem consists only of size constraints.
    isSizeProblem :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool
    isSizeProblem :: forall (m :: * -> *).
    (ReadTCState m, HasOptions m, HasBuiltins m) =>
    ProblemId -> m Bool
    isSizeProblem ProblemId
    pid = do
      test <- m (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      all (mkIsSizeConstraint test (const True) . theConstraint) <$> getConstraintsForProblem pid

    -- | Test whether a constraint speaks about sizes.
    isSizeConstraint :: (HasOptions m, HasBuiltins m) => (Comparison -> Bool) -> Closure Constraint -> m Bool
    isSizeConstraint :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    (Comparison -> Bool) -> Closure Constraint -> m Bool
    isSizeConstraint Comparison -> Bool
    p Closure Constraint
    c = m (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest m (Term -> Maybe BoundedSize)
    -> ((Term -> Maybe BoundedSize) -> Bool) -> m Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Term -> Maybe BoundedSize
    test -> (Term -> Maybe BoundedSize)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    mkIsSizeConstraint Term -> Maybe BoundedSize
    test Comparison -> Bool
    p Closure Constraint
    c

    mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool
    mkIsSizeConstraint :: (Term -> Maybe BoundedSize)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    mkIsSizeConstraint Term -> Maybe BoundedSize
    test = (Type -> Bool)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    isSizeConstraint_ ((Type -> Bool)
     -> (Comparison -> Bool) -> Closure Constraint -> Bool)
    -> (Type -> Bool)
    -> (Comparison -> Bool)
    -> Closure Constraint
    -> Bool
    forall a b. (a -> b) -> a -> b
    $ Maybe BoundedSize -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe BoundedSize -> Bool)
    -> (Type -> Maybe BoundedSize) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe BoundedSize
    test (Term -> Maybe BoundedSize)
    -> (Type -> Term) -> Type -> Maybe BoundedSize
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Term
    forall t a. Type'' t a -> a
    unEl

    isSizeConstraint_
      :: (Type -> Bool)       -- ^ Test for being a sized type
      -> (Comparison -> Bool) -- ^ Restriction to these directions.
      -> Closure Constraint
      -> Bool
    isSizeConstraint_ :: (Type -> Bool)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    isSizeConstraint_ Type -> Bool
    _isSizeType Comparison -> Bool
    p Closure{ clValue :: forall a. Closure a -> a
    clValue = ValueCmp Comparison
    cmp CompareAs
    AsSizes       Term
    _ Term
    _ } = Comparison -> Bool
    p Comparison
    cmp
    isSizeConstraint_  Type -> Bool
    isSizeType Comparison -> Bool
    p Closure{ clValue :: forall a. Closure a -> a
    clValue = ValueCmp Comparison
    cmp (AsTermsOf Type
    s) Term
    _ Term
    _ } = Comparison -> Bool
    p Comparison
    cmp Bool -> Bool -> Bool
    && Type -> Bool
    isSizeType Type
    s
    isSizeConstraint_ Type -> Bool
    _isSizeType Comparison -> Bool
    _ Closure Constraint
    _ = Bool
    False

    -- | Take out all size constraints of the given direction (DANGER!).
    takeSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
    takeSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
    takeSizeConstraints Comparison -> Bool
    p = do
      test <- TCMT IO (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      takeConstraints (mkIsSizeConstraint test p . theConstraint)

    -- | Find the size constraints of the matching direction.
    getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
    getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
    getSizeConstraints Comparison -> Bool
    p = do
      test <- TCMT IO (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      filter (mkIsSizeConstraint test p . theConstraint) <$> getAllConstraints

    -- | Return a list of size metas and their context.
    getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
    getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
    getSizeMetas Bool
    interactionMetas = do
      test <- TCMT IO (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      catMaybes <$> do
        getOpenMetas >>= do
          mapM $ \ MetaId
    m -> do
            let no :: TCMT IO (Maybe a)
    no = Maybe a -> TCMT IO (Maybe a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
            mi <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
            case mvJudgement mi of
              Judgement MetaId
    _ | BlockedConst{} <- MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mi -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall {a}. TCMT IO (Maybe a)
    no  -- Blocked terms should not be touched (#2637, #2881)
              HasType MetaId
    _ Comparison
    cmp Type
    a -> do
                TelV tel b <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
                -- b is reduced
                caseMaybe (test $ unEl b) no $ \ BoundedSize
    _ -> do
                  let yes :: TCMT IO (Maybe (MetaId, Type, Telescope))
    yes = Maybe (MetaId, Type, Telescope)
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (MetaId, Type, Telescope)
     -> TCMT IO (Maybe (MetaId, Type, Telescope)))
    -> Maybe (MetaId, Type, Telescope)
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall a b. (a -> b) -> a -> b
    $ (MetaId, Type, Telescope) -> Maybe (MetaId, Type, Telescope)
    forall a. a -> Maybe a
    Just (MetaId
    m, Type
    a, Telescope
    tel)
                  if Bool
    interactionMetas then TCMT IO (Maybe (MetaId, Type, Telescope))
    yes else do
                    TCMT IO Bool
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Maybe InteractionId -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe InteractionId -> Bool)
    -> TCMT IO (Maybe InteractionId) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO (Maybe InteractionId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe InteractionId)
    isInteractionMeta MetaId
    m) TCMT IO (Maybe (MetaId, Type, Telescope))
    forall {a}. TCMT IO (Maybe a)
    no TCMT IO (Maybe (MetaId, Type, Telescope))
    yes
              Judgement MetaId
    _ -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall {a}. TCMT IO (Maybe a)
    no

    {- ROLLED BACK
    getSizeMetas :: TCM ([(MetaId, Int)], [SizeConstraint])
    getSizeMetas = do
      ms <- getOpenMetas
      test <- isSizeTypeTest
      let sizeCon m = do
            let nothing  = return ([], [])
            mi <- lookupMeta m
            case mvJudgement mi of
              HasType _ a -> do
                TelV tel b <- telView =<< instantiateFull a
                let noConstr = return ([(m, size tel)], [])
                case test b of
                  Nothing            -> nothing
                  Just BoundedNo     -> noConstr
                  Just (BoundedLt u) -> noConstr
    {- WORKS NOT
                  Just (BoundedLt u) -> flip catchError (const $ noConstr) $ do
                    -- we assume the metavariable is used in an
                    -- extension of its creation context
                    ctxIds <- getContextId
                    let a = SizeMeta m $ take (size tel) $ reverse ctxIds
                    (b, n) <- oldSizeExpr u
                    return ([(m, size tel)], [Leq a (n-1) b])
    -}
              _ -> nothing
      (mss, css) <- unzip <$> mapM sizeCon ms
      return (concat mss, concat css)
    -}

    ------------------------------------------------------------------------
    -- * Size constraint solving.
    ------------------------------------------------------------------------

    -- | Atomic size expressions.
    data OldSizeExpr
      = SizeMeta MetaId [Int] -- ^ A size meta applied to de Bruijn indices.
      | Rigid Int             -- ^ A de Bruijn index.
      deriving (OldSizeExpr -> OldSizeExpr -> Bool
    (OldSizeExpr -> OldSizeExpr -> Bool)
    -> (OldSizeExpr -> OldSizeExpr -> Bool) -> Eq OldSizeExpr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: OldSizeExpr -> OldSizeExpr -> Bool
    == :: OldSizeExpr -> OldSizeExpr -> Bool
    $c/= :: OldSizeExpr -> OldSizeExpr -> Bool
    /= :: OldSizeExpr -> OldSizeExpr -> Bool
    Eq, Int -> OldSizeExpr -> [Char] -> [Char]
    [OldSizeExpr] -> [Char] -> [Char]
    OldSizeExpr -> [Char]
    (Int -> OldSizeExpr -> [Char] -> [Char])
    -> (OldSizeExpr -> [Char])
    -> ([OldSizeExpr] -> [Char] -> [Char])
    -> Show OldSizeExpr
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> OldSizeExpr -> [Char] -> [Char]
    showsPrec :: Int -> OldSizeExpr -> [Char] -> [Char]
    $cshow :: OldSizeExpr -> [Char]
    show :: OldSizeExpr -> [Char]
    $cshowList :: [OldSizeExpr] -> [Char] -> [Char]
    showList :: [OldSizeExpr] -> [Char] -> [Char]
    Show)

    instance Pretty OldSizeExpr where
      pretty :: OldSizeExpr -> Doc
    pretty (SizeMeta MetaId
    m [Int]
    _) = [Char] -> Doc
    forall a. [Char] -> Doc a
    P.text [Char]
    "X" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> MetaId -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty MetaId
    m
      pretty (Rigid Int
    i)      = [Char] -> Doc
    forall a. [Char] -> Doc a
    P.text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "c" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i

    -- | Size constraints we can solve.
    data OldSizeConstraint
      = Leq OldSizeExpr Int OldSizeExpr
        -- ^ @Leq a +n b@ represents @a =< b + n@.
        --   @Leq a -n b@ represents @a + n =< b@.
      deriving (Int -> OldSizeConstraint -> [Char] -> [Char]
    [OldSizeConstraint] -> [Char] -> [Char]
    OldSizeConstraint -> [Char]
    (Int -> OldSizeConstraint -> [Char] -> [Char])
    -> (OldSizeConstraint -> [Char])
    -> ([OldSizeConstraint] -> [Char] -> [Char])
    -> Show OldSizeConstraint
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> OldSizeConstraint -> [Char] -> [Char]
    showsPrec :: Int -> OldSizeConstraint -> [Char] -> [Char]
    $cshow :: OldSizeConstraint -> [Char]
    show :: OldSizeConstraint -> [Char]
    $cshowList :: [OldSizeConstraint] -> [Char] -> [Char]
    showList :: [OldSizeConstraint] -> [Char] -> [Char]
    Show)

    instance Pretty OldSizeConstraint where
      pretty :: OldSizeConstraint -> Doc
    pretty (Leq OldSizeExpr
    a Int
    n OldSizeExpr
    b)
        | Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0    = OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    a Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    "=<" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    b
        | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0     = OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    a Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    "=<" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    b Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    "+" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> [Char] -> Doc
    forall a. [Char] -> Doc a
    P.text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)
        | Bool
    otherwise = OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    a Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    "+" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> [Char] -> Doc
    forall a. [Char] -> Doc a
    P.text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show (-Int
    n)) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    "=<" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    b

    -- | Compute a set of size constraints that all live in the same context
    --   from constraints over terms of type size that may live in different
    --   contexts.
    --
    --   cf. 'Agda.TypeChecking.LevelConstraints.simplifyLevelConstraint'
    oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint]
    oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint]
    oldComputeSizeConstraints [] = [OldSizeConstraint] -> TCM [OldSizeConstraint]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] -- special case to avoid maximum []
    oldComputeSizeConstraints [ProblemConstraint]
    cs = [Maybe OldSizeConstraint] -> [OldSizeConstraint]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe OldSizeConstraint] -> [OldSizeConstraint])
    -> TCMT IO [Maybe OldSizeConstraint] -> TCM [OldSizeConstraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Constraint -> TCMT IO (Maybe OldSizeConstraint))
    -> [Constraint] -> TCMT IO [Maybe OldSizeConstraint]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Constraint -> TCMT IO (Maybe OldSizeConstraint)
    oldComputeSizeConstraint [Constraint]
    leqs
      where
        -- get the constraints plus contexts they are defined in
        gammas :: [Context]
    gammas       = (ProblemConstraint -> Context) -> [ProblemConstraint] -> [Context]
    forall a b. (a -> b) -> [a] -> [b]
    map (TCEnv -> Context
    envContext (TCEnv -> Context)
    -> (ProblemConstraint -> TCEnv) -> ProblemConstraint -> Context
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv (Closure Constraint -> TCEnv)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint) [ProblemConstraint]
    cs
        ls :: [Constraint]
    ls           = (ProblemConstraint -> Constraint)
    -> [ProblemConstraint] -> [Constraint]
    forall a b. (a -> b) -> [a] -> [b]
    map (Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (Closure Constraint -> Constraint)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Constraint
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint) [ProblemConstraint]
    cs
        -- compute the longest context (common water level)
        ns :: [Int]
    ns           = (Context -> Int) -> [Context] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Context -> Int
    forall a. Sized a => a -> Int
    size [Context]
    gammas
        waterLevel :: Int
    waterLevel   = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Int]
    ns
        -- lift all constraints to live in the longest context
        -- (assuming this context is an extension of the shorter ones)
        -- by raising the de Bruijn indices
        leqs :: [Constraint]
    leqs = (Int -> Constraint -> Constraint)
    -> [Int] -> [Constraint] -> [Constraint]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> Constraint -> Constraint
    forall a. Subst a => Int -> a -> a
    raise ((Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int
    waterLevel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -) [Int]
    ns) [Constraint]
    ls

    -- | Turn a constraint over de Bruijn indices into a size constraint.
    oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
    oldComputeSizeConstraint :: Constraint -> TCMT IO (Maybe OldSizeConstraint)
    oldComputeSizeConstraint Constraint
    c =
      case Constraint
    c of
        ValueCmp Comparison
    CmpLeq CompareAs
    _ Term
    u Term
    v -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    50 (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
    sep
              [ TCMT IO Doc
    "converting size constraint"
              , Constraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
    prettyTCM Constraint
    c
              ]
            (a, n) <- Term -> TCMT IO (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    u
            (b, m) <- oldSizeExpr v
            return $ Just $ Leq a (m - n) b
          TCMT IO (Maybe OldSizeConstraint)
    -> (TCErr -> TCMT IO (Maybe OldSizeConstraint))
    -> TCMT IO (Maybe OldSizeConstraint)
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    err -> case TCErr
    err of
            PatternErr{} -> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe OldSizeConstraint
    forall a. Maybe a
    Nothing
            TCErr
    _            -> TCErr -> TCMT IO (Maybe OldSizeConstraint)
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
        Constraint
    _ -> TCMT IO (Maybe OldSizeConstraint)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Turn a term with de Bruijn indices into a size expression with offset.
    --
    --   Throws a 'patternViolation' if the term isn't a proper size expression.
    oldSizeExpr :: (PureTCM m, MonadBlock m) => Term -> m (OldSizeExpr, Int)
    oldSizeExpr :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    u = do
      u <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u -- Andreas, 2009-02-09.
                    -- This is necessary to surface the solutions of metavariables.
      reportSDoc "tc.conv.size" 60 $ "oldSizeExpr:" <+> prettyTCM u
      s <- sizeView u
      case s of
        SizeView
    SizeInf     -> Blocker -> m (OldSizeExpr, Int)
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock
        SizeSuc Term
    u   -> (Int -> Int) -> (OldSizeExpr, Int) -> (OldSizeExpr, Int)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) ((OldSizeExpr, Int) -> (OldSizeExpr, Int))
    -> m (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    u
        OtherSize Term
    u -> case Term
    u of
          Var Int
    i []  -> (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> OldSizeExpr
    Rigid Int
    i, Int
    0)
          MetaV MetaId
    m [Elim]
    es | Just [Int]
    xs <- (Elim -> Maybe Int) -> [Elim] -> Maybe [Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> Maybe Int
    isVar [Elim]
    es, [Int] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct [Int]
    xs
                    -> (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaId -> [Int] -> OldSizeExpr
    SizeMeta MetaId
    m [Int]
    xs, Int
    0)
          Term
    _ -> Blocker -> m (OldSizeExpr, Int)
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock
      where
        isVar :: Elim -> Maybe Int
    isVar (Proj{})  = Maybe Int
    forall a. Maybe a
    Nothing
        isVar (IApply Term
    _ Term
    _ Term
    v) = Elim -> Maybe Int
    isVar (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    v))
        isVar (Apply Arg Term
    v) = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v of
          Var Int
    i [] -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i
          Term
    _        -> Maybe Int
    forall a. Maybe a
    Nothing

    -- | Compute list of size metavariables with their arguments
    --   appearing in a constraint.
    flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
    flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
    flexibleVariables (Leq OldSizeExpr
    a Int
    _ OldSizeExpr
    b) = OldSizeExpr -> [(MetaId, [Int])]
    flex OldSizeExpr
    a [(MetaId, [Int])] -> [(MetaId, [Int])] -> [(MetaId, [Int])]
    forall a. [a] -> [a] -> [a]
    ++ OldSizeExpr -> [(MetaId, [Int])]
    flex OldSizeExpr
    b
      where
        flex :: OldSizeExpr -> [(MetaId, [Int])]
    flex (Rigid Int
    _)       = []
        flex (SizeMeta MetaId
    m [Int]
    xs) = [(MetaId
    m, [Int]
    xs)]

    -- | Convert size constraint into form where each meta is applied
    --   to indices @0,1,..,n-1@ where @n@ is the arity of that meta.
    --
    --   @X[σ] <= t@ becomes @X[id] <= t[σ^-1]@
    --
    --   @X[σ] ≤ Y[τ]@ becomes @X[id] ≤ Y[τ[σ^-1]]@ or @X[σ[τ^1]] ≤ Y[id]@
    --   whichever is defined.  If none is defined, we give up.
    --
    oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
    oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
    oldCanonicalizeSizeConstraint c :: OldSizeConstraint
    c@(Leq OldSizeExpr
    a Int
    n OldSizeExpr
    b) =
      case (OldSizeExpr
    a,OldSizeExpr
    b) of
        (Rigid{}, Rigid{})       -> OldSizeConstraint -> Maybe OldSizeConstraint
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return OldSizeConstraint
    c
        (SizeMeta MetaId
    m [Int]
    xs, Rigid Int
    i) -> do
          j <- Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    i [Int]
    xs
          return $ Leq (SizeMeta m [0..size xs-1]) n (Rigid j)
        (Rigid Int
    i, SizeMeta MetaId
    m [Int]
    xs) -> do
          j <- Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    i [Int]
    xs
          return $ Leq (Rigid j) n (SizeMeta m [0..size xs-1])
        (SizeMeta MetaId
    m [Int]
    xs, SizeMeta MetaId
    l [Int]
    ys)
             -- try to invert xs on ys
           | Just [Int]
    ys' <- (Int -> Maybe Int) -> [Int] -> Maybe [Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\ Int
    y -> Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    y [Int]
    xs) [Int]
    ys ->
               OldSizeConstraint -> Maybe OldSizeConstraint
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OldSizeConstraint -> Maybe OldSizeConstraint)
    -> OldSizeConstraint -> Maybe OldSizeConstraint
    forall a b. (a -> b) -> a -> b
    $ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
    Leq (MetaId -> [Int] -> OldSizeExpr
    SizeMeta MetaId
    m [Int
    0..[Int] -> Int
    forall a. Sized a => a -> Int
    size [Int]
    xsInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1]) Int
    n (MetaId -> [Int] -> OldSizeExpr
    SizeMeta MetaId
    l [Int]
    ys')
             -- try to invert ys on xs
           | Just [Int]
    xs' <- (Int -> Maybe Int) -> [Int] -> Maybe [Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\ Int
    x -> Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    x [Int]
    ys) [Int]
    xs ->
               OldSizeConstraint -> Maybe OldSizeConstraint
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OldSizeConstraint -> Maybe OldSizeConstraint)
    -> OldSizeConstraint -> Maybe OldSizeConstraint
    forall a b. (a -> b) -> a -> b
    $ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
    Leq (MetaId -> [Int] -> OldSizeExpr
    SizeMeta MetaId
    m [Int]
    xs') Int
    n (MetaId -> [Int] -> OldSizeExpr
    SizeMeta MetaId
    l [Int
    0..[Int] -> Int
    forall a. Sized a => a -> Int
    size [Int]
    ysInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1])
             -- give up
           | Bool
    otherwise -> Maybe OldSizeConstraint
    forall a. Maybe a
    Nothing