    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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 ( MonadError(..) )

    import qualified Data.Foldable as Fold
    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.CallStack
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- * Builtins
    ------------------------------------------------------------------------

    -- | Ensure that option @--sized-types@ is on, for the given reason.
    --
    requireOptionSizedTypes :: (HasCallStack, HasOptions m, MonadTCError m) => String -> m ()
    requireOptionSizedTypes :: forall (m :: * -> *).
    (HasCallStack, HasOptions m, MonadTCError m) =>
    String -> m ()
    requireOptionSizedTypes String
    reason = m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    sizedTypesOption (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
      TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    NeedOptionSizedTypes String
    reason

    getBuiltinSize :: (HasBuiltins m) => m (Maybe QName, Maybe QName)
    getBuiltinSize :: forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize = do
      size   <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSize
      sizelt <- getBuiltinName' builtinSizeLt
      return (size, sizelt)

    -- | 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
    <$> BuiltinId -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSizeLt

    -- | Add polarity info to a SIZE builtin.
    builtinSizeHook :: BuiltinId -> QName -> Type -> TCM ()
    builtinSizeHook :: BuiltinId -> QName -> Type -> TCM ()
    builtinSizeHook BuiltinId
    s QName
    q Type
    t = do
      Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (BuiltinId
    s BuiltinId -> [BuiltinId] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [BuiltinId
    builtinSizeLt, BuiltinId
    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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (BuiltinId
    s BuiltinId -> BuiltinId -> Bool
    forall a. Eq a => a -> a -> Bool
    == BuiltinId
    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 =
    -}

    ------------------------------------------------------------------------
    -- * 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
    $c== :: BoundedSize -> BoundedSize -> Bool
    == :: BoundedSize -> BoundedSize -> Bool
    $c/= :: BoundedSize -> BoundedSize -> Bool
    /= :: 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
    $cshowsPrec :: Offset -> BoundedSize -> ShowS
    showsPrec :: Offset -> BoundedSize -> ShowS
    $cshow :: BoundedSize -> String
    show :: BoundedSize -> String
    $cshowList :: [BoundedSize] -> ShowS
    showList :: [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)
    forall (m :: * -> *).
    (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)
    forall (m :: * -> *).
    (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)
    forall (m :: * -> *).
    (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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a. a -> m a
    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)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Type -> m (Maybe BoundedSize)
    isSizeType Type
    a
      isSizeType CompareAs
    AsSizes       = Maybe BoundedSize -> m (Maybe BoundedSize)
    forall a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    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
        (size, sizelt) <- m (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
        let 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
        return testType

    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 a. a -> m a
    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
      (size, sizelt) <- m (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
      return $ (`elem` [size, sizelt]) . Just

    ------------------------------------------------------------------------
    -- * 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 []

    {-# SPECIALIZE sizeType :: TCM Type #-}
    -- | 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
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    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 a. a -> m a
    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
        BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinSizeSuc m (Maybe Term)
    -> (Maybe Term -> m (Maybe QName)) -> m (Maybe QName)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just (Def QName
    x []) -> Maybe QName -> m (Maybe QName)
    forall a. a -> m a
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing

    {-# SPECIALIZE sizeSuc :: Nat -> Term -> TCM Term #-}
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
                | Bool
    otherwise = do
      suc <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSizeSuc
      return $ fromMaybe __IMPOSSIBLE__ (iterate (sizeSuc_ suc) v !!! 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)
            => List1 Term -> m Term
    sizeMax :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    List1 Term -> m Term
    sizeMax List1 Term
    vs = case List1 Term
    vs of
      Term
    v :| [] -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      List1 Term
    vs  -> do
        max <- BuiltinId -> m QName
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    builtinSizeMax
        return $ 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]) 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
      inf <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSizeInf
      suc <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSizeSuc
      case v of
        Def QName
    x []        | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    inf -> SizeView -> m SizeView
    forall a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    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
    $cshowsPrec :: Offset -> ProjectedVar -> ShowS
    showsPrec :: Offset -> ProjectedVar -> ShowS
    $cshow :: ProjectedVar -> String
    show :: ProjectedVar -> String
    $cshowList :: [ProjectedVar] -> ShowS
    showList :: [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim [Elim]
    es
      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
    $cshowsPrec :: Offset -> DeepSizeView -> ShowS
    showsPrec :: Offset -> DeepSizeView -> ShowS
    $cshow :: DeepSizeView -> String
    show :: DeepSizeView -> String
    $cshowList :: [DeepSizeView] -> ShowS
    showList :: [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
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "+" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> 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
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "+" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> 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
    $cfmap :: forall a b.
    (a -> b) -> SizeViewComparable a -> SizeViewComparable b
    fmap :: forall a b.
    (a -> b) -> SizeViewComparable a -> SizeViewComparable b
    $c<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
    <$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
    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 -> TCM Term
    unSizeView SizeView
    SizeInf       = TCM Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
    unSizeView (SizeSuc Term
    v)   = Offset -> Term -> TCM Term
    forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
    sizeSuc Offset
    1 Term
    v
    unSizeView (OtherSize Term
    v) = Term -> TCM Term
    forall a. a -> TCMT IO a
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u

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

    type SizeMaxView = List1 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 a b. (a -> b -> b) -> b -> NonEmpty a -> b
    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
    List1.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 a b.
    (a -> b) -> SizeViewComparable a -> SizeViewComparable b
    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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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 = List1 Term -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    List1 Term -> m Term
    sizeMax (List1 Term -> m Term) -> m (List1 Term) -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (DeepSizeView -> m Term) -> SizeMaxView -> m (List1 Term)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    Trav.mapM DeepSizeView -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    DeepSizeView -> m Term
    unDeepSizeView SizeMaxView
    vs