    module Agda.TypeChecking.Level where

    import Data.Maybe
    import qualified Data.List as List
    import Data.List.NonEmpty (NonEmpty(..))
    import Data.Traversable (Traversable)

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

    import Agda.TypeChecking.Free.Lazy
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Reduce

    import Agda.Utils.Maybe ( caseMaybeM, allJustM )
    import Agda.Utils.Monad ( tryMaybe )
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    data LevelKit = LevelKit
      { LevelKit -> Term
    lvlType  :: Term
      , LevelKit -> Term -> Term
    lvlSuc   :: Term -> Term
      , LevelKit -> Term -> Term -> Term
    lvlMax   :: Term -> Term -> Term
      , LevelKit -> Term
    lvlZero  :: Term
      , LevelKit -> QName
    typeName :: QName
      , LevelKit -> QName
    sucName  :: QName
      , LevelKit -> QName
    maxName  :: QName
      , LevelKit -> QName
    zeroName :: QName
      }

    -- | Get the 'primLevel' as a 'Type'.
    levelType :: (HasBuiltins m) => m Type
    levelType :: forall (m :: * -> *). HasBuiltins m => m Type
    levelType = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort' Term
    mkType Integer
    0) (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
    builtinLevel

    isLevelType :: PureTCM m => Type -> m Bool
    isLevelType :: forall (m :: * -> *). PureTCM m => Type -> m Bool
    isLevelType Type
    a = 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
    a) m Term -> (Term -> m Bool) -> m Bool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Def QName
    f [] -> do
        Def QName
    lvl [] <- 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
    builtinLevel
        Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    lvl
      Term
    _ -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    levelSucFunction :: TCM (Term -> Term)
    levelSucFunction :: TCM (Term -> Term)
    levelSucFunction = Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 (Term -> Term -> Term) -> TCMT IO Term -> TCM (Term -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc

    {-# SPECIALIZE builtinLevelKit :: TCM LevelKit #-}
    {-# SPECIALIZE builtinLevelKit :: ReduceM LevelKit #-}
    builtinLevelKit :: (HasBuiltins m) => m LevelKit
    builtinLevelKit :: forall (m :: * -> *). HasBuiltins m => m LevelKit
    builtinLevelKit = do
        level :: Term
    level@(Def QName
    l []) <- 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
    builtinLevel
        zero :: Term
    zero@(Def QName
    z [])  <- 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
    builtinLevelZero
        suc :: Term
    suc@(Def QName
    s [])   <- 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
    builtinLevelSuc
        max :: Term
    max@(Def QName
    m [])   <- 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
    builtinLevelMax
        LevelKit -> m LevelKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LevelKit -> m LevelKit) -> LevelKit -> m LevelKit
    forall a b. (a -> b) -> a -> b
    $ LevelKit :: Term
    -> (Term -> Term)
    -> (Term -> Term -> Term)
    -> Term
    -> QName
    -> QName
    -> QName
    -> QName
    -> LevelKit
    LevelKit
          { lvlType :: Term
    lvlType  = Term
    level
          , lvlSuc :: Term -> Term
    lvlSuc   = \ Term
    a -> Term
    suc Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    `apply1` Term
    a
          , lvlMax :: Term -> Term -> Term
    lvlMax   = \ Term
    a Term
    b -> Term
    max Term -> [Term] -> Term
    forall t. Apply t => t -> [Term] -> t
    `applys` [Term
    a, Term
    b]
          , lvlZero :: Term
    lvlZero  = Term
    zero
          , typeName :: QName
    typeName = QName
    l
          , sucName :: QName
    sucName  = QName
    s
          , maxName :: QName
    maxName  = QName
    m
          , zeroName :: QName
    zeroName = QName
    z
          }

    -- | Raises an error if no level kit is available.
    requireLevels :: HasBuiltins m => m LevelKit
    requireLevels :: forall (m :: * -> *). HasBuiltins m => m LevelKit
    requireLevels = m LevelKit
    forall (m :: * -> *). HasBuiltins m => m LevelKit
    builtinLevelKit

    -- | Checks whether level kit is fully available.
    haveLevels :: HasBuiltins m => m Bool
    haveLevels :: forall (m :: * -> *). HasBuiltins m => m Bool
    haveLevels = m (Maybe [Term]) -> m Bool -> ([Term] -> m Bool) -> m Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM ([m (Maybe Term)] -> m (Maybe [Term])
    forall (m :: * -> *) a. Monad m => [m (Maybe a)] -> m (Maybe [a])
    allJustM ([m (Maybe Term)] -> m (Maybe [Term]))
    -> [m (Maybe Term)] -> m (Maybe [Term])
    forall a b. (a -> b) -> a -> b
    $ (String -> m (Maybe Term)) -> [String] -> [m (Maybe Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' [String]
    levelBuiltins)
        (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False)
        (\ [Term]
    _bs -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
      where
      levelBuiltins :: [String]
    levelBuiltins =
        [ String
    builtinLevel
        , String
    builtinLevelZero
        , String
    builtinLevelSuc
        , String
    builtinLevelMax
        ]

    {-# SPECIALIZE unLevel :: Term -> TCM Term #-}
    {-# SPECIALIZE unLevel :: Term -> ReduceM Term #-}
    unLevel :: (HasBuiltins m) => Term -> m Term
    unLevel :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
    unLevel (Level Level
    l)  = Level -> m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    l
    unLevel Term
    v = Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

    {-# SPECIALIZE reallyUnLevelView :: Level -> TCM Term #-}
    {-# SPECIALIZE reallyUnLevelView :: Level -> ReduceM Term #-}
    reallyUnLevelView :: (HasBuiltins m) => Level -> m Term
    reallyUnLevelView :: forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    nv = do
      Term
    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
    builtinLevelSuc
      Term
    zer <- 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
    builtinLevelZero
      case Level
    nv of
        Max Integer
    n []       -> 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) -> Integer -> Term
    unConstV Term
    zer (Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    suc) Integer
    n
        Max Integer
    0 [PlusLevel' Term
    a]      -> 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) -> PlusLevel' Term -> Term
    unPlusV (Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 Term
    suc) PlusLevel' Term
    a
        Level
    _              -> (LevelKit -> Level -> Term
    `unlevelWithKit` Level
    nv) (LevelKit -> Term) -> m LevelKit -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m LevelKit
    forall (m :: * -> *). HasBuiltins m => m LevelKit
    builtinLevelKit

    unlevelWithKit :: LevelKit -> Level -> Term
    unlevelWithKit :: LevelKit -> Level -> Term
    unlevelWithKit LevelKit{ lvlZero :: LevelKit -> Term
    lvlZero = Term
    zer, lvlSuc :: LevelKit -> Term -> Term
    lvlSuc = Term -> Term
    suc, lvlMax :: LevelKit -> Term -> Term -> Term
    lvlMax = Term -> Term -> Term
    max } = \case
      Max Integer
    m []  -> Term -> (Term -> Term) -> Integer -> Term
    unConstV Term
    zer Term -> Term
    suc Integer
    m
      Max Integer
    0 [PlusLevel' Term
    a] -> (Term -> Term) -> PlusLevel' Term -> Term
    unPlusV Term -> Term
    suc PlusLevel' Term
    a
      Max Integer
    m [PlusLevel' Term]
    as  -> (Term -> Term -> Term) -> [Term] -> Term
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 Term -> Term -> Term
    max ([Term] -> Term) -> [Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [ Term -> (Term -> Term) -> Integer -> Term
    unConstV Term
    zer Term -> Term
    suc Integer
    m | Integer
    m Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 ] [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (PlusLevel' Term -> Term) -> [PlusLevel' Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Term) -> PlusLevel' Term -> Term
    unPlusV Term -> Term
    suc) [PlusLevel' Term]
    as

    unConstV :: Term -> (Term -> Term) -> Integer -> Term
    unConstV :: Term -> (Term -> Term) -> Integer -> Term
    unConstV Term
    zer Term -> Term
    suc Integer
    n = ((Term -> Term) -> Term -> Term) -> Term -> [Term -> Term] -> Term
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    ($) Term
    zer (Integer -> (Term -> Term) -> [Term -> Term]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate Integer
    n Term -> Term
    suc)

    unPlusV :: (Term -> Term) -> PlusLevel -> Term
    unPlusV :: (Term -> Term) -> PlusLevel' Term -> Term
    unPlusV Term -> Term
    suc (Plus Integer
    n Term
    a) = ((Term -> Term) -> Term -> Term) -> Term -> [Term -> Term] -> Term
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    ($) Term
    a (Integer -> (Term -> Term) -> [Term -> Term]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate Integer
    n Term -> Term
    suc)

    maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
    maybePrimCon :: TCMT IO Term -> TCM (Maybe ConHead)
    maybePrimCon TCMT IO Term
    prim = TCMT IO ConHead -> TCM (Maybe ConHead)
    forall e (m :: * -> *) a.
    (MonadError e m, Functor m) =>
    m a -> m (Maybe a)
    tryMaybe (TCMT IO ConHead -> TCM (Maybe ConHead))
    -> TCMT IO ConHead -> TCM (Maybe ConHead)
    forall a b. (a -> b) -> a -> b
    $ do
        Con ConHead
    c ConInfo
    ci [] <- TCMT IO Term
    prim
        ConHead -> TCMT IO ConHead
    forall (m :: * -> *) a. Monad m => a -> m a
    return ConHead
    c

    maybePrimDef :: TCM Term -> TCM (Maybe QName)
    maybePrimDef :: TCMT IO Term -> TCM (Maybe QName)
    maybePrimDef TCMT IO Term
    prim = TCMT IO QName -> TCM (Maybe QName)
    forall e (m :: * -> *) a.
    (MonadError e m, Functor m) =>
    m a -> m (Maybe a)
    tryMaybe (TCMT IO QName -> TCM (Maybe QName))
    -> TCMT IO QName -> TCM (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ do
        Def QName
    f [] <- TCMT IO Term
    prim
        QName -> TCMT IO QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    f

    levelView :: PureTCM m => Term -> m Level
    levelView :: forall (m :: * -> *). PureTCM m => Term -> m Level
    levelView Term
    a = do
      String -> VerboseLevel -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> String -> m ()
    reportSLn String
    "tc.level.view" VerboseLevel
    50 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "{ levelView " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Term -> String
    forall a. Show a => a -> String
    show Term
    a
      Level
    v <- Term -> m Level
    forall (m :: * -> *). PureTCM m => Term -> m Level
    levelView' Term
    a
      String -> VerboseLevel -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> String -> m ()
    reportSLn String
    "tc.level.view" VerboseLevel
    50 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "  view: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Level -> String
    forall a. Show a => a -> String
    show Level
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "}"
      Level -> m Level
    forall (m :: * -> *) a. Monad m => a -> m a
    return Level
    v

    levelView' :: PureTCM m => Term -> m Level
    levelView' :: forall (m :: * -> *). PureTCM m => Term -> m Level
    levelView' Term
    a = do
      Def QName
    lzero [] <- 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
    builtinLevelZero
      Def QName
    lsuc  [] <- 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
    builtinLevelSuc
      Def QName
    lmax  [] <- 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
    builtinLevelMax
      let view :: Term -> m Level
    view Term
    a = do
            Blocked Term
    ba <- Term -> m (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    a
            case Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    ba of
              Level Level
    l -> Level -> m Level
    forall (m :: * -> *) a. Monad m => a -> m a
    return Level
    l
              Def QName
    s [Apply Arg Term
    arg]
                | QName
    s QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    lsuc  -> Level -> Level
    levelSuc (Level -> Level) -> m Level -> m Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Level
    view (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg)
              Def QName
    z []
                | QName
    z QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    lzero -> Level -> m Level
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Level -> m Level) -> Level -> m Level
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    0
              Def QName
    m [Apply Arg Term
    arg1, Apply Arg Term
    arg2]
                | QName
    m QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    lmax  -> Level -> Level -> Level
    levelLub (Level -> Level -> Level) -> m Level -> m (Level -> Level)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Level
    view (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg1) m (Level -> Level) -> m Level -> m Level
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Level
    view (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg2)
              Term
    l              -> Level -> m Level
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Level -> m Level) -> Level -> m Level
    forall a b. (a -> b) -> a -> b
    $ Term -> Level
    forall t. t -> Level' t
    atomicLevel Term
    l
      Term -> m Level
    view Term
    a

    -- | Given a level @l@, find the maximum constant @n@ such that @l = n + l'@
    levelPlusView :: Level -> (Integer, Level)
    levelPlusView :: Level -> (Integer, Level)
    levelPlusView (Max Integer
    0 []) = (Integer
    0 , Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 [])
    levelPlusView (Max Integer
    0 as :: [PlusLevel' Term]
    as@(PlusLevel' Term
    _:[PlusLevel' Term]
    _)) = (Integer
    minN , Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 ((PlusLevel' Term -> PlusLevel' Term)
    -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' Term -> PlusLevel' Term
    sub [PlusLevel' Term]
    as))
      where
        minN :: Integer
    minN = [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [ Integer
    n | Plus Integer
    n Term
    _ <- [PlusLevel' Term]
    as ]
        sub :: PlusLevel' Term -> PlusLevel' Term
    sub (Plus Integer
    n Term
    a) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    minN) Term
    a
    levelPlusView (Max Integer
    n [PlusLevel' Term]
    as) = (Integer
    minN , Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    minN) ((PlusLevel' Term -> PlusLevel' Term)
    -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' Term -> PlusLevel' Term
    sub [PlusLevel' Term]
    as))
      where
        minN :: Integer
    minN = [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum ([Integer] -> Integer) -> [Integer] -> Integer
    forall a b. (a -> b) -> a -> b
    $ Integer
    n Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [ Integer
    n' | Plus Integer
    n' Term
    _ <- [PlusLevel' Term]
    as ]
        sub :: PlusLevel' Term -> PlusLevel' Term
    sub (Plus Integer
    n' Term
    a) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer
    n' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    minN) Term
    a

    -- | Given a level @l@, find the biggest constant @n@ such that @n <= l@
    levelLowerBound :: Level -> Integer
    levelLowerBound :: Level -> Integer
    levelLowerBound (Max Integer
    m [PlusLevel' Term]
    as) = [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Integer] -> Integer) -> [Integer] -> Integer
    forall a b. (a -> b) -> a -> b
    $ Integer
    m Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [Integer
    n | Plus Integer
    n Term
    _ <- [PlusLevel' Term]
    as]

    -- | Given a constant @n@ and a level @l@, find the level @l'@ such
    --   that @l = n + l'@ (or Nothing if there is no such level).
    --   Operates on levels in canonical form.
    subLevel :: Integer -> Level -> Maybe Level
    subLevel :: Integer -> Level -> Maybe Level
    subLevel Integer
    n (Max Integer
    m [PlusLevel' Term]
    ls) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max (Integer -> [PlusLevel' Term] -> Level)
    -> Maybe Integer -> Maybe ([PlusLevel' Term] -> Level)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Integer
    m' Maybe ([PlusLevel' Term] -> Level)
    -> Maybe [PlusLevel' Term] -> Maybe Level
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (PlusLevel' Term -> Maybe (PlusLevel' Term))
    -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse PlusLevel' Term -> Maybe (PlusLevel' Term)
    subPlus [PlusLevel' Term]
    ls
      where
        m' :: Maybe Integer
        m' :: Maybe Integer
    m' | Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0, Bool -> Bool
    not ([PlusLevel' Term] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [PlusLevel' Term]
    ls) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0
           | Bool
    otherwise             = Integer -> Maybe Integer
    sub Integer
    m

        -- General purpose function.
        nonNeg :: Integer -> Maybe Integer
        nonNeg :: Integer -> Maybe Integer
    nonNeg Integer
    j | Integer
    j Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0 = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    j
                 | Bool
    otherwise = Maybe Integer
    forall a. Maybe a
    Nothing

        sub :: Integer -> Maybe Integer
        sub :: Integer -> Maybe Integer
    sub = Integer -> Maybe Integer
    nonNeg (Integer -> Maybe Integer)
    -> (Integer -> Integer) -> Integer -> Maybe Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    subtract Integer
    n

        subPlus :: PlusLevel -> Maybe PlusLevel
        subPlus :: PlusLevel' Term -> Maybe (PlusLevel' Term)
    subPlus (Plus Integer
    j Term
    l) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer -> Term -> PlusLevel' Term)
    -> Maybe Integer -> Maybe (Term -> PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Maybe Integer
    sub Integer
    j Maybe (Term -> PlusLevel' Term)
    -> Maybe Term -> Maybe (PlusLevel' Term)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    l

    -- | Given two levels @a@ and @b@, try to decompose the first one as
    -- @a = a' ⊔ b@ (for the minimal value of @a'@).
    levelMaxDiff :: Level -> Level -> Maybe Level
    levelMaxDiff :: Level -> Level -> Maybe Level
    levelMaxDiff (Max Integer
    m [PlusLevel' Term]
    as) (Max Integer
    n [PlusLevel' Term]
    bs) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max (Integer -> [PlusLevel' Term] -> Level)
    -> Maybe Integer -> Maybe ([PlusLevel' Term] -> Level)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Integer -> Maybe Integer
    diffC Integer
    m Integer
    n Maybe ([PlusLevel' Term] -> Level)
    -> Maybe [PlusLevel' Term] -> Maybe Level
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    diffP [PlusLevel' Term]
    as [PlusLevel' Term]
    bs
      where
        diffC :: Integer -> Integer -> Maybe Integer
        diffC :: Integer -> Integer -> Maybe Integer
    diffC Integer
    m Integer
    n
          | Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n    = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0
          | Integer
    m Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    n     = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    m
          | Bool
    otherwise = Maybe Integer
    forall a. Maybe a
    Nothing

        diffP :: [PlusLevel] -> [PlusLevel] -> Maybe [PlusLevel]
        diffP :: [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    diffP [PlusLevel' Term]
    as     []     = [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    forall a. a -> Maybe a
    Just [PlusLevel' Term]
    as
        diffP []     [PlusLevel' Term]
    bs     = Maybe [PlusLevel' Term]
    forall a. Maybe a
    Nothing
        diffP (a :: PlusLevel' Term
    a@(Plus Integer
    m Term
    x) : [PlusLevel' Term]
    as) (b :: PlusLevel' Term
    b@(Plus Integer
    n Term
    y) : [PlusLevel' Term]
    bs)
          | Term
    x Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    y = if
            | Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n    -> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    diffP [PlusLevel' Term]
    as [PlusLevel' Term]
    bs
            | Integer
    m Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    n     -> (Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    m Term
    xPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. a -> [a] -> [a]
    :) ([PlusLevel' Term] -> [PlusLevel' Term])
    -> Maybe [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    diffP [PlusLevel' Term]
    as [PlusLevel' Term]
    bs
            | Bool
    otherwise -> Maybe [PlusLevel' Term]
    forall a. Maybe a
    Nothing
          | Bool
    otherwise = (PlusLevel' Term
    aPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. a -> [a] -> [a]
    :) ([PlusLevel' Term] -> [PlusLevel' Term])
    -> Maybe [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
    diffP [PlusLevel' Term]
    as (PlusLevel' Term
    bPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. a -> [a] -> [a]
    :[PlusLevel' Term]
    bs)

    -- | A @SingleLevel@ is a @Level@ that cannot be further decomposed as
    --   a maximum @a ⊔ b@.
    data SingleLevel' t = SingleClosed Integer | SinglePlus (PlusLevel' t)
      deriving (VerboseLevel -> SingleLevel' t -> String -> String
    [SingleLevel' t] -> String -> String
    SingleLevel' t -> String
    (VerboseLevel -> SingleLevel' t -> String -> String)
    -> (SingleLevel' t -> String)
    -> ([SingleLevel' t] -> String -> String)
    -> Show (SingleLevel' t)
    forall t.
    Show t =>
    VerboseLevel -> SingleLevel' t -> String -> String
    forall t. Show t => [SingleLevel' t] -> String -> String
    forall t. Show t => SingleLevel' t -> String
    forall a.
    (VerboseLevel -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [SingleLevel' t] -> String -> String
    $cshowList :: forall t. Show t => [SingleLevel' t] -> String -> String
    show :: SingleLevel' t -> String
    $cshow :: forall t. Show t => SingleLevel' t -> String
    showsPrec :: VerboseLevel -> SingleLevel' t -> String -> String
    $cshowsPrec :: forall t.
    Show t =>
    VerboseLevel -> SingleLevel' t -> String -> String
    Show, (forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b)
    -> (forall a b. a -> SingleLevel' b -> SingleLevel' a)
    -> Functor SingleLevel'
    forall a b. a -> SingleLevel' b -> SingleLevel' a
    forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' 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 -> SingleLevel' b -> SingleLevel' a
    $c<$ :: forall a b. a -> SingleLevel' b -> SingleLevel' a
    fmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
    $cfmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
    Functor, (forall m. Monoid m => SingleLevel' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b)
    -> (forall a. (a -> a -> a) -> SingleLevel' a -> a)
    -> (forall a. (a -> a -> a) -> SingleLevel' a -> a)
    -> (forall a. SingleLevel' a -> [a])
    -> (forall a. SingleLevel' a -> Bool)
    -> (forall a. SingleLevel' a -> VerboseLevel)
    -> (forall a. Eq a => a -> SingleLevel' a -> Bool)
    -> (forall a. Ord a => SingleLevel' a -> a)
    -> (forall a. Ord a => SingleLevel' a -> a)
    -> (forall a. Num a => SingleLevel' a -> a)
    -> (forall a. Num a => SingleLevel' a -> a)
    -> Foldable SingleLevel'
    forall a. Eq a => a -> SingleLevel' a -> Bool
    forall a. Num a => SingleLevel' a -> a
    forall a. Ord a => SingleLevel' a -> a
    forall m. Monoid m => SingleLevel' m -> m
    forall a. SingleLevel' a -> Bool
    forall a. SingleLevel' a -> VerboseLevel
    forall a. SingleLevel' a -> [a]
    forall a. (a -> a -> a) -> SingleLevel' a -> a
    forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> VerboseLevel)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => SingleLevel' a -> a
    $cproduct :: forall a. Num a => SingleLevel' a -> a
    sum :: forall a. Num a => SingleLevel' a -> a
    $csum :: forall a. Num a => SingleLevel' a -> a
    minimum :: forall a. Ord a => SingleLevel' a -> a
    $cminimum :: forall a. Ord a => SingleLevel' a -> a
    maximum :: forall a. Ord a => SingleLevel' a -> a
    $cmaximum :: forall a. Ord a => SingleLevel' a -> a
    elem :: forall a. Eq a => a -> SingleLevel' a -> Bool
    $celem :: forall a. Eq a => a -> SingleLevel' a -> Bool
    length :: forall a. SingleLevel' a -> VerboseLevel
    $clength :: forall a. SingleLevel' a -> VerboseLevel
    null :: forall a. SingleLevel' a -> Bool
    $cnull :: forall a. SingleLevel' a -> Bool
    toList :: forall a. SingleLevel' a -> [a]
    $ctoList :: forall a. SingleLevel' a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    foldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    $cfoldr :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    fold :: forall m. Monoid m => SingleLevel' m -> m
    $cfold :: forall m. Monoid m => SingleLevel' m -> m
    Foldable, Functor SingleLevel'
    Foldable SingleLevel'
    Functor SingleLevel'
    -> Foldable SingleLevel'
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> SingleLevel' a -> f (SingleLevel' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        SingleLevel' (f a) -> f (SingleLevel' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> SingleLevel' a -> m (SingleLevel' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        SingleLevel' (m a) -> m (SingleLevel' a))
    -> Traversable SingleLevel'
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    SingleLevel' (m a) -> m (SingleLevel' a)
    forall (f :: * -> *) a.
    Applicative f =>
    SingleLevel' (f a) -> f (SingleLevel' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    SingleLevel' (m a) -> m (SingleLevel' a)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    SingleLevel' (m a) -> m (SingleLevel' a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    SingleLevel' (f a) -> f (SingleLevel' a)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    SingleLevel' (f a) -> f (SingleLevel' a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
    Traversable)

    type SingleLevel = SingleLevel' Term

    deriving instance Eq SingleLevel

    unSingleLevel :: SingleLevel' t -> Level' t
    unSingleLevel :: forall t. SingleLevel' t -> Level' t
    unSingleLevel (SingleClosed Integer
    m) = Integer -> [PlusLevel' t] -> Level' t
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    m []
    unSingleLevel (SinglePlus PlusLevel' t
    a)   = Integer -> [PlusLevel' t] -> Level' t
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 [PlusLevel' t
    a]

    -- | Return the maximum of the given @SingleLevel@s
    unSingleLevels :: [SingleLevel] -> Level
    unSingleLevels :: [SingleLevel] -> Level
    unSingleLevels [SingleLevel]
    ls = Integer -> [PlusLevel' Term] -> Level
    levelMax Integer
    n [PlusLevel' Term]
    as
      where
        n :: Integer
    n = [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Integer] -> Integer) -> [Integer] -> Integer
    forall a b. (a -> b) -> a -> b
    $ Integer
    0 Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [Integer
    m | SingleClosed Integer
    m <- [SingleLevel]
    ls]
        as :: [PlusLevel' Term]
    as = [PlusLevel' Term
    a | SinglePlus PlusLevel' Term
    a <- [SingleLevel]
    ls]

    levelMaxView :: Level' t -> NonEmpty (SingleLevel' t)
    levelMaxView :: forall t. Level' t -> NonEmpty (SingleLevel' t)
    levelMaxView (Max Integer
    n [])     = SingleLevel' t -> NonEmpty (SingleLevel' t)
    forall el coll. Singleton el coll => el -> coll
    singleton (SingleLevel' t -> NonEmpty (SingleLevel' t))
    -> SingleLevel' t -> NonEmpty (SingleLevel' t)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SingleLevel' t
    forall t. Integer -> SingleLevel' t
    SingleClosed Integer
    n
    levelMaxView (Max Integer
    0 (PlusLevel' t
    a:[PlusLevel' t]
    as)) = PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus PlusLevel' t
    a SingleLevel' t -> [SingleLevel' t] -> NonEmpty (SingleLevel' t)
    forall a. a -> [a] -> NonEmpty a
    :| (PlusLevel' t -> SingleLevel' t)
    -> [PlusLevel' t] -> [SingleLevel' t]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus [PlusLevel' t]
    as
    levelMaxView (Max Integer
    n [PlusLevel' t]
    as)     = Integer -> SingleLevel' t
    forall t. Integer -> SingleLevel' t
    SingleClosed Integer
    n SingleLevel' t -> [SingleLevel' t] -> NonEmpty (SingleLevel' t)
    forall a. a -> [a] -> NonEmpty a
    :| (PlusLevel' t -> SingleLevel' t)
    -> [PlusLevel' t] -> [SingleLevel' t]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus [PlusLevel' t]
    as

    singleLevelView :: Level' t -> Maybe (SingleLevel' t)
    singleLevelView :: forall t. Level' t -> Maybe (SingleLevel' t)
    singleLevelView Level' t
    l = case Level' t -> NonEmpty (SingleLevel' t)
    forall t. Level' t -> NonEmpty (SingleLevel' t)
    levelMaxView Level' t
    l of
      SingleLevel' t
    s :| [] -> SingleLevel' t -> Maybe (SingleLevel' t)
    forall a. a -> Maybe a
    Just SingleLevel' t
    s
      NonEmpty (SingleLevel' t)
    _       -> Maybe (SingleLevel' t)
    forall a. Maybe a
    Nothing

    instance Subst t => Subst (SingleLevel' t) where
      type SubstArg (SingleLevel' t) = SubstArg t

      applySubst :: Substitution' (SubstArg (SingleLevel' t))
    -> SingleLevel' t -> SingleLevel' t
    applySubst Substitution' (SubstArg (SingleLevel' t))
    sub (SingleClosed Integer
    m) = Integer -> SingleLevel' t
    forall t. Integer -> SingleLevel' t
    SingleClosed Integer
    m
      applySubst Substitution' (SubstArg (SingleLevel' t))
    sub (SinglePlus PlusLevel' t
    a)   = PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus (PlusLevel' t -> SingleLevel' t) -> PlusLevel' t -> SingleLevel' t
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (PlusLevel' t))
    -> PlusLevel' t -> PlusLevel' t
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (PlusLevel' t))
    Substitution' (SubstArg (SingleLevel' t))
    sub PlusLevel' t
    a

    instance Free t => Free (SingleLevel' t) where
      freeVars' :: forall a c. IsVarSet a c => SingleLevel' t -> FreeM a c
    freeVars' (SingleClosed Integer
    m) = FreeM a c
    forall a. Monoid a => a
    mempty
      freeVars' (SinglePlus PlusLevel' t
    a)   = PlusLevel' t -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' PlusLevel' t
    a