    -- | Stuff for sized types that does not require modules
    --   "Agda.TypeChecking.Reduce" or "Agda.TypeChecking.Constraints"
    --   (which import "Agda.TypeChecking.Monad").

    module Agda.TypeChecking.Monad.SizedTypes where

    import Control.Monad.Except

    import qualified Data.Foldable as Fold
    import Data.List.NonEmpty (NonEmpty(..))
    import qualified Data.List.NonEmpty as NonEmpty
    import qualified Data.Traversable as Trav

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Substitute

    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- * Testing for type 'Size'
    ------------------------------------------------------------------------

    -- | Result of querying whether size variable @i@ is bounded by another
    --   size.
    data BoundedSize
      =  BoundedLt Term -- ^ yes @i : Size< t@
      |  BoundedNo
         deriving (BoundedSize -> BoundedSize -> Bool
    (BoundedSize -> BoundedSize -> Bool)
    -> (BoundedSize -> BoundedSize -> Bool) -> Eq BoundedSize
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: BoundedSize -> BoundedSize -> Bool
    $c/= :: BoundedSize -> BoundedSize -> Bool
    == :: BoundedSize -> BoundedSize -> Bool
    $c== :: BoundedSize -> BoundedSize -> Bool
    Eq, Offset -> BoundedSize -> ShowS
    [BoundedSize] -> ShowS
    BoundedSize -> String
    (Offset -> BoundedSize -> ShowS)
    -> (BoundedSize -> String)
    -> ([BoundedSize] -> ShowS)
    -> Show BoundedSize
    forall a.
    (Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [BoundedSize] -> ShowS
    $cshowList :: [BoundedSize] -> ShowS
    show :: BoundedSize -> String
    $cshow :: BoundedSize -> String
    showsPrec :: Offset -> BoundedSize -> ShowS
    $cshowsPrec :: Offset -> BoundedSize -> ShowS
    Show)

    -- | Check if a type is the 'primSize' type. The argument should be 'reduce'd.
    class IsSizeType a where
      isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)

    instance IsSizeType a => IsSizeType (Dom a) where
      isSizeType :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Dom a -> m (Maybe BoundedSize)
    isSizeType = a -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType (a -> m (Maybe BoundedSize))
    -> (Dom a -> a) -> Dom a -> m (Maybe BoundedSize)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom a -> a
    forall t e. Dom' t e -> e
    unDom

    instance IsSizeType a => IsSizeType (b,a) where
      isSizeType :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    (b, a) -> m (Maybe BoundedSize)
    isSizeType = a -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType (a -> m (Maybe BoundedSize))
    -> ((b, a) -> a) -> (b, a) -> m (Maybe BoundedSize)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b, a) -> a
    forall a b. (a, b) -> b
    snd

    instance IsSizeType a => IsSizeType (Type' a) where
      isSizeType :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Type' a -> m (Maybe BoundedSize)
    isSizeType = a -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType (a -> m (Maybe BoundedSize))
    -> (Type' a -> a) -> Type' a -> m (Maybe BoundedSize)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type' a -> a
    forall t a. Type'' t a -> a
    unEl

    instance IsSizeType Term where
      isSizeType :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Term -> m (Maybe BoundedSize)
    isSizeType Term
    v = m (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest m (Term -> Maybe BoundedSize) -> m Term -> m (Maybe BoundedSize)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v

    instance IsSizeType CompareAs where
      isSizeType :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    CompareAs -> m (Maybe BoundedSize)
    isSizeType (AsTermsOf Type
    a) = Type -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Type
    a
      isSizeType CompareAs
    AsSizes       = Maybe BoundedSize -> m (Maybe BoundedSize)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe BoundedSize -> m (Maybe BoundedSize))
    -> Maybe BoundedSize -> m (Maybe BoundedSize)
    forall a b. (a -> b) -> a -> b
    $ BoundedSize -> Maybe BoundedSize
    forall a. a -> Maybe a
    Just BoundedSize
    BoundedNo
      isSizeType CompareAs
    AsTypes       = Maybe BoundedSize -> m (Maybe BoundedSize)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe BoundedSize
    forall a. Maybe a
    Nothing

    isSizeTypeTest :: (HasOptions m, HasBuiltins m) => m (Term -> Maybe BoundedSize)
    isSizeTypeTest :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest =
      (m (Term -> Maybe BoundedSize)
     -> m (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize))
    -> m (Term -> Maybe BoundedSize)
    -> m (Term -> Maybe BoundedSize)
    -> m (Term -> Maybe BoundedSize)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (m Bool
    -> m (Term -> Maybe BoundedSize)
    -> m (Term -> Maybe BoundedSize)
    -> m (Term -> Maybe BoundedSize)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    sizedTypesOption) ((Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize))
    -> (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
    forall a b. (a -> b) -> a -> b
    $ Maybe BoundedSize -> Term -> Maybe BoundedSize
    forall a b. a -> b -> a
    const Maybe BoundedSize
    forall a. Maybe a
    Nothing) (m (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize))
    -> m (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
    forall a b. (a -> b) -> a -> b
    $ do
        (Maybe QName
    size, Maybe QName
    sizelt) <- m (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
        let testType :: Term -> Maybe BoundedSize
    testType (Def QName
    d [])        | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    size   = BoundedSize -> Maybe BoundedSize
    forall a. a -> Maybe a
    Just BoundedSize
    BoundedNo
            testType (Def QName
    d [Apply Arg Term
    v]) | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    sizelt = BoundedSize -> Maybe BoundedSize
    forall a. a -> Maybe a
    Just (BoundedSize -> Maybe BoundedSize)
    -> BoundedSize -> Maybe BoundedSize
    forall a b. (a -> b) -> a -> b
    $ 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
    v
            testType Term
    _                                    = Maybe BoundedSize
    forall a. Maybe a
    Nothing
        (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term -> Maybe BoundedSize
    testType

    getBuiltinDefName :: (HasBuiltins m) => String -> m (Maybe QName)
    getBuiltinDefName :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinDefName String
    s = Maybe Term -> Maybe QName
    fromDef (Maybe Term -> Maybe QName) -> m (Maybe Term) -> m (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    s
      where
        fromDef :: Maybe Term -> Maybe QName
    fromDef (Just (Def QName
    d [])) = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d
        fromDef Maybe Term
    _                 = Maybe QName
    forall a. Maybe a
    Nothing

    getBuiltinSize :: (HasBuiltins m) => m (Maybe QName, Maybe QName)
    getBuiltinSize :: forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize = do
      Maybe QName
    size   <- String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinDefName String
    builtinSize
      Maybe QName
    sizelt <- String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinDefName String
    builtinSizeLt
      (Maybe QName, Maybe QName) -> m (Maybe QName, Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName
    size, Maybe QName
    sizelt)

    isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
    isSizeNameTest :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (QName -> Bool)
    isSizeNameTest = m Bool
    -> m (QName -> Bool) -> m (QName -> Bool) -> m (QName -> Bool)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    sizedTypesOption
      m (QName -> Bool)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (QName -> Bool)
    isSizeNameTestRaw
      ((QName -> Bool) -> m (QName -> Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName -> Bool) -> m (QName -> Bool))
    -> (QName -> Bool) -> m (QName -> Bool)
    forall a b. (a -> b) -> a -> b
    $ Bool -> QName -> Bool
    forall a b. a -> b -> a
    const Bool
    False)

    isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
    isSizeNameTestRaw :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (QName -> Bool)
    isSizeNameTestRaw = do
      (Maybe QName
    size, Maybe QName
    sizelt) <- m (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
      (QName -> Bool) -> m (QName -> Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName -> Bool) -> m (QName -> Bool))
    -> (QName -> Bool) -> m (QName -> Bool)
    forall a b. (a -> b) -> a -> b
    $ (Maybe QName -> [Maybe QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Maybe QName
    size, Maybe QName
    sizelt]) (Maybe QName -> Bool) -> (QName -> Maybe QName) -> QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Maybe QName
    forall a. a -> Maybe a
    Just

    -- | Test whether OPTIONS --sized-types and whether
    --   the size built-ins are defined.
    haveSizedTypes :: TCM Bool
    haveSizedTypes :: TCM Bool
    haveSizedTypes = do
        Def QName
    _ [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSize
        Def QName
    _ [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
        Def QName
    _ [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeSuc
        TCM Bool
    forall (m :: * -> *). HasOptions m => m Bool
    sizedTypesOption
      TCM Bool -> (TCErr -> TCM Bool) -> TCM Bool
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ -> Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Test whether the SIZELT builtin is defined.
    haveSizeLt :: TCM Bool
    haveSizeLt :: TCM Bool
    haveSizeLt = Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe QName -> Bool) -> TCMT IO (Maybe QName) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinDefName String
    builtinSizeLt

    -- | Add polarity info to a SIZE builtin.
    builtinSizeHook :: String -> QName -> Type -> TCM ()
    builtinSizeHook :: String -> QName -> Type -> TCM ()
    builtinSizeHook String
    s QName
    q Type
    t = do
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (String
    s String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    builtinSizeLt, String
    builtinSizeSuc]) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q
          ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ ([Polarity] -> [Polarity]) -> Definition -> Definition
    updateDefPolarity       ([Polarity] -> [Polarity] -> [Polarity]
    forall a b. a -> b -> a
    const [Polarity
    Covariant])
          (Definition -> Definition)
    -> (Definition -> Definition) -> Definition -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Occurrence] -> [Occurrence]) -> Definition -> Definition
    updateDefArgOccurrences ([Occurrence] -> [Occurrence] -> [Occurrence]
    forall a b. a -> b -> a
    const [Occurrence
    StrictPos])
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    builtinSizeMax) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q
          ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ ([Polarity] -> [Polarity]) -> Definition -> Definition
    updateDefPolarity       ([Polarity] -> [Polarity] -> [Polarity]
    forall a b. a -> b -> a
    const [Polarity
    Covariant, Polarity
    Covariant])
          (Definition -> Definition)
    -> (Definition -> Definition) -> Definition -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Occurrence] -> [Occurrence]) -> Definition -> Definition
    updateDefArgOccurrences ([Occurrence] -> [Occurrence] -> [Occurrence]
    forall a b. a -> b -> a
    const [Occurrence
    StrictPos, Occurrence
    StrictPos])
    {-
          . updateDefType           (const tmax)
      where
        -- TODO: max : (i j : Size) -> Size< (suc (max i j))
        tmax =
    -}

    ------------------------------------------------------------------------
    -- * Constructors
    ------------------------------------------------------------------------

    -- | The sort of built-in types @SIZE@ and @SIZELT@.
    sizeSort :: Sort
    sizeSort :: Sort
    sizeSort = Integer -> Sort
    mkType Integer
    0

    -- | The type of built-in types @SIZE@ and @SIZELT@.
    sizeUniv :: Type
    sizeUniv :: Type
    sizeUniv = Sort -> Type
    sort (Sort -> Type) -> Sort -> Type
    forall a b. (a -> b) -> a -> b
    $ Sort
    sizeSort

    -- | The built-in type @SIZE@ with user-given name.
    sizeType_ :: QName -> Type
    sizeType_ :: QName -> Type
    sizeType_ QName
    size = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    sizeSort (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> [Elim] -> Term
    Def QName
    size []

    -- | The built-in type @SIZE@.
    sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type
    sizeType :: forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    sizeSort (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Type) -> m (Maybe Term) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSize

    -- | The name of @SIZESUC@.
    sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName)
    sizeSucName :: forall (m :: * -> *).
    (HasBuiltins m, HasOptions m) =>
    m (Maybe QName)
    sizeSucName = do
      m Bool -> m (Maybe QName) -> m (Maybe QName) -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Bool -> Bool
    not (Bool -> Bool) -> m Bool -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    sizedTypesOption) (Maybe QName -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing) (m (Maybe QName) -> m (Maybe QName))
    -> m (Maybe QName) -> m (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ do
        String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSizeSuc m (Maybe Term)
    -> (Maybe Term -> m (Maybe QName)) -> m (Maybe QName)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just (Def QName
    x []) -> Maybe QName -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> m (Maybe QName)) -> Maybe QName -> m (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x
          Maybe Term
    _               -> Maybe QName -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing

    sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
    sizeSuc :: forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
    sizeSuc Offset
    n Term
    v | Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    < Offset
    0     = m Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                | Offset
    n Offset -> Offset -> Bool
    forall a. Eq a => a -> a -> Bool
    == Offset
    0    = Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
                | Bool
    otherwise = do
      Def QName
    suc [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSizeSuc
      Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((Term -> Term) -> Term -> [Term]
    forall a. (a -> a) -> a -> [a]
    iterate (QName -> Term -> Term
    sizeSuc_ QName
    suc) Term
    v [Term] -> Offset -> Maybe Term
    forall a. [a] -> Offset -> Maybe a
    !!! Offset
    n)

    sizeSuc_ :: QName -> Term -> Term
    sizeSuc_ :: QName -> Term -> Term
    sizeSuc_ QName
    suc Term
    v = QName -> [Elim] -> Term
    Def QName
    suc [Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Arg Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    v]

    -- | Transform list of terms into a term build from binary maximum.
    sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
            => NonEmpty Term -> m Term
    sizeMax :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    NonEmpty Term -> m Term
    sizeMax NonEmpty Term
    vs = case NonEmpty Term
    vs of
      Term
    v :| [] -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      NonEmpty Term
    vs  -> do
        Def QName
    max [] <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeMax
        Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> Term) -> NonEmpty Term -> Term
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 (\ Term
    u Term
    v -> QName -> [Elim] -> Term
    Def QName
    max ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ (Term -> Elim) -> [Term] -> [Elim]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> (Term -> Arg Term) -> Term -> Elim
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall a. a -> Arg a
    defaultArg) [Term
    u,Term
    v]) NonEmpty Term
    vs

    ------------------------------------------------------------------------
    -- * Viewing and unviewing sizes
    ------------------------------------------------------------------------

    -- | A useful view on sizes.
    data SizeView = SizeInf | SizeSuc Term | OtherSize Term

    -- | Expects argument to be 'reduce'd.
    sizeView :: (HasBuiltins m, MonadTCEnv m, ReadTCState m)
             => Term -> m SizeView
    sizeView :: forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    v = do
      Def QName
    inf [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSizeInf
      Def QName
    suc [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSizeSuc
      case Term
    v of
        Def QName
    x []        | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    inf -> SizeView -> m SizeView
    forall (m :: * -> *) a. Monad m => a -> m a
    return SizeView
    SizeInf
        Def QName
    x [Apply Arg Term
    u] | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    suc -> SizeView -> m SizeView
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeView -> m SizeView) -> SizeView -> m SizeView
    forall a b. (a -> b) -> a -> b
    $ Term -> SizeView
    SizeSuc (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u)
        Term
    _                          -> SizeView -> m SizeView
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeView -> m SizeView) -> SizeView -> m SizeView
    forall a b. (a -> b) -> a -> b
    $ Term -> SizeView
    OtherSize Term
    v

    -- | A de Bruijn index under some projections.

    data ProjectedVar = ProjectedVar
      { ProjectedVar -> Offset
    pvIndex :: Int
      , ProjectedVar -> [(ProjOrigin, QName)]
    prProjs :: [(ProjOrigin, QName)]
      }
      deriving (Offset -> ProjectedVar -> ShowS
    [ProjectedVar] -> ShowS
    ProjectedVar -> String
    (Offset -> ProjectedVar -> ShowS)
    -> (ProjectedVar -> String)
    -> ([ProjectedVar] -> ShowS)
    -> Show ProjectedVar
    forall a.
    (Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [ProjectedVar] -> ShowS
    $cshowList :: [ProjectedVar] -> ShowS
    show :: ProjectedVar -> String
    $cshow :: ProjectedVar -> String
    showsPrec :: Offset -> ProjectedVar -> ShowS
    $cshowsPrec :: Offset -> ProjectedVar -> ShowS
    Show)

    -- | Ignore 'ProjOrigin' in equality test.

    instance Eq ProjectedVar where
      ProjectedVar Offset
    i [(ProjOrigin, QName)]
    prjs == :: ProjectedVar -> ProjectedVar -> Bool
    == ProjectedVar Offset
    i' [(ProjOrigin, QName)]
    prjs' =
        Offset
    i Offset -> Offset -> Bool
    forall a. Eq a => a -> a -> Bool
    == Offset
    i' Bool -> Bool -> Bool
    && ((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (ProjOrigin, QName) -> QName
    forall a b. (a, b) -> b
    snd [(ProjOrigin, QName)]
    prjs [QName] -> [QName] -> Bool
    forall a. Eq a => a -> a -> Bool
    == ((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (ProjOrigin, QName) -> QName
    forall a b. (a, b) -> b
    snd [(ProjOrigin, QName)]
    prjs'

    viewProjectedVar :: Term -> Maybe ProjectedVar
    viewProjectedVar :: Term -> Maybe ProjectedVar
    viewProjectedVar = \case
      Var Offset
    i [Elim]
    es -> Offset -> [(ProjOrigin, QName)] -> ProjectedVar
    ProjectedVar Offset
    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
      Term
    _ -> Maybe ProjectedVar
    forall a. Maybe a
    Nothing

    unviewProjectedVar :: ProjectedVar -> Term
    unviewProjectedVar :: ProjectedVar -> Term
    unviewProjectedVar (ProjectedVar Offset
    i [(ProjOrigin, QName)]
    prjs) = Offset -> [Elim] -> Term
    Var Offset
    i ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ ((ProjOrigin, QName) -> Elim) -> [(ProjOrigin, QName)] -> [Elim]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ProjOrigin -> QName -> Elim) -> (ProjOrigin, QName) -> Elim
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj) [(ProjOrigin, QName)]
    prjs

    type Offset = Nat

    -- | A deep view on sizes.
    data DeepSizeView
      = DSizeInf
      | DSizeVar ProjectedVar Offset
      | DSizeMeta MetaId Elims Offset
      | DOtherSize Term
      deriving (Offset -> DeepSizeView -> ShowS
    [DeepSizeView] -> ShowS
    DeepSizeView -> String
    (Offset -> DeepSizeView -> ShowS)
    -> (DeepSizeView -> String)
    -> ([DeepSizeView] -> ShowS)
    -> Show DeepSizeView
    forall a.
    (Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [DeepSizeView] -> ShowS
    $cshowList :: [DeepSizeView] -> ShowS
    show :: DeepSizeView -> String
    $cshow :: DeepSizeView -> String
    showsPrec :: Offset -> DeepSizeView -> ShowS
    $cshowsPrec :: Offset -> DeepSizeView -> ShowS
    Show)

    instance Pretty DeepSizeView where
      pretty :: DeepSizeView -> Doc
    pretty = \case
        DeepSizeView
    DSizeInf        -> Doc
    "∞"
        DSizeVar ProjectedVar
    pv Offset
    o    -> Term -> Doc
    forall a. Pretty a => a -> Doc
    pretty (ProjectedVar -> Term
    unviewProjectedVar ProjectedVar
    pv) Doc -> Doc -> Doc
    <+> Doc
    "+" Doc -> Doc -> Doc
    <+> Offset -> Doc
    forall a. Pretty a => a -> Doc
    pretty Offset
    o
        DSizeMeta MetaId
    x [Elim]
    es Offset
    o -> Term -> Doc
    forall a. Pretty a => a -> Doc
    pretty (MetaId -> [Elim] -> Term
    MetaV MetaId
    x [Elim]
    es) Doc -> Doc -> Doc
    <+> Doc
    "+" Doc -> Doc -> Doc
    <+> Offset -> Doc
    forall a. Pretty a => a -> Doc
    pretty Offset
    o
        DOtherSize Term
    t     -> Term -> Doc
    forall a. Pretty a => a -> Doc
    pretty Term
    t

    data SizeViewComparable a
      = NotComparable
      | YesAbove DeepSizeView a
      | YesBelow DeepSizeView a
      deriving ((forall a b.
     (a -> b) -> SizeViewComparable a -> SizeViewComparable b)
    -> (forall a b. a -> SizeViewComparable b -> SizeViewComparable a)
    -> Functor SizeViewComparable
    forall a b. a -> SizeViewComparable b -> SizeViewComparable a
    forall a b.
    (a -> b) -> SizeViewComparable a -> SizeViewComparable b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
    $c<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
    fmap :: forall a b.
    (a -> b) -> SizeViewComparable a -> SizeViewComparable b
    $cfmap :: forall a b.
    (a -> b) -> SizeViewComparable a -> SizeViewComparable b
    Functor)

    -- | @sizeViewComparable v w@ checks whether @v >= w@ (then @Left@)
    --   or @v <= w@ (then @Right@).  If uncomparable, it returns @NotComparable@.
    sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
    sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
    sizeViewComparable DeepSizeView
    v DeepSizeView
    w = case (DeepSizeView
    v,DeepSizeView
    w) of
      (DeepSizeView
    DSizeInf, DeepSizeView
    _) -> DeepSizeView -> () -> SizeViewComparable ()
    forall a. DeepSizeView -> a -> SizeViewComparable a
    YesAbove DeepSizeView
    w ()
      (DeepSizeView
    _, DeepSizeView
    DSizeInf) -> DeepSizeView -> () -> SizeViewComparable ()
    forall a. DeepSizeView -> a -> SizeViewComparable a
    YesBelow DeepSizeView
    w ()
      (DSizeVar ProjectedVar
    x Offset
    n, DSizeVar ProjectedVar
    y Offset
    m) | ProjectedVar
    x ProjectedVar -> ProjectedVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProjectedVar
    y -> if Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    m then DeepSizeView -> () -> SizeViewComparable ()
    forall a. DeepSizeView -> a -> SizeViewComparable a
    YesAbove DeepSizeView
    w () else DeepSizeView -> () -> SizeViewComparable ()
    forall a. DeepSizeView -> a -> SizeViewComparable a
    YesBelow DeepSizeView
    w ()
      (DeepSizeView, DeepSizeView)
    _ -> SizeViewComparable ()
    forall a. SizeViewComparable a
    NotComparable

    sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
    sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
    sizeViewSuc_ QName
    suc = \case
      DeepSizeView
    DSizeInf         -> DeepSizeView
    DSizeInf
      DSizeVar ProjectedVar
    i Offset
    n     -> ProjectedVar -> Offset -> DeepSizeView
    DSizeVar ProjectedVar
    i (Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    1)
      DSizeMeta MetaId
    x [Elim]
    vs Offset
    n -> MetaId -> [Elim] -> Offset -> DeepSizeView
    DSizeMeta MetaId
    x [Elim]
    vs (Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    1)
      DOtherSize Term
    u     -> Term -> DeepSizeView
    DOtherSize (Term -> DeepSizeView) -> Term -> DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ QName -> Term -> Term
    sizeSuc_ QName
    suc Term
    u

    -- | @sizeViewPred k v@ decrements @v@ by @k@ (must be possible!).
    sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView
    sizeViewPred :: Offset -> DeepSizeView -> DeepSizeView
    sizeViewPred Offset
    0 = DeepSizeView -> DeepSizeView
    forall a. a -> a
    id
    sizeViewPred Offset
    k = \case
      DeepSizeView
    DSizeInf -> DeepSizeView
    DSizeInf
      DSizeVar  ProjectedVar
    i    Offset
    n | Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    k -> ProjectedVar -> Offset -> DeepSizeView
    DSizeVar  ProjectedVar
    i    (Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    k)
      DSizeMeta MetaId
    x [Elim]
    vs Offset
    n | Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    k -> MetaId -> [Elim] -> Offset -> DeepSizeView
    DSizeMeta MetaId
    x [Elim]
    vs (Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    k)
      DeepSizeView
    _ -> DeepSizeView
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | @sizeViewOffset v@ returns the number of successors or Nothing when infty.
    sizeViewOffset :: DeepSizeView -> Maybe Offset
    sizeViewOffset :: DeepSizeView -> Maybe Offset
    sizeViewOffset = \case
      DeepSizeView
    DSizeInf         -> Maybe Offset
    forall a. Maybe a
    Nothing
      DSizeVar ProjectedVar
    i Offset
    n     -> Offset -> Maybe Offset
    forall a. a -> Maybe a
    Just Offset
    n
      DSizeMeta MetaId
    x [Elim]
    vs Offset
    n -> Offset -> Maybe Offset
    forall a. a -> Maybe a
    Just Offset
    n
      DOtherSize Term
    u     -> Offset -> Maybe Offset
    forall a. a -> Maybe a
    Just Offset
    0

    -- | Remove successors common to both sides.
    removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
    removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
    removeSucs (DeepSizeView
    v, DeepSizeView
    w) = (Offset -> DeepSizeView -> DeepSizeView
    sizeViewPred Offset
    k DeepSizeView
    v, Offset -> DeepSizeView -> DeepSizeView
    sizeViewPred Offset
    k DeepSizeView
    w)
      where k :: Offset
    k = case (DeepSizeView -> Maybe Offset
    sizeViewOffset DeepSizeView
    v, DeepSizeView -> Maybe Offset
    sizeViewOffset DeepSizeView
    w) of
                  (Just  Offset
    n, Just  Offset
    m) -> Offset -> Offset -> Offset
    forall a. Ord a => a -> a -> a
    min Offset
    n Offset
    m
                  (Just  Offset
    n, Maybe Offset
    Nothing) -> Offset
    n
                  (Maybe Offset
    Nothing, Just  Offset
    m) -> Offset
    m
                  (Maybe Offset
    Nothing, Maybe Offset
    Nothing) -> Offset
    0

    -- | Turn a size view into a term.
    unSizeView :: SizeView -> TCM Term
    unSizeView :: SizeView -> TCMT IO Term
    unSizeView SizeView
    SizeInf       = TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
    unSizeView (SizeSuc Term
    v)   = Offset -> Term -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
    sizeSuc Offset
    1 Term
    v
    unSizeView (OtherSize Term
    v) = Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

    unDeepSizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
                   => DeepSizeView -> m Term
    unDeepSizeView :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView = \case
      DeepSizeView
    DSizeInf         -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
      DSizeVar ProjectedVar
    pv    Offset
    n -> Offset -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
    sizeSuc Offset
    n (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ ProjectedVar -> Term
    unviewProjectedVar ProjectedVar
    pv
      DSizeMeta MetaId
    x [Elim]
    us Offset
    n -> Offset -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
    sizeSuc Offset
    n (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [Elim] -> Term
    MetaV MetaId
    x [Elim]
    us
      DOtherSize Term
    u     -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u

    ------------------------------------------------------------------------
    -- * View on sizes where maximum is pulled to the top
    ------------------------------------------------------------------------

    type SizeMaxView = NonEmpty DeepSizeView
    type SizeMaxView' = [DeepSizeView]

    maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
    maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
    maxViewMax SizeMaxView
    v SizeMaxView
    w = case (SizeMaxView
    v,SizeMaxView
    w) of
      (DeepSizeView
    DSizeInf :| [DeepSizeView]
    _, SizeMaxView
    _) -> DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton DeepSizeView
    DSizeInf
      (SizeMaxView
    _, DeepSizeView
    DSizeInf :| [DeepSizeView]
    _) -> DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton DeepSizeView
    DSizeInf
      (SizeMaxView, SizeMaxView)
    _                 -> (DeepSizeView -> SizeMaxView -> SizeMaxView)
    -> SizeMaxView -> SizeMaxView -> SizeMaxView
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Fold.foldr DeepSizeView -> SizeMaxView -> SizeMaxView
    maxViewCons SizeMaxView
    w SizeMaxView
    v

    -- | @maxViewCons v ws = max v ws@.  It only adds @v@ to @ws@ if it is not
    --   subsumed by an element of @ws@.
    maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
    maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
    maxViewCons DeepSizeView
    _ (DeepSizeView
    DSizeInf :| [DeepSizeView]
    _) = DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton DeepSizeView
    DSizeInf
    maxViewCons DeepSizeView
    DSizeInf SizeMaxView
    _        = DeepSizeView -> SizeMaxView
    forall el coll. Singleton el coll => el -> coll
    singleton DeepSizeView
    DSizeInf
    maxViewCons DeepSizeView
    v SizeMaxView
    ws = case DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
    sizeViewComparableWithMax DeepSizeView
    v SizeMaxView
    ws of
      SizeViewComparable [DeepSizeView]
    NotComparable  -> DeepSizeView -> SizeMaxView -> SizeMaxView
    forall a. a -> NonEmpty a -> NonEmpty a
    NonEmpty.cons DeepSizeView
    v SizeMaxView
    ws
      YesAbove DeepSizeView
    _ [DeepSizeView]
    ws' -> DeepSizeView
    v DeepSizeView -> [DeepSizeView] -> SizeMaxView
    forall a. a -> [a] -> NonEmpty a
    :| [DeepSizeView]
    ws'
      YesBelow{}     -> SizeMaxView
    ws

    -- | @sizeViewComparableWithMax v ws@ tries to find @w@ in @ws@ that compares with @v@
    --   and singles this out.
    --   Precondition: @v /= DSizeInv@.
    sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView'
    sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
    sizeViewComparableWithMax DeepSizeView
    v (DeepSizeView
    w :| [DeepSizeView]
    ws) =
      case ([DeepSizeView]
    ws, DeepSizeView -> DeepSizeView -> SizeViewComparable ()
    sizeViewComparable DeepSizeView
    v DeepSizeView
    w) of
        (DeepSizeView
    w':[DeepSizeView]
    ws', SizeViewComparable ()
    NotComparable) -> (DeepSizeView
    wDeepSizeView -> [DeepSizeView] -> [DeepSizeView]
    forall a. a -> [a] -> [a]
    :) ([DeepSizeView] -> [DeepSizeView])
    -> SizeViewComparable [DeepSizeView]
    -> SizeViewComparable [DeepSizeView]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
    sizeViewComparableWithMax DeepSizeView
    v (DeepSizeView
    w' DeepSizeView -> [DeepSizeView] -> SizeMaxView
    forall a. a -> [a] -> NonEmpty a
    :| [DeepSizeView]
    ws')
        ([DeepSizeView]
    ws    , SizeViewComparable ()
    r)             -> (() -> [DeepSizeView])
    -> SizeViewComparable () -> SizeViewComparable [DeepSizeView]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([DeepSizeView] -> () -> [DeepSizeView]
    forall a b. a -> b -> a
    const [DeepSizeView]
    ws) SizeViewComparable ()
    r

    maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
    maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
    maxViewSuc_ QName
    suc = (DeepSizeView -> DeepSizeView) -> SizeMaxView -> SizeMaxView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName -> DeepSizeView -> DeepSizeView
    sizeViewSuc_ QName
    suc)

    unMaxView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
              => SizeMaxView -> m Term
    unMaxView :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    SizeMaxView -> m Term
    unMaxView SizeMaxView
    vs = NonEmpty Term -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    NonEmpty Term -> m Term
    sizeMax (NonEmpty Term -> m Term) -> m (NonEmpty Term) -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (DeepSizeView -> m Term) -> SizeMaxView -> m (NonEmpty Term)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    Trav.mapM DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView SizeMaxView
    vs