    module Agda.Syntax.Concrete.Definitions.Types where

    import Control.DeepSeq

    import Data.Data
    import Data.Map (Map)
    import Data.Semigroup ( Semigroup(..) )

    import GHC.Generics (Generic)

    import Agda.Syntax.Position
    import Agda.Syntax.Common hiding (TerminationCheck())
    import qualified Agda.Syntax.Common as Common
    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Name
    import Agda.Syntax.Concrete.Pretty

    import Agda.Utils.Pretty
    import Agda.Utils.Impossible
    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.List1 as List1

    {--------------------------------------------------------------------------
        Types
     --------------------------------------------------------------------------}

    {-| The nice declarations. No fixity declarations and function definitions are
        contained in a single constructor instead of spread out between type
        signatures and clauses. The @private@, @postulate@, @abstract@ and @instance@
        modifiers have been distributed to the individual declarations.

        Observe the order of components:

          Range
          Fixity'
          Access
          IsAbstract
          IsInstance
          TerminationCheck
          PositivityCheck

          further attributes

          (Q)Name

          content (Expr, Declaration ...)
    -}
    data NiceDeclaration
      = Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
          -- ^ 'IsAbstract' argument: We record whether a declaration was made in an @abstract@ block.
          --
          --   'ArgInfo' argument: Axioms and functions can be declared irrelevant.
          --   ('Hiding' should be 'NotHidden'.)
      | NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
      | PrimitiveFunction Range Access IsAbstract Name (Arg Expr)
      | NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
      | NiceModule Range Access IsAbstract QName Telescope [Declaration]
      | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
      | NiceOpen Range QName ImportDirective
      | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
      | NicePragma Range Pragma
      | NiceRecSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
      | NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
      | NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration
        -- ^ An uncategorized function clause, could be a function clause
        --   without type signature or a pattern lhs (e.g. for irrefutable let).
        --   The 'Declaration' is the actual 'FunClause'.
      | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
      | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
          -- ^ Block of function clauses (we have seen the type signature before).
          --   The 'Declaration's are the original declarations that were processed
          --   into this 'FunDef' and are only used in 'notSoNiceDeclaration'.
          --   Andreas, 2017-01-01: Because of issue #2372, we add 'IsInstance' here.
          --   An alias should know that it is an instance.
      | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
      | NiceLoneConstructor Range [NiceConstructor]
      | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]
          -- ^ @(Maybe Range)@ gives range of the 'pattern' declaration.
      | NicePatternSyn Range Access Name [Arg Name] Pattern
      | NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
      | NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
      | NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
      deriving (Typeable NiceDeclaration
    Typeable NiceDeclaration
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c NiceDeclaration)
    -> (NiceDeclaration -> Constr)
    -> (NiceDeclaration -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c NiceDeclaration))
    -> ((forall b. Data b => b -> b)
        -> NiceDeclaration -> NiceDeclaration)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> NiceDeclaration -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> NiceDeclaration -> m NiceDeclaration)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> NiceDeclaration -> m NiceDeclaration)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> NiceDeclaration -> m NiceDeclaration)
    -> Data NiceDeclaration
    NiceDeclaration -> DataType
    NiceDeclaration -> Constr
    (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
    forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NiceDeclaration
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c NiceDeclaration)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration
    gmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
    $cgmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
    gmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
    $cgmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c NiceDeclaration)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c NiceDeclaration)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
    dataTypeOf :: NiceDeclaration -> DataType
    $cdataTypeOf :: NiceDeclaration -> DataType
    toConstr :: NiceDeclaration -> Constr
    $ctoConstr :: NiceDeclaration -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NiceDeclaration
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NiceDeclaration
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
    Data, Int -> NiceDeclaration -> ShowS
    [NiceDeclaration] -> ShowS
    NiceDeclaration -> String
    (Int -> NiceDeclaration -> ShowS)
    -> (NiceDeclaration -> String)
    -> ([NiceDeclaration] -> ShowS)
    -> Show NiceDeclaration
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [NiceDeclaration] -> ShowS
    $cshowList :: [NiceDeclaration] -> ShowS
    show :: NiceDeclaration -> String
    $cshow :: NiceDeclaration -> String
    showsPrec :: Int -> NiceDeclaration -> ShowS
    $cshowsPrec :: Int -> NiceDeclaration -> ShowS
    Show, (forall x. NiceDeclaration -> Rep NiceDeclaration x)
    -> (forall x. Rep NiceDeclaration x -> NiceDeclaration)
    -> Generic NiceDeclaration
    forall x. Rep NiceDeclaration x -> NiceDeclaration
    forall x. NiceDeclaration -> Rep NiceDeclaration x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep NiceDeclaration x -> NiceDeclaration
    $cfrom :: forall x. NiceDeclaration -> Rep NiceDeclaration x
    Generic)

    instance NFData NiceDeclaration

    type TerminationCheck = Common.TerminationCheck Measure

    -- | Termination measure is, for now, a variable name.
    type Measure = Name

    type Catchall = Bool

    -- | Only 'Axiom's.
    type NiceConstructor = NiceTypeSignature

    -- | Only 'Axiom's.
    type NiceTypeSignature  = NiceDeclaration

    -- | One clause in a function definition. There is no guarantee that the 'LHS'
    --   actually declares the 'Name'. We will have to check that later.
    data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
        deriving (Typeable Clause
    Typeable Clause
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Clause -> c Clause)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Clause)
    -> (Clause -> Constr)
    -> (Clause -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Clause))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause))
    -> ((forall b. Data b => b -> b) -> Clause -> Clause)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Clause -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Clause -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Clause -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Clause -> m Clause)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Clause -> m Clause)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Clause -> m Clause)
    -> Data Clause
    Clause -> DataType
    Clause -> Constr
    (forall b. Data b => b -> b) -> Clause -> Clause
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
    forall u. (forall d. Data d => d -> u) -> Clause -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Clause
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Clause -> c Clause
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Clause)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Clause -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Clause -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
    gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
    $cgmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Clause)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Clause)
    dataTypeOf :: Clause -> DataType
    $cdataTypeOf :: Clause -> DataType
    toConstr :: Clause -> Constr
    $ctoConstr :: Clause -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Clause
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Clause
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Clause -> c Clause
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Clause -> c Clause
    Data, Int -> Clause -> ShowS
    [Clause] -> ShowS
    Clause -> String
    (Int -> Clause -> ShowS)
    -> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Clause] -> ShowS
    $cshowList :: [Clause] -> ShowS
    show :: Clause -> String
    $cshow :: Clause -> String
    showsPrec :: Int -> Clause -> ShowS
    $cshowsPrec :: Int -> Clause -> ShowS
    Show, (forall x. Clause -> Rep Clause x)
    -> (forall x. Rep Clause x -> Clause) -> Generic Clause
    forall x. Rep Clause x -> Clause
    forall x. Clause -> Rep Clause x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Clause x -> Clause
    $cfrom :: forall x. Clause -> Rep Clause x
    Generic)

    instance NFData Clause

    -- | When processing a mutual block we collect the various checks present in the block
    --   before combining them.

    data MutualChecks = MutualChecks
      { MutualChecks -> [TerminationCheck]
    mutualTermination :: [TerminationCheck]
      , MutualChecks -> [CoverageCheck]
    mutualCoverage    :: [CoverageCheck]
      , MutualChecks -> [PositivityCheck]
    mutualPositivity  :: [PositivityCheck]
      }

    instance Semigroup MutualChecks where
      MutualChecks [TerminationCheck]
    a [CoverageCheck]
    b [PositivityCheck]
    c <> :: MutualChecks -> MutualChecks -> MutualChecks
    <> MutualChecks [TerminationCheck]
    a' [CoverageCheck]
    b' [PositivityCheck]
    c'
        = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks ([TerminationCheck]
    a [TerminationCheck] -> [TerminationCheck] -> [TerminationCheck]
    forall a. Semigroup a => a -> a -> a
    <> [TerminationCheck]
    a') ([CoverageCheck]
    b [CoverageCheck] -> [CoverageCheck] -> [CoverageCheck]
    forall a. Semigroup a => a -> a -> a
    <> [CoverageCheck]
    b') ([PositivityCheck]
    c [PositivityCheck] -> [PositivityCheck] -> [PositivityCheck]
    forall a. Semigroup a => a -> a -> a
    <> [PositivityCheck]
    c')

    instance Monoid MutualChecks where
      mempty :: MutualChecks
    mempty = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [] [] []
      mappend :: MutualChecks -> MutualChecks -> MutualChecks
    mappend = MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | In an inferred `mutual' block we keep accumulating nice declarations until all
    --   of the lone signatures have an attached definition. The type is therefore a bit
    --   span-like: we return an initial segment (the inferred mutual block) together
    --   with leftovers.

    data InferredMutual = InferredMutual
      { InferredMutual -> MutualChecks
    inferredChecks    :: MutualChecks       -- checks for this block
      , InferredMutual -> [NiceDeclaration]
    inferredBlock     :: [NiceDeclaration]  -- mutual block
      , InferredMutual -> [NiceDeclaration]
    inferredLeftovers :: [NiceDeclaration]  -- leftovers
      }

    extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
    extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
    extendInferredBlock NiceDeclaration
    d (InferredMutual MutualChecks
    cs [NiceDeclaration]
    ds [NiceDeclaration]
    left) = MutualChecks
    -> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
    InferredMutual MutualChecks
    cs (NiceDeclaration
    d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    : [NiceDeclaration]
    ds) [NiceDeclaration]
    left

    -- | In an `interleaved mutual' block we collect the data signatures, function signatures,
    --   as well as their associated constructors and function clauses respectively.
    --   Each signature is given a position in the block (from 0 onwards) and each set
    --   of constructor / clauses is given a *distinct* one. This allows for interleaved
    --   forward declarations similar to what one gets in a new-style mutual block.
    type InterleavedMutual = Map Name InterleavedDecl

    data InterleavedDecl
      = InterleavedData
        { InterleavedDecl -> Int
    interleavedDeclNum  :: DeclNum
            -- ^ Internal number of the data signature.
        , InterleavedDecl -> NiceDeclaration
    interleavedDeclSig  :: NiceDeclaration
            -- ^ The data signature.
        , InterleavedDecl -> Maybe (Int, List1 [NiceDeclaration])
    interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor])
            -- ^ Constructors associated to the data signature.
        }
      | InterleavedFun
        { interleavedDeclNum  :: DeclNum
            -- ^ Internal number of the function signature.
        , interleavedDeclSig  :: NiceDeclaration
            -- ^ The function signature.
        , InterleavedDecl -> Maybe (Int, List1 ([Declaration], [Clause]))
    interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration],[Clause]))
            -- ^ Function clauses associated to the function signature.
        }

    -- | Numbering declarations in an @interleaved mutual@ block.
    type DeclNum = Int

    isInterleavedFun :: InterleavedDecl -> Maybe ()
    isInterleavedFun :: InterleavedDecl -> Maybe ()
    isInterleavedFun InterleavedFun{} = () -> Maybe ()
    forall a. a -> Maybe a
    Just ()
    isInterleavedFun InterleavedDecl
    _ = Maybe ()
    forall a. Maybe a
    Nothing

    isInterleavedData :: InterleavedDecl -> Maybe ()
    isInterleavedData :: InterleavedDecl -> Maybe ()
    isInterleavedData InterleavedData{} = () -> Maybe ()
    forall a. a -> Maybe a
    Just ()
    isInterleavedData InterleavedDecl
    _ = Maybe ()
    forall a. Maybe a
    Nothing

    interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)]
    interleavedDecl :: Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
    interleavedDecl Name
    k = \case
      InterleavedData Int
    i d :: NiceDeclaration
    d@(NiceDataSig Range
    _ Access
    acc IsAbstract
    abs PositivityCheck
    pc UniverseCheck
    uc Name
    _ [LamBinding]
    pars Expr
    _) Maybe (Int, List1 [NiceDeclaration])
    ds ->
        let fpars :: [LamBinding]
    fpars = (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap LamBinding -> [LamBinding]
    dropTypeAndModality [LamBinding]
    pars
            ddef :: [NiceDeclaration] -> NiceDeclaration
    ddef  = Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceDataDef Range
    forall a. Range' a
    noRange Origin
    UserWritten IsAbstract
    abs PositivityCheck
    pc UniverseCheck
    uc Name
    k [LamBinding]
    fpars
        in (Int
    i,NiceDeclaration
    d) (Int, NiceDeclaration)
    -> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
    forall a. a -> [a] -> [a]
    : [(Int, NiceDeclaration)]
    -> ((Int, List1 [NiceDeclaration]) -> [(Int, NiceDeclaration)])
    -> Maybe (Int, List1 [NiceDeclaration])
    -> [(Int, NiceDeclaration)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\ (Int
    j, List1 [NiceDeclaration]
    dss) -> [(Int
    j, [NiceDeclaration] -> NiceDeclaration
    ddef (List1 [NiceDeclaration] -> [NiceDeclaration]
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (List1 [NiceDeclaration] -> List1 [NiceDeclaration]
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse List1 [NiceDeclaration]
    dss)))]) Maybe (Int, List1 [NiceDeclaration])
    ds
      InterleavedFun Int
    i d :: NiceDeclaration
    d@(FunSig Range
    r Access
    acc IsAbstract
    abs IsInstance
    inst IsMacro
    mac ArgInfo
    info TerminationCheck
    tc CoverageCheck
    cc Name
    n Expr
    e) Maybe (Int, List1 ([Declaration], [Clause]))
    dcs ->
        let fdef :: List1 ([Declaration], [Clause]) -> NiceDeclaration
    fdef List1 ([Declaration], [Clause])
    dcss = let (NonEmpty [Declaration]
    dss, NonEmpty [Clause]
    css) = List1 ([Declaration], [Clause])
    -> (NonEmpty [Declaration], NonEmpty [Clause])
    forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
    List1.unzip List1 ([Declaration], [Clause])
    dcss in
                        Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceDeclaration
    FunDef Range
    r (NonEmpty [Declaration] -> [Declaration]
    forall a. Semigroup a => NonEmpty a -> a
    sconcat NonEmpty [Declaration]
    dss) IsAbstract
    abs IsInstance
    inst TerminationCheck
    tc CoverageCheck
    cc Name
    n (NonEmpty [Clause] -> [Clause]
    forall a. Semigroup a => NonEmpty a -> a
    sconcat NonEmpty [Clause]
    css)
        in (Int
    i,NiceDeclaration
    d) (Int, NiceDeclaration)
    -> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
    forall a. a -> [a] -> [a]
    : [(Int, NiceDeclaration)]
    -> ((Int, List1 ([Declaration], [Clause]))
        -> [(Int, NiceDeclaration)])
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    -> [(Int, NiceDeclaration)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\ (Int
    j, List1 ([Declaration], [Clause])
    dcss) -> [(Int
    j, List1 ([Declaration], [Clause]) -> NiceDeclaration
    fdef (List1 ([Declaration], [Clause]) -> List1 ([Declaration], [Clause])
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse List1 ([Declaration], [Clause])
    dcss))]) Maybe (Int, List1 ([Declaration], [Clause]))
    dcs
      InterleavedDecl
    _ -> [(Int, NiceDeclaration)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- someone messed up and broke the invariant

    -- | Several declarations expect only type signatures as sub-declarations.  These are:
    data KindOfBlock
      = PostulateBlock  -- ^ @postulate@
      | PrimitiveBlock  -- ^ @primitive@.  Ensured by parser.
      | InstanceBlock   -- ^ @instance@.  Actually, here all kinds of sub-declarations are allowed a priori.
      | FieldBlock      -- ^ @field@.  Ensured by parser.
      | DataBlock       -- ^ @data ... where@.  Here we got a bad error message for Agda-2.5 (Issue 1698).
      | ConstructorBlock  -- ^ @constructor@, in @interleaved mutual@.
      deriving (Typeable KindOfBlock
    Typeable KindOfBlock
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c KindOfBlock)
    -> (KindOfBlock -> Constr)
    -> (KindOfBlock -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c KindOfBlock))
    -> ((forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r)
    -> (forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
    -> Data KindOfBlock
    KindOfBlock -> DataType
    KindOfBlock -> Constr
    (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
    forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KindOfBlock
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c KindOfBlock)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
    gmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
    $cgmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c KindOfBlock)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c KindOfBlock)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
    dataTypeOf :: KindOfBlock -> DataType
    $cdataTypeOf :: KindOfBlock -> DataType
    toConstr :: KindOfBlock -> Constr
    $ctoConstr :: KindOfBlock -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KindOfBlock
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KindOfBlock
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
    Data, KindOfBlock -> KindOfBlock -> Catchall
    (KindOfBlock -> KindOfBlock -> Catchall)
    -> (KindOfBlock -> KindOfBlock -> Catchall) -> Eq KindOfBlock
    forall a. (a -> a -> Catchall) -> (a -> a -> Catchall) -> Eq a
    /= :: KindOfBlock -> KindOfBlock -> Catchall
    $c/= :: KindOfBlock -> KindOfBlock -> Catchall
    == :: KindOfBlock -> KindOfBlock -> Catchall
    $c== :: KindOfBlock -> KindOfBlock -> Catchall
    Eq, Eq KindOfBlock
    Eq KindOfBlock
    -> (KindOfBlock -> KindOfBlock -> Ordering)
    -> (KindOfBlock -> KindOfBlock -> Catchall)
    -> (KindOfBlock -> KindOfBlock -> Catchall)
    -> (KindOfBlock -> KindOfBlock -> Catchall)
    -> (KindOfBlock -> KindOfBlock -> Catchall)
    -> (KindOfBlock -> KindOfBlock -> KindOfBlock)
    -> (KindOfBlock -> KindOfBlock -> KindOfBlock)
    -> Ord KindOfBlock
    KindOfBlock -> KindOfBlock -> Catchall
    KindOfBlock -> KindOfBlock -> Ordering
    KindOfBlock -> KindOfBlock -> KindOfBlock
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Catchall)
    -> (a -> a -> Catchall)
    -> (a -> a -> Catchall)
    -> (a -> a -> Catchall)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: KindOfBlock -> KindOfBlock -> KindOfBlock
    $cmin :: KindOfBlock -> KindOfBlock -> KindOfBlock
    max :: KindOfBlock -> KindOfBlock -> KindOfBlock
    $cmax :: KindOfBlock -> KindOfBlock -> KindOfBlock
    >= :: KindOfBlock -> KindOfBlock -> Catchall
    $c>= :: KindOfBlock -> KindOfBlock -> Catchall
    > :: KindOfBlock -> KindOfBlock -> Catchall
    $c> :: KindOfBlock -> KindOfBlock -> Catchall
    <= :: KindOfBlock -> KindOfBlock -> Catchall
    $c<= :: KindOfBlock -> KindOfBlock -> Catchall
    < :: KindOfBlock -> KindOfBlock -> Catchall
    $c< :: KindOfBlock -> KindOfBlock -> Catchall
    compare :: KindOfBlock -> KindOfBlock -> Ordering
    $ccompare :: KindOfBlock -> KindOfBlock -> Ordering
    Ord, Int -> KindOfBlock -> ShowS
    [KindOfBlock] -> ShowS
    KindOfBlock -> String
    (Int -> KindOfBlock -> ShowS)
    -> (KindOfBlock -> String)
    -> ([KindOfBlock] -> ShowS)
    -> Show KindOfBlock
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [KindOfBlock] -> ShowS
    $cshowList :: [KindOfBlock] -> ShowS
    show :: KindOfBlock -> String
    $cshow :: KindOfBlock -> String
    showsPrec :: Int -> KindOfBlock -> ShowS
    $cshowsPrec :: Int -> KindOfBlock -> ShowS
    Show)

    instance HasRange NiceDeclaration where
      getRange :: NiceDeclaration -> Range
    getRange (Axiom Range
    r Access
    _ IsAbstract
    _ IsInstance
    _ ArgInfo
    _ Name
    _ Expr
    _)           = Range
    r
      getRange (NiceField Range
    r Access
    _ IsAbstract
    _ IsInstance
    _ TacticAttribute
    _ Name
    _ Arg Expr
    _)       = Range
    r
      getRange (NiceMutual Range
    r TerminationCheck
    _ CoverageCheck
    _ PositivityCheck
    _ [NiceDeclaration]
    _)          = Range
    r
      getRange (NiceModule Range
    r Access
    _ IsAbstract
    _ QName
    _ Telescope
    _ [Declaration]
    _ )       = Range
    r
      getRange (NiceModuleMacro Range
    r Access
    _ Name
    _ ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _)   = Range
    r
      getRange (NiceOpen Range
    r QName
    _ ImportDirective
    _)                = Range
    r
      getRange (NiceImport Range
    r QName
    _ Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _)          = Range
    r
      getRange (NicePragma Range
    r Pragma
    _)                = Range
    r
      getRange (PrimitiveFunction Range
    r Access
    _ IsAbstract
    _ Name
    _ Arg Expr
    _)   = Range
    r
      getRange (FunSig Range
    r Access
    _ IsAbstract
    _ IsInstance
    _ IsMacro
    _ ArgInfo
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    _ Expr
    _)    = Range
    r
      getRange (FunDef Range
    r [Declaration]
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    _ [Clause]
    _)        = Range
    r
      getRange (NiceDataDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [LamBinding]
    _ [NiceDeclaration]
    _)   = Range
    r
      getRange (NiceLoneConstructor Range
    r [NiceDeclaration]
    _)       = Range
    r
      getRange (NiceRecDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ RecordDirectives
    _ [LamBinding]
    _ [Declaration]
    _)  = Range
    r
      getRange (NiceRecSig Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _)    = Range
    r
      getRange (NiceDataSig Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _)   = Range
    r
      getRange (NicePatternSyn Range
    r Access
    _ Name
    _ [Arg Name]
    _ Pattern
    _)      = Range
    r
      getRange (NiceGeneralize Range
    r Access
    _ ArgInfo
    _ TacticAttribute
    _ Name
    _ Expr
    _)    = Range
    r
      getRange (NiceFunClause Range
    r Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ Catchall
    _ Declaration
    _)   = Range
    r
      getRange (NiceUnquoteDecl Range
    r Access
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    _ Expr
    _) = Range
    r
      getRange (NiceUnquoteDef Range
    r Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    _ Expr
    _)    = Range
    r

    instance Pretty NiceDeclaration where
      pretty :: NiceDeclaration -> Doc
    pretty = \case
        Axiom Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ ArgInfo
    _ Name
    x Expr
    _            -> String -> Doc
    text String
    "postulate" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> Doc
    colon Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "_"
        NiceField Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ TacticAttribute
    _ Name
    x Arg Expr
    _        -> String -> Doc
    text String
    "field" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        PrimitiveFunction Range
    _ Access
    _ IsAbstract
    _ Name
    x Arg Expr
    _    -> String -> Doc
    text String
    "primitive" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceMutual{}                   -> String -> Doc
    text String
    "mutual"
        NiceModule Range
    _ Access
    _ IsAbstract
    _ QName
    x Telescope
    _ [Declaration]
    _         -> String -> Doc
    text String
    "module" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "where"
        NiceModuleMacro Range
    _ Access
    _ Name
    x ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _    -> String -> Doc
    text String
    "module" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "= ..."
        NiceOpen Range
    _ QName
    x ImportDirective
    _                 -> String -> Doc
    text String
    "open" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
        NiceImport Range
    _ QName
    x Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _           -> String -> Doc
    text String
    "import" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
        NicePragma{}                   -> String -> Doc
    text String
    "{-# ... #-}"
        NiceRecSig Range
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    _ Expr
    _     -> String -> Doc
    text String
    "record" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceDataSig Range
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    _ Expr
    _    -> String -> Doc
    text String
    "data" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceFunClause{}                -> String -> Doc
    text String
    "<function clause>"
        FunSig Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ IsMacro
    _ ArgInfo
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    x Expr
    _     -> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> Doc
    colon Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "_"
        FunDef Range
    _ [Declaration]
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    x [Clause]
    _         -> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "= _"
        NiceDataDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    _ [NiceDeclaration]
    _    -> String -> Doc
    text String
    "data" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "where"
        NiceLoneConstructor Range
    _ [NiceDeclaration]
    ds       -> String -> Doc
    text String
    "constructor"
        NiceRecDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x  RecordDirectives
    _ [LamBinding]
    _ [Declaration]
    _  -> String -> Doc
    text String
    "record" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "where"
        NicePatternSyn Range
    _ Access
    _ Name
    x [Arg Name]
    _ Pattern
    _       -> String -> Doc
    text String
    "pattern" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceGeneralize Range
    _ Access
    _ ArgInfo
    _ TacticAttribute
    _ Name
    x Expr
    _     -> String -> Doc
    text String
    "variable" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceUnquoteDecl Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    xs Expr
    _ -> String -> Doc
    text String
    "<unquote declarations>"
        NiceUnquoteDef Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    xs Expr
    _    -> String -> Doc
    text String
    "<unquote definitions>"

    declName :: NiceDeclaration -> String
    declName :: NiceDeclaration -> String
    declName Axiom{}             = String
    "Postulates"
    declName NiceField{}         = String
    "Fields"
    declName NiceMutual{}        = String
    "Mutual blocks"
    declName NiceModule{}        = String
    "Modules"
    declName NiceModuleMacro{}   = String
    "Modules"
    declName NiceOpen{}          = String
    "Open declarations"
    declName NiceImport{}        = String
    "Import statements"
    declName NicePragma{}        = String
    "Pragmas"
    declName PrimitiveFunction{} = String
    "Primitive declarations"
    declName NicePatternSyn{}    = String
    "Pattern synonyms"
    declName NiceGeneralize{}    = String
    "Generalized variables"
    declName NiceUnquoteDecl{}   = String
    "Unquoted declarations"
    declName NiceUnquoteDef{}    = String
    "Unquoted definitions"
    declName NiceRecSig{}        = String
    "Records"
    declName NiceDataSig{}       = String
    "Data types"
    declName NiceFunClause{}     = String
    "Functions without a type signature"
    declName FunSig{}            = String
    "Type signatures"
    declName FunDef{}            = String
    "Function definitions"
    declName NiceRecDef{}        = String
    "Records"
    declName NiceDataDef{}       = String
    "Data types"
    declName NiceLoneConstructor{} = String
    "Constructors"

    data InMutual
      = InMutual    -- ^ we are nicifying a mutual block
      | NotInMutual -- ^ we are nicifying decls not in a mutual block
        deriving (InMutual -> InMutual -> Catchall
    (InMutual -> InMutual -> Catchall)
    -> (InMutual -> InMutual -> Catchall) -> Eq InMutual
    forall a. (a -> a -> Catchall) -> (a -> a -> Catchall) -> Eq a
    /= :: InMutual -> InMutual -> Catchall
    $c/= :: InMutual -> InMutual -> Catchall
    == :: InMutual -> InMutual -> Catchall
    $c== :: InMutual -> InMutual -> Catchall
    Eq, Int -> InMutual -> ShowS
    [InMutual] -> ShowS
    InMutual -> String
    (Int -> InMutual -> ShowS)
    -> (InMutual -> String) -> ([InMutual] -> ShowS) -> Show InMutual
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [InMutual] -> ShowS
    $cshowList :: [InMutual] -> ShowS
    show :: InMutual -> String
    $cshow :: InMutual -> String
    showsPrec :: Int -> InMutual -> ShowS
    $cshowsPrec :: Int -> InMutual -> ShowS
    Show)

    -- | The kind of the forward declaration.

    data DataRecOrFun
      = DataName
        { DataRecOrFun -> PositivityCheck
    _kindPosCheck :: PositivityCheck
        , DataRecOrFun -> UniverseCheck
    _kindUniCheck :: UniverseCheck
        }
        -- ^ Name of a data type
      | RecName
        { _kindPosCheck :: PositivityCheck
        , _kindUniCheck :: UniverseCheck
        }
        -- ^ Name of a record type
      | FunName TerminationCheck CoverageCheck
        -- ^ Name of a function.
      deriving (Typeable DataRecOrFun
    Typeable DataRecOrFun
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c DataRecOrFun)
    -> (DataRecOrFun -> Constr)
    -> (DataRecOrFun -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c DataRecOrFun))
    -> ((forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r)
    -> (forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
    -> Data DataRecOrFun
    DataRecOrFun -> DataType
    DataRecOrFun -> Constr
    (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
    forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataRecOrFun
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DataRecOrFun)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
    gmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
    $cgmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DataRecOrFun)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DataRecOrFun)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
    dataTypeOf :: DataRecOrFun -> DataType
    $cdataTypeOf :: DataRecOrFun -> DataType
    toConstr :: DataRecOrFun -> Constr
    $ctoConstr :: DataRecOrFun -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataRecOrFun
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataRecOrFun
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
    Data, Int -> DataRecOrFun -> ShowS
    [DataRecOrFun] -> ShowS
    DataRecOrFun -> String
    (Int -> DataRecOrFun -> ShowS)
    -> (DataRecOrFun -> String)
    -> ([DataRecOrFun] -> ShowS)
    -> Show DataRecOrFun
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [DataRecOrFun] -> ShowS
    $cshowList :: [DataRecOrFun] -> ShowS
    show :: DataRecOrFun -> String
    $cshow :: DataRecOrFun -> String
    showsPrec :: Int -> DataRecOrFun -> ShowS
    $cshowsPrec :: Int -> DataRecOrFun -> ShowS
    Show)

    -- Ignore pragmas when checking equality
    instance Eq DataRecOrFun where
      DataName{} == :: DataRecOrFun -> DataRecOrFun -> Catchall
    == DataName{} = Catchall
    True
      RecName{}  == RecName{}  = Catchall
    True
      FunName{}  == FunName{}  = Catchall
    True
      DataRecOrFun
    _          == DataRecOrFun
    _          = Catchall
    False

    instance Pretty DataRecOrFun where
      pretty :: DataRecOrFun -> Doc
    pretty DataName{} = Doc
    "data type"
      pretty RecName{}  = Doc
    "record type"
      pretty FunName{}  = Doc
    "function"

    isFunName :: DataRecOrFun -> Bool
    isFunName :: DataRecOrFun -> Catchall
    isFunName (FunName{}) = Catchall
    True
    isFunName DataRecOrFun
    _           = Catchall
    False

    sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
    sameKind :: DataRecOrFun -> DataRecOrFun -> Catchall
    sameKind = DataRecOrFun -> DataRecOrFun -> Catchall
    forall a. Eq a => a -> a -> Catchall
    (==)

    terminationCheck :: DataRecOrFun -> TerminationCheck
    terminationCheck :: DataRecOrFun -> TerminationCheck
    terminationCheck (FunName TerminationCheck
    tc CoverageCheck
    _) = TerminationCheck
    tc
    terminationCheck DataRecOrFun
    _ = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck

    coverageCheck :: DataRecOrFun -> CoverageCheck
    coverageCheck :: DataRecOrFun -> CoverageCheck
    coverageCheck (FunName TerminationCheck
    _ CoverageCheck
    cc) = CoverageCheck
    cc
    coverageCheck DataRecOrFun
    _ = CoverageCheck
    YesCoverageCheck

    positivityCheck :: DataRecOrFun -> PositivityCheck
    positivityCheck :: DataRecOrFun -> PositivityCheck
    positivityCheck (DataName PositivityCheck
    pc UniverseCheck
    _) = PositivityCheck
    pc
    positivityCheck (RecName PositivityCheck
    pc UniverseCheck
    _)  = PositivityCheck
    pc
    positivityCheck (FunName TerminationCheck
    _ CoverageCheck
    _)   = PositivityCheck
    YesPositivityCheck

    mutualChecks :: DataRecOrFun -> MutualChecks
    mutualChecks :: DataRecOrFun -> MutualChecks
    mutualChecks DataRecOrFun
    k = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [DataRecOrFun -> TerminationCheck
    terminationCheck DataRecOrFun
    k] [DataRecOrFun -> CoverageCheck
    coverageCheck DataRecOrFun
    k] [DataRecOrFun -> PositivityCheck
    positivityCheck DataRecOrFun
    k]

    universeCheck :: DataRecOrFun -> UniverseCheck
    universeCheck :: DataRecOrFun -> UniverseCheck
    universeCheck (DataName PositivityCheck
    _ UniverseCheck
    uc) = UniverseCheck
    uc
    universeCheck (RecName PositivityCheck
    _ UniverseCheck
    uc)  = UniverseCheck
    uc
    universeCheck (FunName TerminationCheck
    _ CoverageCheck
    _)   = UniverseCheck
    YesUniverseCheck