    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.SizedTypes where

    import Prelude hiding (null)

    import Control.Monad
    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 Data.List.NonEmpty (NonEmpty(..))
    import qualified Data.Map as Map
    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.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Pretty.Constraint
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
    import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (MonadCheckInternal, infer)
    import {-# SOURCE #-} Agda.TypeChecking.Conversion
    import {-# SOURCE #-} Agda.TypeChecking.Constraints

    import Agda.Utils.Functor
    import Agda.Utils.List as List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (Pretty, prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import qualified Agda.Utils.Pretty as P
    import qualified Agda.Utils.Warshall as W

    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
        Telescope
    tel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "checking that " 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
    prettyTCM Term
    t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " is not an empty type of sizes"
          , if Telescope -> Bool
    forall a. Null a => a -> Bool
    null Telescope
    tel then TCMT IO Doc
    forall a. Null a => a
    empty else do
            TCMT IO Doc
    "in context " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    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
    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)
    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
    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 ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
                      TCMT IO Doc
    "Possibly empty type of sizes " 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
    prettyTCM 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
      SizeView
    v <- Term -> TCMT IO SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    u
      case SizeView
    v of
        SizeView
    SizeInf     -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True  -- OK, infty is never 0.
        SizeSuc{}   -> Bool -> TCMT IO Bool
    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 (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
    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.
      [Type]
    ts <- (Dom' Term (Name, Type) -> Type) -> Context -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Type
    forall a b. (a, b) -> b
    snd ((Name, Type) -> Type)
    -> (Dom' Term (Name, Type) -> (Name, Type))
    -> Dom' Term (Name, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) (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.
      (Int
    n, Set Blocker
    blockers) <- WriterT (Set Blocker) (TCMT IO) Int -> TCM (Int, Set Blocker)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (WriterT (Set Blocker) (TCMT IO) Int -> TCM (Int, Set Blocker))
    -> WriterT (Set Blocker) (TCMT IO) Int -> TCM (Int, Set Blocker)
    forall a b. (a -> b) -> a -> b
    $ [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
    minSizeValAux [Type]
    ts ([Int] -> WriterT (Set Blocker) (TCMT IO) Int)
    -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. a -> [a]
    repeat Int
    0
      let blocker :: Blocker
    blocker = Set Blocker -> Blocker
    unblockOnAll Set Blocker
    blockers
      if Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 then Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True else
        if Blocker
    blocker Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    alwaysUnblock
          then Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          else Blocker -> TCMT IO Bool
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    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 (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 (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 (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 (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)
    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
                DeepSizeView
    v <- TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView
    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 DeepSizeView
    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
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1Int -> 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 (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 :: * -> *).
    (Applicative m, MonadFail 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Def QName
    x [Apply Arg Term
    u] -> do
          Maybe Term
    sizelt <- [Char] -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
    getBuiltin' [Char]
    builtinSizeLt
          BoundedSize -> m BoundedSize
    forall (m :: * -> *) a. Monad m => a -> m a
    return (BoundedSize -> m BoundedSize) -> BoundedSize -> m BoundedSize
    forall a b. (a -> b) -> a -> b
    $ if (Term -> Maybe Term
    forall a. a -> Maybe a
    Just (QName -> [Elim] -> Term
    Def QName
    x []) Maybe Term -> Maybe Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe Term
    sizelt) then Term -> BoundedSize
    BoundedLt (Term -> BoundedSize) -> Term -> BoundedSize
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u else BoundedSize
    BoundedNo
        Term
    _ -> BoundedSize -> m BoundedSize
    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
      Maybe BoundedSize
    res <- Type -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Type
    a
      case Maybe BoundedSize
    res of
        Just (BoundedLt Term
    u) -> do
          Int
    n <- m Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize
          let tel :: Telescope
    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
          Telescope -> m () -> m ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
            Term
    v <- Int -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
    sizeSuc Int
    1 (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Telescope -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    tel
            -- compareSizes CmpLeq v u
            Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint (MetaId -> Blocker
    unblockOnMeta MetaId
    x) (Constraint -> m ()) -> Constraint -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> CompareAs -> Term -> Term -> Constraint
    ValueCmp Comparison
    CmpLeq CompareAs
    AsSizes Term
    v Term
    u
        Maybe BoundedSize
    _ -> () -> m ()
    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.
      (QName
    size, QName
    sizelt) <- (m (QName, QName)
     -> (TCErr -> m (QName, QName)) -> m (QName, QName))
    -> (TCErr -> m (QName, QName))
    -> m (QName, QName)
    -> m (QName, QName)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip m (QName, QName) -> (TCErr -> m (QName, QName)) -> m (QName, QName)
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError (m (QName, QName) -> TCErr -> m (QName, QName)
    forall a b. a -> b -> a
    const m (QName, QName)
    forall (m :: * -> *) a. MonadTCError m => m a
    failure) (m (QName, QName) -> m (QName, QName))
    -> m (QName, QName) -> m (QName, QName)
    forall a b. (a -> b) -> a -> b
    $ do
         Def QName
    size   [Elim]
    _ <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSize
         Def QName
    sizelt [Elim]
    _ <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeLt
         (QName, QName) -> m (QName, QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    size, QName
    sizelt)
      case (Comparison
    cmp, [Elim]
    els1, [Elim]
    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 (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
      Def QName
    inf [] <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
      Def QName
    suc [] <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeSuc
      let loop :: Term -> m DeepSizeView
    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 (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 (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)
    mapM Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim [Elim]
    es
                                         -> DeepSizeView -> m DeepSizeView
    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 (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 (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
      Term -> m DeepSizeView
    loop Term
    v

    sizeMaxView :: PureTCM m => Term -> m SizeMaxView
    sizeMaxView :: forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
    sizeMaxView Term
    v = do
      Maybe QName
    inf <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinDefName [Char]
    builtinSizeInf
      Maybe QName
    suc <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinDefName [Char]
    builtinSizeSuc
      Maybe QName
    max <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinDefName [Char]
    builtinSizeMax
      let loop :: Term -> m SizeMaxView
    loop Term
    v = do
            Term
    v <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
            case Term
    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 (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 (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)
    mapM Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim [Elim]
    es
                                            -> SizeMaxView -> m SizeMaxView
    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 (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 (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
      Term -> m SizeMaxView
    loop Term
    v

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

    -- | 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 (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
    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
    prettyTCM Comparison
    cmp
                       , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
        Term
    u <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
        Term
    v <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
        [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
          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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty 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
    prettyTCM Comparison
    cmp
                       , Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v
                       ]
      SizeMaxView
    us <- Term -> m SizeMaxView
    forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
    sizeMaxView Term
    u
      SizeMaxView
    vs <- Term -> m SizeMaxView
    forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
    sizeMaxView Term
    v
      Comparison -> SizeMaxView -> SizeMaxView -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> SizeMaxView -> SizeMaxView -> m ()
    compareMaxViews Comparison
    cmp SizeMaxView
    us SizeMaxView
    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 (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 (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 (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 (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"
          ]
        Term
    u <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    u
        Term
    v <- SizeMaxView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    SizeMaxView -> m Term
    unMaxView SizeMaxView
    vs
        Type
    size <- m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType
        Comparison -> Type -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Term -> Term -> m ()
    giveUp Comparison
    CmpLeq Type
    size Term
    u Term
    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 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'
        ]
      Type
    size <- m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType
      let (DeepSizeView
    s1, DeepSizeView
    s2) = (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
    removeSucs (DeepSizeView
    s1', DeepSizeView
    s2')
          withUnView :: (Term -> Term -> m ()) -> m ()
    withUnView Term -> Term -> m ()
    cont = do
            Term
    u <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    s1
            Term
    v <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    s2
            Term -> Term -> m ()
    cont Term
    u Term
    v
          failure :: m ()
    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 -> m ()
    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 (Comparison
    cmp, DeepSizeView
    s1, DeepSizeView
    s2) of
        (Comparison
    CmpLeq, DeepSizeView
    _,            DeepSizeView
    DSizeInf)   -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        (Comparison
    CmpEq,  DeepSizeView
    DSizeInf,     DeepSizeView
    DSizeInf)   -> () -> m ()
    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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
           BoundedSize
    res <- ProjectedVar -> m BoundedSize
    forall (m :: * -> *).
    (MonadCheckInternal m, PureTCM m) =>
    ProjectedVar -> m BoundedSize
    isBoundedProjVar ProjectedVar
    i
           case BoundedSize
    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
                Term
    v <- DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView DeepSizeView
    s2
                if Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 then do
                  Term
    u'' <- Int -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
    sizeSuc (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Term
    u'
                  Comparison -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Term -> Term -> m ()
    compareSizes Comparison
    cmp Term
    u'' Term
    v
                 else Comparison -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Term -> Term -> m ()
    compareSizes Comparison
    cmp Term
    u' (Term -> m ()) -> m Term -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
    sizeSuc Int
    1 Term
    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-} (Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    unblock (Constraint -> m ()) -> Constraint -> m ()
    forall a b. (a -> b) -> a -> b
    $ Comparison -> CompareAs -> Term -> Term -> Constraint
    ValueCmp Comparison
    CmpLeq CompareAs
    AsSizes Term
    u Term
    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)
      where
        unblock :: Blocker
    unblock = [Term] -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn [Term
    u, Term
    v]

    -- | 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 :: (OldSizeExpr, Int)
    a@(OldSizeExpr
    e , Int
    n ) <- Term -> m (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    u
        b :: (OldSizeExpr, Int)
    b@(OldSizeExpr
    e', Int
    n') <- Term -> m (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    v
        let triv :: Bool
    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
        [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
          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 [ if Bool
    triv then TCMT IO Doc
    "trivial constraint" else TCMT IO Doc
    forall a. Null a => a
    empty
                       , (OldSizeExpr, Int) -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (OldSizeExpr, Int)
    a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "<="
                       , (OldSizeExpr, Int) -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (OldSizeExpr, Int)
    b
                       ]
        Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    triv
      m Bool -> (TCErr -> m Bool) -> m Bool
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ -> Bool -> m Bool
    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
      Term -> Maybe BoundedSize
    test <- m (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      (ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Term -> Maybe BoundedSize)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    mkIsSizeConstraint Term -> Maybe BoundedSize
    test (Bool -> Comparison -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (Closure Constraint -> Bool)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint) ([ProblemConstraint] -> Bool) -> m [ProblemConstraint] -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProblemId -> m [ProblemConstraint]
    forall (m :: * -> *).
    ReadTCState m =>
    ProblemId -> m [ProblemConstraint]
    getConstraintsForProblem ProblemId
    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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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
      Term -> Maybe BoundedSize
    test <- TCMT IO (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      (ProblemConstraint -> Bool) -> TCM [ProblemConstraint]
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m [ProblemConstraint]
    takeConstraints ((Term -> Maybe BoundedSize)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    mkIsSizeConstraint Term -> Maybe BoundedSize
    test Comparison -> Bool
    p (Closure Constraint -> Bool)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint)

    -- | Find the size constraints of the matching direction.
    getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
    getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
    getSizeConstraints Comparison -> Bool
    p = do
      Term -> Maybe BoundedSize
    test <- TCMT IO (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      (ProblemConstraint -> Bool)
    -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Term -> Maybe BoundedSize)
    -> (Comparison -> Bool) -> Closure Constraint -> Bool
    mkIsSizeConstraint Term -> Maybe BoundedSize
    test Comparison -> Bool
    p (Closure Constraint -> Bool)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint) ([ProblemConstraint] -> [ProblemConstraint])
    -> TCM [ProblemConstraint] -> TCM [ProblemConstraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM [ProblemConstraint]
    forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    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
      Term -> Maybe BoundedSize
    test <- TCMT IO (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      [Maybe (MetaId, Type, Telescope)] -> [(MetaId, Type, Telescope)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (MetaId, Type, Telescope)] -> [(MetaId, Type, Telescope)])
    -> TCMT IO [Maybe (MetaId, Type, Telescope)]
    -> TCM [(MetaId, Type, Telescope)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas TCMT IO [MetaId]
    -> ([MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)])
    -> TCMT IO [Maybe (MetaId, Type, Telescope)]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= do
          (MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
    -> [MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
     -> [MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)])
    -> (MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
    -> [MetaId]
    -> TCMT IO [Maybe (MetaId, Type, Telescope)]
    forall a b. (a -> b) -> a -> b
    $ \ MetaId
    m -> do
            let no :: TCMT IO (Maybe a)
    no = Maybe a -> TCMT IO (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
            MetaVariable
    mi <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
            case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    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 Telescope
    tel Type
    b <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
                -- b is reduced
                Maybe BoundedSize
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    -> (BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Term -> Maybe BoundedSize
    test (Term -> Maybe BoundedSize) -> Term -> Maybe BoundedSize
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    b) TCMT IO (Maybe (MetaId, Type, Telescope))
    forall {a}. TCMT IO (Maybe a)
    no ((BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
     -> TCMT IO (Maybe (MetaId, Type, Telescope)))
    -> (BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    forall a b. (a -> b) -> a -> b
    $ \ BoundedSize
    _ -> do
                  let yes :: TCMT IO (Maybe (MetaId, Type, Telescope))
    yes = Maybe (MetaId, Type, Telescope)
    -> TCMT IO (Maybe (MetaId, Type, Telescope))
    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
    /= :: OldSizeExpr -> OldSizeExpr -> Bool
    $c/= :: OldSizeExpr -> OldSizeExpr -> Bool
    == :: OldSizeExpr -> OldSizeExpr -> Bool
    $c== :: 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
    showList :: [OldSizeExpr] -> [Char] -> [Char]
    $cshowList :: [OldSizeExpr] -> [Char] -> [Char]
    show :: OldSizeExpr -> [Char]
    $cshow :: OldSizeExpr -> [Char]
    showsPrec :: Int -> OldSizeExpr -> [Char] -> [Char]
    $cshowsPrec :: Int -> OldSizeExpr -> [Char] -> [Char]
    Show)

    instance Pretty OldSizeExpr where
      pretty :: OldSizeExpr -> Doc
    pretty (SizeMeta MetaId
    m [Int]
    _) = [Char] -> Doc
    P.text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "X" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show (MetaId -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral MetaId
    m :: Int)
      pretty (Rigid Int
    i)      = [Char] -> Doc
    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
    showList :: [OldSizeConstraint] -> [Char] -> [Char]
    $cshowList :: [OldSizeConstraint] -> [Char] -> [Char]
    show :: OldSizeConstraint -> [Char]
    $cshow :: OldSizeConstraint -> [Char]
    showsPrec :: Int -> OldSizeConstraint -> [Char] -> [Char]
    $cshowsPrec :: Int -> 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
    P.<+> Doc
    "=<" Doc -> Doc -> Doc
    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
    P.<+> Doc
    "=<" Doc -> Doc -> Doc
    P.<+> OldSizeExpr -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OldSizeExpr
    b Doc -> Doc -> Doc
    P.<+> Doc
    "+" Doc -> Doc -> Doc
    P.<+> [Char] -> Doc
    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
    P.<+> Doc
    "+" Doc -> Doc -> Doc
    P.<+> [Char] -> Doc
    P.text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show (-Int
    n)) Doc -> Doc -> Doc
    P.<+> Doc
    "=<" Doc -> Doc -> Doc
    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 (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)
    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 (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
    prettyTCM Constraint
    c
              ]
            (OldSizeExpr
    a, Int
    n) <- Term -> TCMT IO (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    u
            (OldSizeExpr
    b, Int
    m) <- Term -> TCMT IO (OldSizeExpr, Int)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (OldSizeExpr, Int)
    oldSizeExpr Term
    v
            Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint))
    -> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
    forall a b. (a -> b) -> a -> b
    $ OldSizeConstraint -> Maybe OldSizeConstraint
    forall a. a -> Maybe a
    Just (OldSizeConstraint -> Maybe OldSizeConstraint)
    -> OldSizeConstraint -> Maybe OldSizeConstraint
    forall a b. (a -> b) -> a -> b
    $ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
    Leq OldSizeExpr
    a (Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) OldSizeExpr
    b
          TCMT IO (Maybe OldSizeConstraint)
    -> (TCErr -> TCMT IO (Maybe OldSizeConstraint))
    -> TCMT IO (Maybe OldSizeConstraint)
    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 (m :: * -> *) a. Monad m => a -> m a
    return Maybe OldSizeConstraint
    forall a. Maybe a
    Nothing
            TCErr
    _            -> TCErr -> TCMT IO (Maybe OldSizeConstraint)
    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
      Term
    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.
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "oldSizeExpr:" 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
    prettyTCM Term
    u
      SizeView
    s <- Term -> m SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    u
      case SizeView
    s of
        SizeView
    SizeInf     -> Blocker -> m (OldSizeExpr, Int)
    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 (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)
    mapM Elim -> Maybe Int
    isVar [Elim]
    es, [Int] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct [Int]
    xs
                    -> (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return OldSizeConstraint
    c
        (SizeMeta MetaId
    m [Int]
    xs, Rigid Int
    i) -> do
          Int
    j <- Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    i [Int]
    xs
          OldSizeConstraint -> Maybe OldSizeConstraint
    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 (Int -> OldSizeExpr
    Rigid Int
    j)
        (Rigid Int
    i, SizeMeta MetaId
    m [Int]
    xs) -> do
          Int
    j <- Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    i [Int]
    xs
          OldSizeConstraint -> Maybe OldSizeConstraint
    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 (Int -> OldSizeExpr
    Rigid Int
    j) Int
    n (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])
        (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)
    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 (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)
    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 (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

    -- | Main function.
    --   Uses the old solver for size constraints using "Agda.Utils.Warshall".
    --   This solver does not smartly use size hypotheses @j : Size< i@.
    --   It only checks that its computed solution is compatible
    oldSolveSizeConstraints :: TCM ()
    oldSolveSizeConstraints :: TCM ()
    oldSolveSizeConstraints = TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO Bool
    haveSizedTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.solve" Int
    70 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Considering to solve size constraints"
      [ProblemConstraint]
    cs0 <- (Comparison -> Bool) -> TCM [ProblemConstraint]
    getSizeConstraints (Comparison -> Comparison -> Bool
    forall a. Eq a => a -> a -> Bool
    == Comparison
    CmpLeq)
      [OldSizeConstraint]
    cs <- [ProblemConstraint] -> TCM [OldSizeConstraint]
    oldComputeSizeConstraints [ProblemConstraint]
    cs0
      [(MetaId, Type, Telescope)]
    ms <- Bool -> TCM [(MetaId, Type, Telescope)]
    getSizeMetas Bool
    True -- get all size metas, also interaction metas

      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool -> Bool
    not ([OldSizeConstraint] -> Bool
    forall a. Null a => a -> Bool
    null [OldSizeConstraint]
    cs) Bool -> Bool -> Bool
    || Bool -> Bool
    not ([(MetaId, Type, Telescope)] -> Bool
    forall a. Null a => a -> Bool
    null [(MetaId, Type, Telescope)]
    ms)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.solve" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Solving size constraints " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [OldSizeConstraint] -> [Char]
    forall a. Show a => a -> [Char]
    show [OldSizeConstraint]
    cs

        [OldSizeConstraint]
    cs <- [OldSizeConstraint] -> TCM [OldSizeConstraint]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([OldSizeConstraint] -> TCM [OldSizeConstraint])
    -> [OldSizeConstraint] -> TCM [OldSizeConstraint]
    forall a b. (a -> b) -> a -> b
    $ (OldSizeConstraint -> Maybe OldSizeConstraint)
    -> [OldSizeConstraint] -> [OldSizeConstraint]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe OldSizeConstraint -> Maybe OldSizeConstraint
    oldCanonicalizeSizeConstraint [OldSizeConstraint]
    cs
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.solve" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Canonicalized constraints: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [OldSizeConstraint] -> [Char]
    forall a. Show a => a -> [Char]
    show [OldSizeConstraint]
    cs

        let -- Error for giving up
            cannotSolve :: TCM ()
    cannotSolve = TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat (TCMT IO Doc
    "Cannot solve size constraints" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (ProblemConstraint -> TCMT IO Doc)
    -> [ProblemConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [ProblemConstraint]
    cs0)

            -- Size metas in constraints.
            metas0 :: [(MetaId, Int)]  -- meta id + arity
            metas0 :: [(MetaId, Int)]
    metas0 = ((MetaId, Int) -> (MetaId, Int))
    -> [(MetaId, Int)] -> [(MetaId, Int)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    List.nubOn (MetaId, Int) -> (MetaId, Int)
    forall a. a -> a
    id ([(MetaId, Int)] -> [(MetaId, Int)])
    -> [(MetaId, Int)] -> [(MetaId, Int)]
    forall a b. (a -> b) -> a -> b
    $ ((MetaId, [Int]) -> (MetaId, Int))
    -> [(MetaId, [Int])] -> [(MetaId, Int)]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Int] -> Int) -> (MetaId, [Int]) -> (MetaId, Int)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd [Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length) ([(MetaId, [Int])] -> [(MetaId, Int)])
    -> [(MetaId, [Int])] -> [(MetaId, Int)]
    forall a b. (a -> b) -> a -> b
    $ (OldSizeConstraint -> [(MetaId, [Int])])
    -> [OldSizeConstraint] -> [(MetaId, [Int])]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap OldSizeConstraint -> [(MetaId, [Int])]
    flexibleVariables [OldSizeConstraint]
    cs

            -- Unconstrained size metas that do not occur in constraints.
            metas1 :: [(MetaId, Int)]
            metas1 :: [(MetaId, Int)]
    metas1 = [(MetaId, Type, Telescope)]
    -> ((MetaId, Type, Telescope) -> Maybe (MetaId, Int))
    -> [(MetaId, Int)]
    forall a b. [a] -> (a -> Maybe b) -> [b]
    forMaybe [(MetaId, Type, Telescope)]
    ms (((MetaId, Type, Telescope) -> Maybe (MetaId, Int))
     -> [(MetaId, Int)])
    -> ((MetaId, Type, Telescope) -> Maybe (MetaId, Int))
    -> [(MetaId, Int)]
    forall a b. (a -> b) -> a -> b
    $ \ (MetaId
    m, Type
    _, Telescope
    tel) ->
              Maybe (MetaId, Int)
    -> (Int -> Maybe (MetaId, Int)) -> Maybe Int -> Maybe (MetaId, Int)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ((MetaId, Int) -> Maybe (MetaId, Int)
    forall a. a -> Maybe a
    Just (MetaId
    m, Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel)) (Maybe (MetaId, Int) -> Int -> Maybe (MetaId, Int)
    forall a b. a -> b -> a
    const Maybe (MetaId, Int)
    forall a. Maybe a
    Nothing) (Maybe Int -> Maybe (MetaId, Int))
    -> Maybe Int -> Maybe (MetaId, Int)
    forall a b. (a -> b) -> a -> b
    $
                MetaId -> [(MetaId, Int)] -> Maybe Int
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup MetaId
    m [(MetaId, Int)]
    metas0

            -- All size metas
            metas :: [(MetaId, Int)]
    metas = [(MetaId, Int)]
    metas0 [(MetaId, Int)] -> [(MetaId, Int)] -> [(MetaId, Int)]
    forall a. [a] -> [a] -> [a]
    ++ [(MetaId, Int)]
    metas1

        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.solve" Int
    15 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Metas: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(MetaId, Int)] -> [Char]
    forall a. Show a => a -> [Char]
    show [(MetaId, Int)]
    metas0 [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(MetaId, Int)] -> [Char]
    forall a. Show a => a -> [Char]
    show [(MetaId, Int)]
    metas1

        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.size.solve" Int
    20 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            -- debug print the type of all size metas
            [(MetaId, Int)] -> ((MetaId, Int) -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(MetaId, Int)]
    metas (((MetaId, Int) -> TCM ()) -> TCM ())
    -> ((MetaId, Int) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ (MetaId
    m, Int
    _) ->
                [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Judgement MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Judgement MetaId -> TCMT IO Doc)
    -> TCMT IO (Judgement MetaId) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaVariable -> Judgement MetaId
    mvJudgement (MetaVariable -> Judgement MetaId)
    -> TCMT IO MetaVariable -> TCMT IO (Judgement MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m

        -- Run the solver.
        TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM ([(MetaId, Int)] -> [OldSizeConstraint] -> TCMT IO Bool
    oldSolver [(MetaId, Int)]
    metas [OldSizeConstraint]
    cs) TCM ()
    cannotSolve

        -- Double-checking the solution.

        -- Andreas, 2012-09-19
        -- The returned solution might not be consistent with
        -- the hypotheses on rigid vars (j : Size< i).
        -- Thus, we double check that all size constraints
        -- have been solved correctly.
        (TCM () -> (TCErr -> TCM ()) -> TCM ())
    -> (TCErr -> TCM ()) -> TCM () -> TCM ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM () -> (TCErr -> TCM ()) -> TCM ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError (TCM () -> TCErr -> TCM ()
    forall a b. a -> b -> a
    const TCM ()
    cannotSolve) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [ProblemConstraint] -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [ProblemConstraint]
    cs0 ((ProblemConstraint -> TCM ()) -> TCM ())
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Constraint -> TCM ()) -> ProblemConstraint -> TCM ()
    forall (m :: * -> *) a.
    MonadConstraint m =>
    (Constraint -> m a) -> ProblemConstraint -> m a
    withConstraint Constraint -> TCM ()
    forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
    solveConstraint

    -- | Old solver for size constraints using "Agda.Utils.Warshall".
    --   This solver does not smartly use size hypotheses @j : Size< i@.
    oldSolver
      :: [(MetaId, Int)]      -- ^ Size metas and their arity.
      -> [OldSizeConstraint]  -- ^ Size constraints (in preprocessed form).
      -> TCM Bool             -- ^ Returns @False@ if solver fails.
    oldSolver :: [(MetaId, Int)] -> [OldSizeConstraint] -> TCMT IO Bool
    oldSolver [(MetaId, Int)]
    metas [OldSizeConstraint]
    cs = do
      let cannotSolve :: TCMT IO Bool
    cannotSolve    = Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          mkFlex :: (a, a) -> Constraint
    mkFlex (a
    m, a
    ar) = Int -> (Int -> Bool) -> Constraint
    W.NewFlex (a -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    m) ((Int -> Bool) -> Constraint) -> (Int -> Bool) -> Constraint
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i -> Int -> a
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    < a
    ar
          mkConstr :: OldSizeConstraint -> Constraint
    mkConstr (Leq OldSizeExpr
    a Int
    n OldSizeExpr
    b)  = Node -> Int -> Node -> Constraint
    W.Arc (OldSizeExpr -> Node
    mkNode OldSizeExpr
    a) Int
    n (OldSizeExpr -> Node
    mkNode OldSizeExpr
    b)
          mkNode :: OldSizeExpr -> Node
    mkNode (Rigid Int
    i)      = Rigid -> Node
    W.Rigid (Rigid -> Node) -> Rigid -> Node
    forall a b. (a -> b) -> a -> b
    $ Int -> Rigid
    W.RVar Int
    i
          mkNode (SizeMeta MetaId
    m [Int]
    _) = Int -> Node
    W.Flex (Int -> Node) -> Int -> Node
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral MetaId
    m

      -- run the Warshall solver
      case Constraints -> Maybe Solution
    W.solve (Constraints -> Maybe Solution) -> Constraints -> Maybe Solution
    forall a b. (a -> b) -> a -> b
    $ ((MetaId, Int) -> Constraint) -> [(MetaId, Int)] -> Constraints
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId, Int) -> Constraint
    forall {a} {a}. (Integral a, Num a, Ord a) => (a, a) -> Constraint
    mkFlex [(MetaId, Int)]
    metas Constraints -> Constraints -> Constraints
    forall a. [a] -> [a] -> [a]
    ++ (OldSizeConstraint -> Constraint)
    -> [OldSizeConstraint] -> Constraints
    forall a b. (a -> b) -> [a] -> [b]
    map OldSizeConstraint -> Constraint
    mkConstr [OldSizeConstraint]
    cs of
        Maybe Solution
    Nothing  -> TCMT IO Bool
    cannotSolve
        Just Solution
    sol -> do
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.size.solve" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Solved constraints: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Solution -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Solution
    sol
          Term
    suc   <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeSuc
          Term
    infty <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
          let plus :: Term -> Int -> Term
    plus Term
    v Int
    0 = Term
    v
              plus Term
    v Int
    n = Term
    suc Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    `apply1` Term -> Int -> Term
    plus Term
    v (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)

              inst :: (Int, SizeExpr) -> TCM ()
    inst (Int
    i, SizeExpr
    e) = do

                let m :: MetaId
    m  = Int -> MetaId
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i  -- meta variable identifier
                    ar :: Int
    ar = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [(MetaId, Int)] -> Maybe Int
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup MetaId
    m [(MetaId, Int)]
    metas  -- meta var arity

                    term :: SizeExpr -> Term
    term (W.SizeConst Weight
    W.Infinite) = Term
    infty
                    term (W.SizeVar Int
    j Int
    n) | Int
    j Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    ar = Term -> Int -> Term
    plus (Int -> Term
    var (Int -> Term) -> Int -> Term
    forall a b. (a -> b) -> a -> b
    $ Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Int
    n
                    term SizeExpr
    _                        = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

                    tel :: [Arg [Char]]
    tel = Int -> Arg [Char] -> [Arg [Char]]
    forall a. Int -> a -> [a]
    replicate Int
    ar (Arg [Char] -> [Arg [Char]]) -> Arg [Char] -> [Arg [Char]]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Arg [Char]
    forall a. a -> Arg a
    defaultArg [Char]
    "s"
                    -- convert size expression to term
                    v :: Term
    v = SizeExpr -> Term
    term SizeExpr
    e

                [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" 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
                  [ MetaId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":="
                  , 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
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v
                  ]

                -- Andreas, 2012-09-25: do not assign interaction metas to \infty
                let isInf :: SizeExpr -> Bool
    isInf (W.SizeConst Weight
    W.Infinite) = Bool
    True
                    isInf SizeExpr
    _                        = Bool
    False
                TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (((SizeExpr -> Bool
    isInf SizeExpr
    e Bool -> Bool -> Bool
    &&) (Bool -> Bool)
    -> (Maybe InteractionId -> Bool) -> Maybe InteractionId -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . 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 Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  MetaId -> [Arg [Char]] -> Term -> TCM ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    m [Arg [Char]]
    tel Term
    v

          ((Int, SizeExpr) -> TCM ()) -> [(Int, SizeExpr)] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Int, SizeExpr) -> TCM ()
    inst ([(Int, SizeExpr)] -> TCM ()) -> [(Int, SizeExpr)] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Solution -> [(Int, SizeExpr)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Solution
    sol
          Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True