    module Agda.Syntax.Internal
        ( module Agda.Syntax.Internal
        , module Agda.Syntax.Internal.Blockers
        , module Agda.Syntax.Internal.Elim
        , module Agda.Syntax.Internal.Univ
        , module Agda.Syntax.Abstract.Name
        , MetaId(..), ProblemId(..)
        ) where

    import Prelude hiding (null)

    import Control.Monad.Identity
    import Control.DeepSeq

    import Data.Function (on)
    import qualified Data.List as List
    import Data.Maybe
    import Data.Semigroup ( Semigroup, (<>), Sum(..) )

    import GHC.Generics (Generic)

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Literal
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Internal.Blockers
    import Agda.Syntax.Internal.Elim
    import Agda.Syntax.Internal.Univ
    import Agda.Syntax.Common.Pretty

    import Agda.Utils.CallStack
        ( CallStack
        , HasCallStack
        , prettyCallSite
        , headCallSite
        , withCallerCallStack
        )

    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.Null
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Function type domain
    ---------------------------------------------------------------------------

    -- | Similar to 'Arg', but we need to distinguish
    --   an irrelevance annotation in a function domain
    --   (the domain itself is not irrelevant!)
    --   from an irrelevant argument.
    --
    --   @Dom@ is used in 'Pi' of internal syntax, in 'Context' and 'Telescope'.
    --   'Arg' is used for actual arguments ('Var', 'Con', 'Def' etc.)
    --   and in 'Abstract' syntax and other situations.
    --
    --   [ cubical ] When @annFinite (argInfoAnnotation domInfo) = True@ for
    --   the domain of a 'Pi' type, the elements should be compared by
    --   tabulating the domain type.  Only supported in case the domain type
    --   is primIsOne, to obtain the correct equality for partial elements.
    --
    data Dom' t e = Dom
      { forall t e. Dom' t e -> ArgInfo
    domInfo   :: ArgInfo
      , forall t e. Dom' t e -> Maybe NamedName
    domName   :: Maybe NamedName  -- ^ e.g. @x@ in @{x = y : A} -> B@.
      , forall t e. Dom' t e -> Bool
    domIsFinite :: Bool
        -- ^ Is this a Π-type (False), or a partial type (True)?
      , forall t e. Dom' t e -> Maybe t
    domTactic :: Maybe t        -- ^ "@tactic e".
      , forall t e. Dom' t e -> e
    unDom     :: e
      } deriving (Int -> Dom' t e -> ShowS
    [Dom' t e] -> ShowS
    Dom' t e -> [Char]
    (Int -> Dom' t e -> ShowS)
    -> (Dom' t e -> [Char]) -> ([Dom' t e] -> ShowS) -> Show (Dom' t e)
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
    forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
    forall t e. (Show t, Show e) => Dom' t e -> [Char]
    $cshowsPrec :: forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
    showsPrec :: Int -> Dom' t e -> ShowS
    $cshow :: forall t e. (Show t, Show e) => Dom' t e -> [Char]
    show :: Dom' t e -> [Char]
    $cshowList :: forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
    showList :: [Dom' t e] -> ShowS
    Show, (forall a b. (a -> b) -> Dom' t a -> Dom' t b)
    -> (forall a b. a -> Dom' t b -> Dom' t a) -> Functor (Dom' t)
    forall a b. a -> Dom' t b -> Dom' t a
    forall a b. (a -> b) -> Dom' t a -> Dom' t b
    forall t a b. a -> Dom' t b -> Dom' t a
    forall t a b. (a -> b) -> Dom' t a -> Dom' t b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall t a b. (a -> b) -> Dom' t a -> Dom' t b
    fmap :: forall a b. (a -> b) -> Dom' t a -> Dom' t b
    $c<$ :: forall t a b. a -> Dom' t b -> Dom' t a
    <$ :: forall a b. a -> Dom' t b -> Dom' t a
    Functor, (forall m. Monoid m => Dom' t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Dom' t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Dom' t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Dom' t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Dom' t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Dom' t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Dom' t a -> b)
    -> (forall a. (a -> a -> a) -> Dom' t a -> a)
    -> (forall a. (a -> a -> a) -> Dom' t a -> a)
    -> (forall a. Dom' t a -> [a])
    -> (forall a. Dom' t a -> Bool)
    -> (forall a. Dom' t a -> Int)
    -> (forall a. Eq a => a -> Dom' t a -> Bool)
    -> (forall a. Ord a => Dom' t a -> a)
    -> (forall a. Ord a => Dom' t a -> a)
    -> (forall a. Num a => Dom' t a -> a)
    -> (forall a. Num a => Dom' t a -> a)
    -> Foldable (Dom' t)
    forall a. Eq a => a -> Dom' t a -> Bool
    forall a. Num a => Dom' t a -> a
    forall a. Ord a => Dom' t a -> a
    forall m. Monoid m => Dom' t m -> m
    forall a. Dom' t a -> Bool
    forall a. Dom' t a -> Int
    forall a. Dom' t a -> [a]
    forall a. (a -> a -> a) -> Dom' t a -> a
    forall t a. Eq a => a -> Dom' t a -> Bool
    forall t a. Num a => Dom' t a -> a
    forall t a. Ord a => Dom' t a -> a
    forall m a. Monoid m => (a -> m) -> Dom' t a -> m
    forall t m. Monoid m => Dom' t m -> m
    forall t e. Dom' t e -> Bool
    forall t a. Dom' t a -> Int
    forall t a. Dom' t a -> [a]
    forall b a. (b -> a -> b) -> b -> Dom' t a -> b
    forall a b. (a -> b -> b) -> b -> Dom' t a -> b
    forall t a. (a -> a -> a) -> Dom' t a -> a
    forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
    forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
    forall t a b. (a -> b -> b) -> b -> Dom' t 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 -> Int)
    -> (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
    $cfold :: forall t m. Monoid m => Dom' t m -> m
    fold :: forall m. Monoid m => Dom' t m -> m
    $cfoldMap :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
    $cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
    $cfoldr :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
    $cfoldr' :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
    $cfoldl :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
    $cfoldl' :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
    $cfoldr1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
    foldr1 :: forall a. (a -> a -> a) -> Dom' t a -> a
    $cfoldl1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
    foldl1 :: forall a. (a -> a -> a) -> Dom' t a -> a
    $ctoList :: forall t a. Dom' t a -> [a]
    toList :: forall a. Dom' t a -> [a]
    $cnull :: forall t e. Dom' t e -> Bool
    null :: forall a. Dom' t a -> Bool
    $clength :: forall t a. Dom' t a -> Int
    length :: forall a. Dom' t a -> Int
    $celem :: forall t a. Eq a => a -> Dom' t a -> Bool
    elem :: forall a. Eq a => a -> Dom' t a -> Bool
    $cmaximum :: forall t a. Ord a => Dom' t a -> a
    maximum :: forall a. Ord a => Dom' t a -> a
    $cminimum :: forall t a. Ord a => Dom' t a -> a
    minimum :: forall a. Ord a => Dom' t a -> a
    $csum :: forall t a. Num a => Dom' t a -> a
    sum :: forall a. Num a => Dom' t a -> a
    $cproduct :: forall t a. Num a => Dom' t a -> a
    product :: forall a. Num a => Dom' t a -> a
    Foldable, Functor (Dom' t)
    Foldable (Dom' t)
    (Functor (Dom' t), Foldable (Dom' t)) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Dom' t a -> f (Dom' t b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Dom' t (f a) -> f (Dom' t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Dom' t a -> m (Dom' t b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Dom' t (m a) -> m (Dom' t a))
    -> Traversable (Dom' t)
    forall t. Functor (Dom' t)
    forall t. Foldable (Dom' t)
    forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
    forall t (f :: * -> *) a.
    Applicative f =>
    Dom' t (f a) -> f (Dom' t a)
    forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dom' t a -> m (Dom' t b)
    forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' t a -> f (Dom' t b)
    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 => Dom' t (m a) -> m (Dom' t a)
    forall (f :: * -> *) a.
    Applicative f =>
    Dom' t (f a) -> f (Dom' t a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dom' t a -> m (Dom' t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' t a -> f (Dom' t b)
    $ctraverse :: forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' t a -> f (Dom' t b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' t a -> f (Dom' t b)
    $csequenceA :: forall t (f :: * -> *) a.
    Applicative f =>
    Dom' t (f a) -> f (Dom' t a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Dom' t (f a) -> f (Dom' t a)
    $cmapM :: forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dom' t a -> m (Dom' t b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dom' t a -> m (Dom' t b)
    $csequence :: forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
    sequence :: forall (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
    Traversable)

    type Dom = Dom' Term

    instance Decoration (Dom' t) where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Dom' t a -> m (Dom' t b)
    traverseF a -> m b
    f (Dom ArgInfo
    ai Maybe NamedName
    x Bool
    t Maybe t
    b a
    a) = ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> b -> Dom' t b
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom ArgInfo
    ai Maybe NamedName
    x Bool
    t Maybe t
    b (b -> Dom' t b) -> m b -> m (Dom' t b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    a

    instance HasRange a => HasRange (Dom' t a) where
      getRange :: Dom' t a -> Range
    getRange = a -> Range
    forall a. HasRange a => a -> Range
    getRange (a -> Range) -> (Dom' t a -> a) -> Dom' t a -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' t a -> a
    forall t e. Dom' t e -> e
    unDom

    instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
      killRange :: KillRangeT (Dom' t a)
    killRange (Dom ArgInfo
    info Maybe NamedName
    x Bool
    t Maybe t
    b a
    a) = (ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a)
    -> ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom ArgInfo
    info Maybe NamedName
    x Bool
    t Maybe t
    b a
    a

    -- | Ignores 'Origin' and 'FreeVariables' and tactic.
    instance Eq a => Eq (Dom' t a) where
      Dom (ArgInfo Hiding
    h1 Modality
    m1 Origin
    _ FreeVariables
    _ Annotation
    a1) Maybe NamedName
    s1 Bool
    f1 Maybe t
    _ a
    x1 == :: Dom' t a -> Dom' t a -> Bool
    == Dom (ArgInfo Hiding
    h2 Modality
    m2 Origin
    _ FreeVariables
    _ Annotation
    a2) Maybe NamedName
    s2 Bool
    f2 Maybe t
    _ a
    x2 =
        (Hiding
    h1, Modality
    m1, Annotation
    a1, Maybe NamedName
    s1, Bool
    f1, a
    x1) (Hiding, Modality, Annotation, Maybe NamedName, Bool, a)
    -> (Hiding, Modality, Annotation, Maybe NamedName, Bool, a) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Hiding
    h2, Modality
    m2, Annotation
    a2, Maybe NamedName
    s2, Bool
    f2, a
    x2)

    instance LensNamed (Dom' t e) where
      type NameOf (Dom' t e) = NamedName
      lensNamed :: Lens' (Dom' t e) (Maybe (NameOf (Dom' t e)))
    lensNamed Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
    f Dom' t e
    dom = Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
    f (Dom' t e -> Maybe NamedName
    forall t e. Dom' t e -> Maybe NamedName
    domName Dom' t e
    dom) f (Maybe NamedName)
    -> (Maybe NamedName -> Dom' t e) -> f (Dom' t e)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Maybe NamedName
    nm -> Dom' t e
    dom { domName = nm }

    instance LensArgInfo (Dom' t e) where
      getArgInfo :: Dom' t e -> ArgInfo
    getArgInfo        = Dom' t e -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo
      setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e
    setArgInfo ArgInfo
    ai Dom' t e
    dom = Dom' t e
    dom { domInfo = ai }
      mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e
    mapArgInfo ArgInfo -> ArgInfo
    f  Dom' t e
    dom = Dom' t e
    dom { domInfo = f $ domInfo dom }

    instance LensLock (Dom' t e) where
      getLock :: Dom' t e -> Lock
    getLock = ArgInfo -> Lock
    forall a. LensLock a => a -> Lock
    getLock (ArgInfo -> Lock) -> (Dom' t e -> ArgInfo) -> Dom' t e -> Lock
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' t e -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo
      setLock :: Lock -> Dom' t e -> Dom' t e
    setLock = (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e
    forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
    mapArgInfo ((ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e)
    -> (Lock -> ArgInfo -> ArgInfo) -> Lock -> Dom' t e -> Dom' t e
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lock -> ArgInfo -> ArgInfo
    forall a. LensLock a => Lock -> a -> a
    setLock

    -- The other lenses are defined through LensArgInfo

    instance LensHiding        (Dom' t e) where
    instance LensModality      (Dom' t e) where
    instance LensOrigin        (Dom' t e) where
    instance LensFreeVariables (Dom' t e) where
    instance LensAnnotation    (Dom' t e) where

    -- Since we have LensModality, we get relevance and quantity by default

    instance LensRelevance (Dom' t e) where
    instance LensQuantity  (Dom' t e) where
    instance LensCohesion  (Dom' t e) where
    instance LensModalPolarity (Dom' t e) where

    argFromDom :: Dom' t a -> Arg a
    argFromDom :: forall t a. Dom' t a -> Arg a
    argFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    i, unDom :: forall t e. Dom' t e -> e
    unDom = a
    a} = ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i a
    a

    namedArgFromDom :: Dom' t a -> NamedArg a
    namedArgFromDom :: forall t a. Dom' t a -> NamedArg a
    namedArgFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    i, domName :: forall t e. Dom' t e -> Maybe NamedName
    domName = Maybe NamedName
    s, unDom :: forall t e. Dom' t e -> e
    unDom = a
    a} = ArgInfo -> Named_ a -> Arg (Named_ a)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Named_ a -> Arg (Named_ a)) -> Named_ a -> Arg (Named_ a)
    forall a b. (a -> b) -> a -> b
    $ Maybe NamedName -> a -> Named_ a
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    s a
    a

    -- The following functions are less general than they could be:
    -- @Dom@ could be replaced by @Dom' t@.
    -- However, this causes problems with instance resolution in several places.
    -- often for class AddContext.

    domFromArg :: Arg a -> Dom a
    domFromArg :: forall a. Arg a -> Dom a
    domFromArg (Arg ArgInfo
    i a
    a) = ArgInfo
    -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom' Term a
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom ArgInfo
    i Maybe NamedName
    forall a. Maybe a
    Nothing Bool
    False Maybe Term
    forall a. Maybe a
    Nothing a
    a

    domFromNamedArg :: NamedArg a -> Dom a
    domFromNamedArg :: forall a. NamedArg a -> Dom a
    domFromNamedArg (Arg ArgInfo
    i Named_ a
    a) = ArgInfo
    -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom' Term a
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom ArgInfo
    i (Named_ a -> Maybe NamedName
    forall name a. Named name a -> Maybe name
    nameOf Named_ a
    a) Bool
    False Maybe Term
    forall a. Maybe a
    Nothing (Named_ a -> a
    forall name a. Named name a -> a
    namedThing Named_ a
    a)

    defaultDom :: a -> Dom a
    defaultDom :: forall a. a -> Dom a
    defaultDom = ArgInfo -> a -> Dom a
    forall a. ArgInfo -> a -> Dom a
    defaultArgDom ArgInfo
    defaultArgInfo

    defaultArgDom :: ArgInfo -> a -> Dom a
    defaultArgDom :: forall a. ArgInfo -> a -> Dom a
    defaultArgDom ArgInfo
    info a
    x = Arg a -> Dom a
    forall a. Arg a -> Dom a
    domFromArg (ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info a
    x)

    defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
    defaultNamedArgDom :: forall a. ArgInfo -> [Char] -> a -> Dom a
    defaultNamedArgDom ArgInfo
    info [Char]
    s a
    x = (ArgInfo -> a -> Dom' Term a
    forall a. ArgInfo -> a -> Dom a
    defaultArgDom ArgInfo
    info a
    x) { domName = Just $ WithOrigin Inserted $ unranged s }

    -- | Type of argument lists.
    --
    type Args       = [Arg Term]
    type NamedArgs  = [NamedArg Term]

    data DataOrRecord' p
      = IsData
      | IsRecord p
      deriving (Int -> DataOrRecord' p -> ShowS
    [DataOrRecord' p] -> ShowS
    DataOrRecord' p -> [Char]
    (Int -> DataOrRecord' p -> ShowS)
    -> (DataOrRecord' p -> [Char])
    -> ([DataOrRecord' p] -> ShowS)
    -> Show (DataOrRecord' p)
    forall p. Show p => Int -> DataOrRecord' p -> ShowS
    forall p. Show p => [DataOrRecord' p] -> ShowS
    forall p. Show p => DataOrRecord' p -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall p. Show p => Int -> DataOrRecord' p -> ShowS
    showsPrec :: Int -> DataOrRecord' p -> ShowS
    $cshow :: forall p. Show p => DataOrRecord' p -> [Char]
    show :: DataOrRecord' p -> [Char]
    $cshowList :: forall p. Show p => [DataOrRecord' p] -> ShowS
    showList :: [DataOrRecord' p] -> ShowS
    Show, DataOrRecord' p -> DataOrRecord' p -> Bool
    (DataOrRecord' p -> DataOrRecord' p -> Bool)
    -> (DataOrRecord' p -> DataOrRecord' p -> Bool)
    -> Eq (DataOrRecord' p)
    forall p. Eq p => DataOrRecord' p -> DataOrRecord' p -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall p. Eq p => DataOrRecord' p -> DataOrRecord' p -> Bool
    == :: DataOrRecord' p -> DataOrRecord' p -> Bool
    $c/= :: forall p. Eq p => DataOrRecord' p -> DataOrRecord' p -> Bool
    /= :: DataOrRecord' p -> DataOrRecord' p -> Bool
    Eq, (forall x. DataOrRecord' p -> Rep (DataOrRecord' p) x)
    -> (forall x. Rep (DataOrRecord' p) x -> DataOrRecord' p)
    -> Generic (DataOrRecord' p)
    forall x. Rep (DataOrRecord' p) x -> DataOrRecord' p
    forall x. DataOrRecord' p -> Rep (DataOrRecord' p) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall p x. Rep (DataOrRecord' p) x -> DataOrRecord' p
    forall p x. DataOrRecord' p -> Rep (DataOrRecord' p) x
    $cfrom :: forall p x. DataOrRecord' p -> Rep (DataOrRecord' p) x
    from :: forall x. DataOrRecord' p -> Rep (DataOrRecord' p) x
    $cto :: forall p x. Rep (DataOrRecord' p) x -> DataOrRecord' p
    to :: forall x. Rep (DataOrRecord' p) x -> DataOrRecord' p
    Generic)

    type DataOrRecord = DataOrRecord' PatternOrCopattern
    type DataOrRecord_ = DataOrRecord' ()

    pattern IsRecord_ :: DataOrRecord_
    pattern $mIsRecord_ :: forall {r}. DataOrRecord_ -> ((# #) -> r) -> ((# #) -> r) -> r
    $bIsRecord_ :: DataOrRecord_
    IsRecord_ = IsRecord ()

    instance PatternMatchingAllowed DataOrRecord where
      patternMatchingAllowed :: DataOrRecord -> Bool
    patternMatchingAllowed = \case
        DataOrRecord
    IsData -> Bool
    True
        IsRecord PatternOrCopattern
    patCopat -> PatternOrCopattern -> Bool
    forall a. PatternMatchingAllowed a => a -> Bool
    patternMatchingAllowed PatternOrCopattern
    patCopat

    instance CopatternMatchingAllowed DataOrRecord where
      copatternMatchingAllowed :: DataOrRecord -> Bool
    copatternMatchingAllowed = \case
        DataOrRecord
    IsData -> Bool
    False
        IsRecord PatternOrCopattern
    patCopat -> PatternOrCopattern -> Bool
    forall a. CopatternMatchingAllowed a => a -> Bool
    copatternMatchingAllowed PatternOrCopattern
    patCopat

    -- | Store the names of the record fields in the constructor.
    --   This allows reduction of projection redexes outside of TCM.
    --   For instance, during substitution and application.
    data ConHead = ConHead
      { ConHead -> QName
    conName       :: QName         -- ^ The name of the constructor.
      , ConHead -> DataOrRecord
    conDataRecord :: DataOrRecord  -- ^ Data or record constructor?
      , ConHead -> Induction
    conInductive  :: Induction     -- ^ Record constructors can be coinductive.
      , ConHead -> [Arg QName]
    conFields     :: [Arg QName]   -- ^ The name of the record fields.
          --   'Arg' is stored since the info in the constructor args
          --   might not be accurate because of subtyping (issue #2170).
      } deriving (Int -> ConHead -> ShowS
    [ConHead] -> ShowS
    ConHead -> [Char]
    (Int -> ConHead -> ShowS)
    -> (ConHead -> [Char]) -> ([ConHead] -> ShowS) -> Show ConHead
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ConHead -> ShowS
    showsPrec :: Int -> ConHead -> ShowS
    $cshow :: ConHead -> [Char]
    show :: ConHead -> [Char]
    $cshowList :: [ConHead] -> ShowS
    showList :: [ConHead] -> ShowS
    Show, (forall x. ConHead -> Rep ConHead x)
    -> (forall x. Rep ConHead x -> ConHead) -> Generic ConHead
    forall x. Rep ConHead x -> ConHead
    forall x. ConHead -> Rep ConHead x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ConHead -> Rep ConHead x
    from :: forall x. ConHead -> Rep ConHead x
    $cto :: forall x. Rep ConHead x -> ConHead
    to :: forall x. Rep ConHead x -> ConHead
    Generic)

    instance Eq ConHead where
      == :: ConHead -> ConHead -> Bool
    (==) = QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (QName -> QName -> Bool)
    -> (ConHead -> QName) -> ConHead -> ConHead -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` ConHead -> QName
    conName

    instance Ord ConHead where
      <= :: ConHead -> ConHead -> Bool
    (<=) = QName -> QName -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) (QName -> QName -> Bool)
    -> (ConHead -> QName) -> ConHead -> ConHead -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` ConHead -> QName
    conName

    instance Pretty ConHead where
      pretty :: ConHead -> Doc Aspects
    pretty = QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (QName -> Doc Aspects)
    -> (ConHead -> QName) -> ConHead -> Doc Aspects
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName

    instance HasRange ConHead where
      getRange :: ConHead -> Range
    getRange = QName -> Range
    forall a. HasRange a => a -> Range
    getRange (QName -> Range) -> (ConHead -> QName) -> ConHead -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName

    instance SetRange ConHead where
      setRange :: Range -> ConHead -> ConHead
    setRange Range
    r = (QName -> QName) -> ConHead -> ConHead
    forall a. LensConName a => (QName -> QName) -> a -> a
    mapConName (Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r)

    instance CopatternMatchingAllowed ConHead where
      copatternMatchingAllowed :: ConHead -> Bool
    copatternMatchingAllowed = DataOrRecord -> Bool
    forall a. CopatternMatchingAllowed a => a -> Bool
    copatternMatchingAllowed (DataOrRecord -> Bool)
    -> (ConHead -> DataOrRecord) -> ConHead -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> DataOrRecord
    conDataRecord

    class LensConName a where
      getConName :: a -> QName
      setConName :: QName -> a -> a
      setConName = (QName -> QName) -> a -> a
    forall a. LensConName a => (QName -> QName) -> a -> a
    mapConName ((QName -> QName) -> a -> a)
    -> (QName -> QName -> QName) -> QName -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> QName -> QName
    forall a b. a -> b -> a
    const
      mapConName :: (QName -> QName) -> a -> a
      mapConName QName -> QName
    f a
    a = QName -> a -> a
    forall a. LensConName a => QName -> a -> a
    setConName (QName -> QName
    f (a -> QName
    forall a. LensConName a => a -> QName
    getConName a
    a)) a
    a

    instance LensConName ConHead where
      getConName :: ConHead -> QName
    getConName = ConHead -> QName
    conName
      setConName :: QName -> ConHead -> ConHead
    setConName QName
    c ConHead
    con = ConHead
    con { conName = c }

    -- | Raw values.
    --
    --   @Def@ is used for both defined and undefined constants.
    --   Assume there is a type declaration and a definition for
    --     every constant, even if the definition is an empty
    --     list of clauses.
    --
    data Term = Var {-# UNPACK #-} !Int Elims -- ^ @x es@ neutral
              | Lam ArgInfo (Abs Term)        -- ^ Terms are beta normal. Relevance is ignored
              | Lit Literal
              | Def QName Elims               -- ^ @f es@, possibly a delta/iota-redex
              | Con ConHead ConInfo Elims
              -- ^ @c es@ or @record { fs = es }@
              --   @es@ allows only Apply and IApply eliminations,
              --   and IApply only for data constructors.
              | Pi (Dom Type) (Abs Type)      -- ^ dependent or non-dependent function space
              | Sort Sort
              | Level Level
              | MetaV {-# UNPACK #-} !MetaId Elims
              | DontCare Term
                -- ^ Irrelevant stuff in relevant position, but created
                --   in an irrelevant context.  Basically, an internal
                --   version of the irrelevance axiom @.irrAx : .A -> A@.
              | Dummy String Elims
                -- ^ A (part of a) term or type which is only used for internal purposes.
                --   Replaces the @Sort Prop@ hack.
                --   The @String@ typically describes the location where we create this dummy,
                --   but can contain other information as well.
                --   The second field accumulates eliminations in case we
                --   apply a dummy term to more of them. Dummy terms should never be used in places
                --   where they can affect type checking, so syntactic checks are free to ignore the
                --   eliminators, which are only there to ease debugging when a dummy term incorrectly
                --   leaks into a relevant position.
      deriving Int -> Term -> ShowS
    [Term] -> ShowS
    Term -> [Char]
    (Int -> Term -> ShowS)
    -> (Term -> [Char]) -> ([Term] -> ShowS) -> Show Term
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Term -> ShowS
    showsPrec :: Int -> Term -> ShowS
    $cshow :: Term -> [Char]
    show :: Term -> [Char]
    $cshowList :: [Term] -> ShowS
    showList :: [Term] -> ShowS
    Show

    type ConInfo = ConOrigin

    type Elim = Elim' Term
    type Elims = [Elim]  -- ^ eliminations ordered left-to-right.

    -- | Binder.
    --
    --   'Abs': The bound variable might appear in the body.
    --   'NoAbs' is pseudo-binder, it does not introduce a fresh variable,
    --      similar to the @const@ of Haskell.
    --
    data Abs a = Abs   { forall a. Abs a -> [Char]
    absName :: ArgName, forall a. Abs a -> a
    unAbs :: a }
                   -- ^ The body has (at least) one free variable.
                   --   Danger: 'unAbs' doesn't shift variables properly
               | NoAbs { absName :: ArgName, unAbs :: a }
      deriving ((forall a b. (a -> b) -> Abs a -> Abs b)
    -> (forall a b. a -> Abs b -> Abs a) -> Functor Abs
    forall a b. a -> Abs b -> Abs a
    forall a b. (a -> b) -> Abs a -> Abs b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Abs a -> Abs b
    fmap :: forall a b. (a -> b) -> Abs a -> Abs b
    $c<$ :: forall a b. a -> Abs b -> Abs a
    <$ :: forall a b. a -> Abs b -> Abs a
    Functor, (forall m. Monoid m => Abs m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Abs a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Abs a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Abs a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Abs a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Abs a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Abs a -> b)
    -> (forall a. (a -> a -> a) -> Abs a -> a)
    -> (forall a. (a -> a -> a) -> Abs a -> a)
    -> (forall a. Abs a -> [a])
    -> (forall a. Abs a -> Bool)
    -> (forall a. Abs a -> Int)
    -> (forall a. Eq a => a -> Abs a -> Bool)
    -> (forall a. Ord a => Abs a -> a)
    -> (forall a. Ord a => Abs a -> a)
    -> (forall a. Num a => Abs a -> a)
    -> (forall a. Num a => Abs a -> a)
    -> Foldable Abs
    forall a. Eq a => a -> Abs a -> Bool
    forall a. Num a => Abs a -> a
    forall a. Ord a => Abs a -> a
    forall m. Monoid m => Abs m -> m
    forall a. Abs a -> Bool
    forall a. Abs a -> Int
    forall a. Abs a -> [a]
    forall a. (a -> a -> a) -> Abs a -> a
    forall m a. Monoid m => (a -> m) -> Abs a -> m
    forall b a. (b -> a -> b) -> b -> Abs a -> b
    forall a b. (a -> b -> b) -> b -> Abs 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 -> Int)
    -> (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
    $cfold :: forall m. Monoid m => Abs m -> m
    fold :: forall m. Monoid m => Abs m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Abs a -> a
    foldr1 :: forall a. (a -> a -> a) -> Abs a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Abs a -> a
    foldl1 :: forall a. (a -> a -> a) -> Abs a -> a
    $ctoList :: forall a. Abs a -> [a]
    toList :: forall a. Abs a -> [a]
    $cnull :: forall a. Abs a -> Bool
    null :: forall a. Abs a -> Bool
    $clength :: forall a. Abs a -> Int
    length :: forall a. Abs a -> Int
    $celem :: forall a. Eq a => a -> Abs a -> Bool
    elem :: forall a. Eq a => a -> Abs a -> Bool
    $cmaximum :: forall a. Ord a => Abs a -> a
    maximum :: forall a. Ord a => Abs a -> a
    $cminimum :: forall a. Ord a => Abs a -> a
    minimum :: forall a. Ord a => Abs a -> a
    $csum :: forall a. Num a => Abs a -> a
    sum :: forall a. Num a => Abs a -> a
    $cproduct :: forall a. Num a => Abs a -> a
    product :: forall a. Num a => Abs a -> a
    Foldable, Functor Abs
    Foldable Abs
    (Functor Abs, Foldable Abs) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Abs a -> f (Abs b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Abs (f a) -> f (Abs a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Abs a -> m (Abs b))
    -> (forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a))
    -> Traversable Abs
    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 => Abs (m a) -> m (Abs a)
    forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Abs a -> m (Abs b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Abs a -> f (Abs b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Abs a -> f (Abs b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Abs a -> f (Abs b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Abs a -> m (Abs b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Abs a -> m (Abs b)
    $csequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
    sequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
    Traversable, (forall x. Abs a -> Rep (Abs a) x)
    -> (forall x. Rep (Abs a) x -> Abs a) -> Generic (Abs a)
    forall x. Rep (Abs a) x -> Abs a
    forall x. Abs a -> Rep (Abs a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (Abs a) x -> Abs a
    forall a x. Abs a -> Rep (Abs a) x
    $cfrom :: forall a x. Abs a -> Rep (Abs a) x
    from :: forall x. Abs a -> Rep (Abs a) x
    $cto :: forall a x. Rep (Abs a) x -> Abs a
    to :: forall x. Rep (Abs a) x -> Abs a
    Generic)

    instance Decoration Abs where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Abs a -> m (Abs b)
    traverseF a -> m b
    f (Abs   [Char]
    x a
    a) = [Char] -> b -> Abs b
    forall a. [Char] -> a -> Abs a
    Abs   [Char]
    x (b -> Abs b) -> m b -> m (Abs b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    a
      traverseF a -> m b
    f (NoAbs [Char]
    x a
    a) = [Char] -> b -> Abs b
    forall a. [Char] -> a -> Abs a
    NoAbs [Char]
    x (b -> Abs b) -> m b -> m (Abs b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    a

    -- | Types are terms with a sort annotation.
    --
    data Type'' t a = El { forall t a. Type'' t a -> Sort' t
    _getSort :: Sort' t, forall t a. Type'' t a -> a
    unEl :: a }
      deriving (Int -> Type'' t a -> ShowS
    [Type'' t a] -> ShowS
    Type'' t a -> [Char]
    (Int -> Type'' t a -> ShowS)
    -> (Type'' t a -> [Char])
    -> ([Type'' t a] -> ShowS)
    -> Show (Type'' t a)
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    forall t a. (Show t, Show a) => Int -> Type'' t a -> ShowS
    forall t a. (Show t, Show a) => [Type'' t a] -> ShowS
    forall t a. (Show t, Show a) => Type'' t a -> [Char]
    $cshowsPrec :: forall t a. (Show t, Show a) => Int -> Type'' t a -> ShowS
    showsPrec :: Int -> Type'' t a -> ShowS
    $cshow :: forall t a. (Show t, Show a) => Type'' t a -> [Char]
    show :: Type'' t a -> [Char]
    $cshowList :: forall t a. (Show t, Show a) => [Type'' t a] -> ShowS
    showList :: [Type'' t a] -> ShowS
    Show, (forall a b. (a -> b) -> Type'' t a -> Type'' t b)
    -> (forall a b. a -> Type'' t b -> Type'' t a)
    -> Functor (Type'' t)
    forall a b. a -> Type'' t b -> Type'' t a
    forall a b. (a -> b) -> Type'' t a -> Type'' t b
    forall t a b. a -> Type'' t b -> Type'' t a
    forall t a b. (a -> b) -> Type'' t a -> Type'' t b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall t a b. (a -> b) -> Type'' t a -> Type'' t b
    fmap :: forall a b. (a -> b) -> Type'' t a -> Type'' t b
    $c<$ :: forall t a b. a -> Type'' t b -> Type'' t a
    <$ :: forall a b. a -> Type'' t b -> Type'' t a
    Functor, (forall m. Monoid m => Type'' t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Type'' t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Type'' t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Type'' t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Type'' t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Type'' t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Type'' t a -> b)
    -> (forall a. (a -> a -> a) -> Type'' t a -> a)
    -> (forall a. (a -> a -> a) -> Type'' t a -> a)
    -> (forall a. Type'' t a -> [a])
    -> (forall a. Type'' t a -> Bool)
    -> (forall a. Type'' t a -> Int)
    -> (forall a. Eq a => a -> Type'' t a -> Bool)
    -> (forall a. Ord a => Type'' t a -> a)
    -> (forall a. Ord a => Type'' t a -> a)
    -> (forall a. Num a => Type'' t a -> a)
    -> (forall a. Num a => Type'' t a -> a)
    -> Foldable (Type'' t)
    forall a. Eq a => a -> Type'' t a -> Bool
    forall a. Num a => Type'' t a -> a
    forall a. Ord a => Type'' t a -> a
    forall m. Monoid m => Type'' t m -> m
    forall a. Type'' t a -> Bool
    forall a. Type'' t a -> Int
    forall a. Type'' t a -> [a]
    forall a. (a -> a -> a) -> Type'' t a -> a
    forall t a. Eq a => a -> Type'' t a -> Bool
    forall t a. Num a => Type'' t a -> a
    forall t a. Ord a => Type'' t a -> a
    forall m a. Monoid m => (a -> m) -> Type'' t a -> m
    forall t m. Monoid m => Type'' t m -> m
    forall m a. Monoid m => (a -> m) -> Type'' t a -> m
    forall t a. Type'' t a -> Bool
    forall t a. Type'' t a -> Int
    forall t a. Type'' t a -> [a]
    forall b a. (b -> a -> b) -> b -> Type'' t a -> b
    forall a b. (a -> b -> b) -> b -> Type'' t a -> b
    forall t a. (a -> a -> a) -> Type'' t a -> a
    forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
    forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
    forall t a b. (a -> b -> b) -> b -> Type'' t 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 -> Int)
    -> (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
    $cfold :: forall t m. Monoid m => Type'' t m -> m
    fold :: forall m. Monoid m => Type'' t m -> m
    $cfoldMap :: forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Type'' t a -> m
    $cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Type'' t a -> m
    $cfoldr :: forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Type'' t a -> b
    $cfoldr' :: forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Type'' t a -> b
    $cfoldl :: forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Type'' t a -> b
    $cfoldl' :: forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Type'' t a -> b
    $cfoldr1 :: forall t a. (a -> a -> a) -> Type'' t a -> a
    foldr1 :: forall a. (a -> a -> a) -> Type'' t a -> a
    $cfoldl1 :: forall t a. (a -> a -> a) -> Type'' t a -> a
    foldl1 :: forall a. (a -> a -> a) -> Type'' t a -> a
    $ctoList :: forall t a. Type'' t a -> [a]
    toList :: forall a. Type'' t a -> [a]
    $cnull :: forall t a. Type'' t a -> Bool
    null :: forall a. Type'' t a -> Bool
    $clength :: forall t a. Type'' t a -> Int
    length :: forall a. Type'' t a -> Int
    $celem :: forall t a. Eq a => a -> Type'' t a -> Bool
    elem :: forall a. Eq a => a -> Type'' t a -> Bool
    $cmaximum :: forall t a. Ord a => Type'' t a -> a
    maximum :: forall a. Ord a => Type'' t a -> a
    $cminimum :: forall t a. Ord a => Type'' t a -> a
    minimum :: forall a. Ord a => Type'' t a -> a
    $csum :: forall t a. Num a => Type'' t a -> a
    sum :: forall a. Num a => Type'' t a -> a
    $cproduct :: forall t a. Num a => Type'' t a -> a
    product :: forall a. Num a => Type'' t a -> a
    Foldable, Functor (Type'' t)
    Foldable (Type'' t)
    (Functor (Type'' t), Foldable (Type'' t)) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Type'' t a -> f (Type'' t b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Type'' t (f a) -> f (Type'' t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Type'' t a -> m (Type'' t b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Type'' t (m a) -> m (Type'' t a))
    -> Traversable (Type'' t)
    forall t. Functor (Type'' t)
    forall t. Foldable (Type'' t)
    forall t (m :: * -> *) a.
    Monad m =>
    Type'' t (m a) -> m (Type'' t a)
    forall t (f :: * -> *) a.
    Applicative f =>
    Type'' t (f a) -> f (Type'' t a)
    forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Type'' t a -> m (Type'' t b)
    forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Type'' t a -> f (Type'' t b)
    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 => Type'' t (m a) -> m (Type'' t a)
    forall (f :: * -> *) a.
    Applicative f =>
    Type'' t (f a) -> f (Type'' t a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Type'' t a -> m (Type'' t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Type'' t a -> f (Type'' t b)
    $ctraverse :: forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Type'' t a -> f (Type'' t b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Type'' t a -> f (Type'' t b)
    $csequenceA :: forall t (f :: * -> *) a.
    Applicative f =>
    Type'' t (f a) -> f (Type'' t a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Type'' t (f a) -> f (Type'' t a)
    $cmapM :: forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Type'' t a -> m (Type'' t b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Type'' t a -> m (Type'' t b)
    $csequence :: forall t (m :: * -> *) a.
    Monad m =>
    Type'' t (m a) -> m (Type'' t a)
    sequence :: forall (m :: * -> *) a. Monad m => Type'' t (m a) -> m (Type'' t a)
    Traversable)

    type Type' a = Type'' Term a

    type Type = Type' Term

    instance Decoration (Type'' t) where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Type'' t a -> m (Type'' t b)
    traverseF a -> m b
    f (El Sort' t
    s a
    a) = Sort' t -> b -> Type'' t b
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' t
    s (b -> Type'' t b) -> m b -> m (Type'' t b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    a

    class LensSort a where
      lensSort ::  Lens' a Sort
      getSort  :: a -> Sort
      getSort a
    a = a
    a a -> Lens' a Sort -> Sort
    forall o i. o -> Lens' o i -> i
    ^. (Sort -> f Sort) -> a -> f a
    forall a. LensSort a => Lens' a Sort
    Lens' a Sort
    lensSort

    instance LensSort Sort where
      lensSort :: Lens' Sort Sort
    lensSort Sort -> f Sort
    f Sort
    s = Sort -> f Sort
    f Sort
    s f Sort -> (Sort -> Sort) -> f Sort
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Sort
    s' -> Sort
    s'

    instance LensSort (Type' a) where
      lensSort :: Lens' (Type' a) Sort
    lensSort Sort -> f Sort
    f (El Sort
    s a
    a) = Sort -> f Sort
    f Sort
    s f Sort -> (Sort -> Type' a) -> f (Type' a)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Sort
    s' -> Sort -> a -> Type' a
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s' a
    a

    -- General instance leads to overlapping instances.
    -- instance (Decoration f, LensSort a) => LensSort (f a) where
    instance LensSort a => LensSort (Dom a) where
      lensSort :: Lens' (Dom a) Sort
    lensSort = (a -> f a) -> Dom a -> f (Dom a)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Dom' Term a -> m (Dom' Term b)
    traverseF ((a -> f a) -> Dom a -> f (Dom a))
    -> ((Sort -> f Sort) -> a -> f a)
    -> (Sort -> f Sort)
    -> Dom a
    -> f (Dom a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Sort -> f Sort) -> a -> f a
    forall a. LensSort a => Lens' a Sort
    Lens' a Sort
    lensSort

    instance LensSort a => LensSort (Arg a) where
      lensSort :: Lens' (Arg a) Sort
    lensSort = (a -> f a) -> Arg a -> f (Arg a)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Arg a -> m (Arg b)
    traverseF ((a -> f a) -> Arg a -> f (Arg a))
    -> ((Sort -> f Sort) -> a -> f a)
    -> (Sort -> f Sort)
    -> Arg a
    -> f (Arg a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Sort -> f Sort) -> a -> f a
    forall a. LensSort a => Lens' a Sort
    Lens' a Sort
    lensSort

    -- | Sequence of types. An argument of the first type is bound in later types
    --   and so on.
    data Tele a = EmptyTel
                | ExtendTel a (Abs (Tele a))  -- ^ 'Abs' is never 'NoAbs'.
      deriving (Int -> Tele a -> ShowS
    [Tele a] -> ShowS
    Tele a -> [Char]
    (Int -> Tele a -> ShowS)
    -> (Tele a -> [Char]) -> ([Tele a] -> ShowS) -> Show (Tele a)
    forall a. Show a => Int -> Tele a -> ShowS
    forall a. Show a => [Tele a] -> ShowS
    forall a. Show a => Tele a -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> Tele a -> ShowS
    showsPrec :: Int -> Tele a -> ShowS
    $cshow :: forall a. Show a => Tele a -> [Char]
    show :: Tele a -> [Char]
    $cshowList :: forall a. Show a => [Tele a] -> ShowS
    showList :: [Tele a] -> ShowS
    Show, (forall a b. (a -> b) -> Tele a -> Tele b)
    -> (forall a b. a -> Tele b -> Tele a) -> Functor Tele
    forall a b. a -> Tele b -> Tele a
    forall a b. (a -> b) -> Tele a -> Tele b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Tele a -> Tele b
    fmap :: forall a b. (a -> b) -> Tele a -> Tele b
    $c<$ :: forall a b. a -> Tele b -> Tele a
    <$ :: forall a b. a -> Tele b -> Tele a
    Functor, (forall m. Monoid m => Tele m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Tele a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Tele a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Tele a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Tele a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Tele a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Tele a -> b)
    -> (forall a. (a -> a -> a) -> Tele a -> a)
    -> (forall a. (a -> a -> a) -> Tele a -> a)
    -> (forall a. Tele a -> [a])
    -> (forall a. Tele a -> Bool)
    -> (forall a. Tele a -> Int)
    -> (forall a. Eq a => a -> Tele a -> Bool)
    -> (forall a. Ord a => Tele a -> a)
    -> (forall a. Ord a => Tele a -> a)
    -> (forall a. Num a => Tele a -> a)
    -> (forall a. Num a => Tele a -> a)
    -> Foldable Tele
    forall a. Eq a => a -> Tele a -> Bool
    forall a. Num a => Tele a -> a
    forall a. Ord a => Tele a -> a
    forall m. Monoid m => Tele m -> m
    forall a. Tele a -> Bool
    forall a. Tele a -> Int
    forall a. Tele a -> [a]
    forall a. (a -> a -> a) -> Tele a -> a
    forall m a. Monoid m => (a -> m) -> Tele a -> m
    forall b a. (b -> a -> b) -> b -> Tele a -> b
    forall a b. (a -> b -> b) -> b -> Tele 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 -> Int)
    -> (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
    $cfold :: forall m. Monoid m => Tele m -> m
    fold :: forall m. Monoid m => Tele m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Tele a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Tele a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Tele a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Tele a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Tele a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Tele a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Tele a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Tele a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Tele a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Tele a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Tele a -> a
    foldr1 :: forall a. (a -> a -> a) -> Tele a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Tele a -> a
    foldl1 :: forall a. (a -> a -> a) -> Tele a -> a
    $ctoList :: forall a. Tele a -> [a]
    toList :: forall a. Tele a -> [a]
    $cnull :: forall a. Tele a -> Bool
    null :: forall a. Tele a -> Bool
    $clength :: forall a. Tele a -> Int
    length :: forall a. Tele a -> Int
    $celem :: forall a. Eq a => a -> Tele a -> Bool
    elem :: forall a. Eq a => a -> Tele a -> Bool
    $cmaximum :: forall a. Ord a => Tele a -> a
    maximum :: forall a. Ord a => Tele a -> a
    $cminimum :: forall a. Ord a => Tele a -> a
    minimum :: forall a. Ord a => Tele a -> a
    $csum :: forall a. Num a => Tele a -> a
    sum :: forall a. Num a => Tele a -> a
    $cproduct :: forall a. Num a => Tele a -> a
    product :: forall a. Num a => Tele a -> a
    Foldable, Functor Tele
    Foldable Tele
    (Functor Tele, Foldable Tele) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Tele a -> f (Tele b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Tele (f a) -> f (Tele a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Tele a -> m (Tele b))
    -> (forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a))
    -> Traversable Tele
    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 => Tele (m a) -> m (Tele a)
    forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Tele a -> m (Tele b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Tele a -> f (Tele b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Tele a -> f (Tele b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Tele a -> f (Tele b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Tele a -> m (Tele b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Tele a -> m (Tele b)
    $csequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
    sequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
    Traversable, (forall x. Tele a -> Rep (Tele a) x)
    -> (forall x. Rep (Tele a) x -> Tele a) -> Generic (Tele a)
    forall x. Rep (Tele a) x -> Tele a
    forall x. Tele a -> Rep (Tele a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (Tele a) x -> Tele a
    forall a x. Tele a -> Rep (Tele a) x
    $cfrom :: forall a x. Tele a -> Rep (Tele a) x
    from :: forall x. Tele a -> Rep (Tele a) x
    $cto :: forall a x. Rep (Tele a) x -> Tele a
    to :: forall x. Rep (Tele a) x -> Tele a
    Generic)

    type Telescope = Tele (Dom Type)

    data UnivSize
      = USmall  -- ^ @Prop/Set/SSet ℓ@.
      | ULarge  -- ^ @(Prop/Set/SSet)ωᵢ@.
      deriving stock (UnivSize -> UnivSize -> Bool
    (UnivSize -> UnivSize -> Bool)
    -> (UnivSize -> UnivSize -> Bool) -> Eq UnivSize
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: UnivSize -> UnivSize -> Bool
    == :: UnivSize -> UnivSize -> Bool
    $c/= :: UnivSize -> UnivSize -> Bool
    /= :: UnivSize -> UnivSize -> Bool
    Eq, Int -> UnivSize -> ShowS
    [UnivSize] -> ShowS
    UnivSize -> [Char]
    (Int -> UnivSize -> ShowS)
    -> (UnivSize -> [Char]) -> ([UnivSize] -> ShowS) -> Show UnivSize
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnivSize -> ShowS
    showsPrec :: Int -> UnivSize -> ShowS
    $cshow :: UnivSize -> [Char]
    show :: UnivSize -> [Char]
    $cshowList :: [UnivSize] -> ShowS
    showList :: [UnivSize] -> ShowS
    Show)

    -- | Sorts.
    --
    data Sort' t
      = Univ Univ (Level' t)
          -- ^ @Prop ℓ@, @Set ℓ@, @SSet ℓ@.
      | Inf Univ !Integer
          -- ^ @Propωᵢ@, @(S)Setωᵢ@.
      | SizeUniv    -- ^ @SizeUniv@, a sort inhabited by type @Size@.
      | LockUniv    -- ^ @LockUniv@, a sort for locks.
      | LevelUniv   -- ^ @LevelUniv@, a sort inhabited by type @Level@. When --level-universe isn't on, this universe reduces to @Set 0@
      | IntervalUniv -- ^ @IntervalUniv@, a sort inhabited by the cubical interval.
      | PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) -- ^ Sort of the pi type.
      | FunSort (Sort' t) (Sort' t) -- ^ Sort of a (non-dependent) function type.
      | UnivSort (Sort' t) -- ^ Sort of another sort.
      | MetaS {-# UNPACK #-} !MetaId [Elim' t]
      | DefS QName [Elim' t] -- ^ A postulated sort.
      | DummyS String
        -- ^ A (part of a) term or type which is only used for internal purposes.
        --   Replaces the abuse of @Prop@ for a dummy sort.
        --   The @String@ typically describes the location where we create this dummy,
        --   but can contain other information as well.
      deriving Int -> Sort' t -> ShowS
    [Sort' t] -> ShowS
    Sort' t -> [Char]
    (Int -> Sort' t -> ShowS)
    -> (Sort' t -> [Char]) -> ([Sort' t] -> ShowS) -> Show (Sort' t)
    forall t. Show t => Int -> Sort' t -> ShowS
    forall t. Show t => [Sort' t] -> ShowS
    forall t. Show t => Sort' t -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall t. Show t => Int -> Sort' t -> ShowS
    showsPrec :: Int -> Sort' t -> ShowS
    $cshow :: forall t. Show t => Sort' t -> [Char]
    show :: Sort' t -> [Char]
    $cshowList :: forall t. Show t => [Sort' t] -> ShowS
    showList :: [Sort' t] -> ShowS
    Show

    pattern Prop, Type, SSet :: Level' t -> Sort' t
    pattern $mProp :: forall {r} {t}. Sort' t -> (Level' t -> r) -> ((# #) -> r) -> r
    $bProp :: forall t. Level' t -> Sort' t
    Prop l = Univ UProp l
    pattern $mType :: forall {r} {t}. Sort' t -> (Level' t -> r) -> ((# #) -> r) -> r
    $bType :: forall t. Level' t -> Sort' t
    Type l = Univ UType l
    pattern $mSSet :: forall {r} {t}. Sort' t -> (Level' t -> r) -> ((# #) -> r) -> r
    $bSSet :: forall t. Level' t -> Sort' t
    SSet l = Univ USSet l

    {-# COMPLETE
      Prop, Type, SSet, Inf,
      SizeUniv, LockUniv, LevelUniv, IntervalUniv,
      PiSort, FunSort, UnivSort, MetaS, DefS, DummyS #-}

    type Sort = Sort' Term

    -- | A level is a maximum expression of a closed level and 0..n
    --   'PlusLevel' expressions each of which is an atom plus a number.
    data Level' t = Max !Integer [PlusLevel' t]
      deriving (Int -> Level' t -> ShowS
    [Level' t] -> ShowS
    Level' t -> [Char]
    (Int -> Level' t -> ShowS)
    -> (Level' t -> [Char]) -> ([Level' t] -> ShowS) -> Show (Level' t)
    forall t. Show t => Int -> Level' t -> ShowS
    forall t. Show t => [Level' t] -> ShowS
    forall t. Show t => Level' t -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall t. Show t => Int -> Level' t -> ShowS
    showsPrec :: Int -> Level' t -> ShowS
    $cshow :: forall t. Show t => Level' t -> [Char]
    show :: Level' t -> [Char]
    $cshowList :: forall t. Show t => [Level' t] -> ShowS
    showList :: [Level' t] -> ShowS
    Show, (forall a b. (a -> b) -> Level' a -> Level' b)
    -> (forall a b. a -> Level' b -> Level' a) -> Functor Level'
    forall a b. a -> Level' b -> Level' a
    forall a b. (a -> b) -> Level' a -> Level' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Level' a -> Level' b
    fmap :: forall a b. (a -> b) -> Level' a -> Level' b
    $c<$ :: forall a b. a -> Level' b -> Level' a
    <$ :: forall a b. a -> Level' b -> Level' a
    Functor, (forall m. Monoid m => Level' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Level' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Level' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Level' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Level' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Level' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Level' a -> b)
    -> (forall a. (a -> a -> a) -> Level' a -> a)
    -> (forall a. (a -> a -> a) -> Level' a -> a)
    -> (forall a. Level' a -> [a])
    -> (forall a. Level' a -> Bool)
    -> (forall a. Level' a -> Int)
    -> (forall a. Eq a => a -> Level' a -> Bool)
    -> (forall a. Ord a => Level' a -> a)
    -> (forall a. Ord a => Level' a -> a)
    -> (forall a. Num a => Level' a -> a)
    -> (forall a. Num a => Level' a -> a)
    -> Foldable Level'
    forall a. Eq a => a -> Level' a -> Bool
    forall a. Num a => Level' a -> a
    forall a. Ord a => Level' a -> a
    forall m. Monoid m => Level' m -> m
    forall a. Level' a -> Bool
    forall a. Level' a -> Int
    forall a. Level' a -> [a]
    forall a. (a -> a -> a) -> Level' a -> a
    forall m a. Monoid m => (a -> m) -> Level' a -> m
    forall b a. (b -> a -> b) -> b -> Level' a -> b
    forall a b. (a -> b -> b) -> b -> Level' 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 -> Int)
    -> (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
    $cfold :: forall m. Monoid m => Level' m -> m
    fold :: forall m. Monoid m => Level' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Level' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Level' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Level' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Level' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Level' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Level' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Level' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Level' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Level' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Level' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Level' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Level' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Level' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Level' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Level' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Level' a -> a
    $ctoList :: forall a. Level' a -> [a]
    toList :: forall a. Level' a -> [a]
    $cnull :: forall a. Level' a -> Bool
    null :: forall a. Level' a -> Bool
    $clength :: forall a. Level' a -> Int
    length :: forall a. Level' a -> Int
    $celem :: forall a. Eq a => a -> Level' a -> Bool
    elem :: forall a. Eq a => a -> Level' a -> Bool
    $cmaximum :: forall a. Ord a => Level' a -> a
    maximum :: forall a. Ord a => Level' a -> a
    $cminimum :: forall a. Ord a => Level' a -> a
    minimum :: forall a. Ord a => Level' a -> a
    $csum :: forall a. Num a => Level' a -> a
    sum :: forall a. Num a => Level' a -> a
    $cproduct :: forall a. Num a => Level' a -> a
    product :: forall a. Num a => Level' a -> a
    Foldable, Functor Level'
    Foldable Level'
    (Functor Level', Foldable Level') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Level' a -> f (Level' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Level' (f a) -> f (Level' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Level' a -> m (Level' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Level' (m a) -> m (Level' a))
    -> Traversable Level'
    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 => Level' (m a) -> m (Level' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Level' (f a) -> f (Level' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Level' a -> m (Level' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Level' a -> f (Level' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Level' a -> f (Level' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Level' a -> f (Level' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Level' (f a) -> f (Level' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Level' (f a) -> f (Level' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Level' a -> m (Level' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Level' a -> m (Level' b)
    $csequence :: forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
    sequence :: forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
    Traversable)

    type Level = Level' Term

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

    type PlusLevel = PlusLevel' Term
    type LevelAtom = Term

    ---------------------------------------------------------------------------
    -- * Brave Terms
    ---------------------------------------------------------------------------

    -- | Newtypes for terms that produce a dummy, rather than crash, when
    --   applied to incompatible eliminations.
    newtype BraveTerm = BraveTerm { BraveTerm -> Term
    unBrave :: Term } deriving Int -> BraveTerm -> ShowS
    [BraveTerm] -> ShowS
    BraveTerm -> [Char]
    (Int -> BraveTerm -> ShowS)
    -> (BraveTerm -> [Char])
    -> ([BraveTerm] -> ShowS)
    -> Show BraveTerm
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> BraveTerm -> ShowS
    showsPrec :: Int -> BraveTerm -> ShowS
    $cshow :: BraveTerm -> [Char]
    show :: BraveTerm -> [Char]
    $cshowList :: [BraveTerm] -> ShowS
    showList :: [BraveTerm] -> ShowS
    Show

    ---------------------------------------------------------------------------
    -- * Blocked Terms
    ---------------------------------------------------------------------------

    type Blocked    = Blocked' Term
    type NotBlocked = NotBlocked' Term
    --
    -- | @'Blocked a@ without the @a@.
    type Blocked_ = Blocked ()

    ---------------------------------------------------------------------------
    -- * Definitions
    ---------------------------------------------------------------------------

    -- | Named pattern arguments.
    type NAPs = [NamedArg DeBruijnPattern]

    -- | A clause is a list of patterns and the clause body.
    --
    --  The telescope contains the types of the pattern variables and the
    --  de Bruijn indices say how to get from the order the variables occur in
    --  the patterns to the order they occur in the telescope. The body
    --  binds the variables in the order they appear in the telescope.
    --
    --  @clauseTel ~ permute clausePerm (patternVars namedClausePats)@
    --
    --  Terms in dot patterns are valid in the clause telescope.
    --
    --  For the purpose of the permutation and the body dot patterns count
    --  as variables. TODO: Change this!
    data Clause = Clause
        { Clause -> Range
    clauseLHSRange    :: Range
        , Clause -> Range
    clauseFullRange   :: Range
        , Clause -> Telescope
    clauseTel         :: Telescope
          -- ^ @Δ@: The types of the pattern variables in dependency order.
        , Clause -> NAPs
    namedClausePats   :: NAPs
          -- ^ @Δ ⊢ ps@.  The de Bruijn indices refer to @Δ@.
        , Clause -> Maybe Term
    clauseBody        :: Maybe Term
          -- ^ @Just v@ with @Δ ⊢ v@ for a regular clause, or @Nothing@ for an
          --   absurd one.
        , Clause -> Maybe (Arg Type)
    clauseType        :: Maybe (Arg Type)
          -- ^ @Δ ⊢ t@.  The type of the rhs under @clauseTel@.
          --   Used, e.g., by @TermCheck@.
          --   Can be 'Irrelevant' if we encountered an irrelevant projection
          --   pattern on the lhs.
        , Clause -> Catchall
    clauseCatchall    :: Catchall
          -- ^ Clause has been labelled as CATCHALL.
        , Clause -> Maybe Bool
    clauseRecursive   :: Maybe Bool
          -- ^ @clauseBody@ contains recursive calls; computed by termination checker.
          --   @Nothing@ means that termination checker has not run yet,
          --   or that @clauseBody@ contains meta-variables;
          --   these could be filled with recursive calls later!
          --   @Just False@ means definitely no recursive call.
          --   @Just True@ means definitely a recursive call.
        , Clause -> Maybe Bool
    clauseUnreachable :: Maybe Bool
          -- ^ Clause has been labelled as unreachable by the coverage checker.
          --   @Nothing@ means coverage checker has not run yet (clause may be unreachable).
          --   @Just False@ means clause is not unreachable.
          --   @Just True@ means clause is unreachable.
        , Clause -> ExpandedEllipsis
    clauseEllipsis    :: ExpandedEllipsis
          -- ^ Was this clause created by expansion of an ellipsis?
        , Clause -> Maybe ModuleName
    clauseWhereModule :: Maybe ModuleName
          -- ^ Keeps track of the module name associate with the clause's where clause.
        }
      deriving (Int -> Clause -> ShowS
    [Clause] -> ShowS
    Clause -> [Char]
    (Int -> Clause -> ShowS)
    -> (Clause -> [Char]) -> ([Clause] -> ShowS) -> Show Clause
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Clause -> ShowS
    showsPrec :: Int -> Clause -> ShowS
    $cshow :: Clause -> [Char]
    show :: Clause -> [Char]
    $cshowList :: [Clause] -> ShowS
    showList :: [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
    $cfrom :: forall x. Clause -> Rep Clause x
    from :: forall x. Clause -> Rep Clause x
    $cto :: forall x. Rep Clause x -> Clause
    to :: forall x. Rep Clause x -> Clause
    Generic)

    clausePats :: Clause -> [Arg DeBruijnPattern]
    clausePats :: Clause -> [Arg DeBruijnPattern]
    clausePats = (Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern)
    -> NAPs -> [Arg DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named_ DeBruijnPattern -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named_ DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing) (NAPs -> [Arg DeBruijnPattern])
    -> (Clause -> NAPs) -> Clause -> [Arg DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> NAPs
    namedClausePats

    instance HasRange Clause where
      getRange :: Clause -> Range
    getRange = Clause -> Range
    clauseLHSRange

    -- | Pattern variables.
    type PatVarName = ArgName

    patVarNameToString :: PatVarName -> String
    patVarNameToString :: ShowS
    patVarNameToString = ShowS
    argNameToString

    nameToPatVarName :: Name -> PatVarName
    nameToPatVarName :: Name -> [Char]
    nameToPatVarName = Name -> [Char]
    nameToArgName

    data PatternInfo = PatternInfo
      { PatternInfo -> PatOrigin
    patOrigin :: PatOrigin
      , PatternInfo -> [Name]
    patAsNames :: [Name]
      } deriving (Int -> PatternInfo -> ShowS
    [PatternInfo] -> ShowS
    PatternInfo -> [Char]
    (Int -> PatternInfo -> ShowS)
    -> (PatternInfo -> [Char])
    -> ([PatternInfo] -> ShowS)
    -> Show PatternInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PatternInfo -> ShowS
    showsPrec :: Int -> PatternInfo -> ShowS
    $cshow :: PatternInfo -> [Char]
    show :: PatternInfo -> [Char]
    $cshowList :: [PatternInfo] -> ShowS
    showList :: [PatternInfo] -> ShowS
    Show, PatternInfo -> PatternInfo -> Bool
    (PatternInfo -> PatternInfo -> Bool)
    -> (PatternInfo -> PatternInfo -> Bool) -> Eq PatternInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PatternInfo -> PatternInfo -> Bool
    == :: PatternInfo -> PatternInfo -> Bool
    $c/= :: PatternInfo -> PatternInfo -> Bool
    /= :: PatternInfo -> PatternInfo -> Bool
    Eq, (forall x. PatternInfo -> Rep PatternInfo x)
    -> (forall x. Rep PatternInfo x -> PatternInfo)
    -> Generic PatternInfo
    forall x. Rep PatternInfo x -> PatternInfo
    forall x. PatternInfo -> Rep PatternInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PatternInfo -> Rep PatternInfo x
    from :: forall x. PatternInfo -> Rep PatternInfo x
    $cto :: forall x. Rep PatternInfo x -> PatternInfo
    to :: forall x. Rep PatternInfo x -> PatternInfo
    Generic)

    defaultPatternInfo :: PatternInfo
    defaultPatternInfo :: PatternInfo
    defaultPatternInfo = PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    PatOSystem []

    -- | Origin of the pattern: what did the user write in this position?
    data PatOrigin
      = PatOSystem         -- ^ Pattern inserted by the system
      | PatOSplit          -- ^ Pattern generated by case split
      | PatOSplitArg ArgName -- ^ Argument to pattern generated by case split
      | PatOVar Name       -- ^ User wrote a variable pattern
      | PatODot            -- ^ User wrote a dot pattern
      | PatOWild           -- ^ User wrote a wildcard pattern
      | PatOCon            -- ^ User wrote a constructor pattern
      | PatORec            -- ^ User wrote a record pattern
      | PatOLit            -- ^ User wrote a literal pattern
      | PatOAbsurd         -- ^ User wrote an absurd pattern
      deriving (Int -> PatOrigin -> ShowS
    [PatOrigin] -> ShowS
    PatOrigin -> [Char]
    (Int -> PatOrigin -> ShowS)
    -> (PatOrigin -> [Char])
    -> ([PatOrigin] -> ShowS)
    -> Show PatOrigin
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PatOrigin -> ShowS
    showsPrec :: Int -> PatOrigin -> ShowS
    $cshow :: PatOrigin -> [Char]
    show :: PatOrigin -> [Char]
    $cshowList :: [PatOrigin] -> ShowS
    showList :: [PatOrigin] -> ShowS
    Show, PatOrigin -> PatOrigin -> Bool
    (PatOrigin -> PatOrigin -> Bool)
    -> (PatOrigin -> PatOrigin -> Bool) -> Eq PatOrigin
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PatOrigin -> PatOrigin -> Bool
    == :: PatOrigin -> PatOrigin -> Bool
    $c/= :: PatOrigin -> PatOrigin -> Bool
    /= :: PatOrigin -> PatOrigin -> Bool
    Eq, (forall x. PatOrigin -> Rep PatOrigin x)
    -> (forall x. Rep PatOrigin x -> PatOrigin) -> Generic PatOrigin
    forall x. Rep PatOrigin x -> PatOrigin
    forall x. PatOrigin -> Rep PatOrigin x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PatOrigin -> Rep PatOrigin x
    from :: forall x. PatOrigin -> Rep PatOrigin x
    $cto :: forall x. Rep PatOrigin x -> PatOrigin
    to :: forall x. Rep PatOrigin x -> PatOrigin
    Generic)

    -- | Patterns are variables, constructors, or wildcards.
    --   @QName@ is used in @ConP@ rather than @Name@ since
    --     a constructor might come from a particular namespace.
    --     This also meshes well with the fact that values (i.e.
    --     the arguments we are matching with) use @QName@.
    --
    data Pattern' x
      = VarP PatternInfo x
        -- ^ @x@
      | DotP PatternInfo Term
        -- ^ @.t@
      | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
        -- ^ @c ps@
        --   The subpatterns do not contain any projection copatterns.
      | LitP PatternInfo Literal
        -- ^ E.g. @5@, @"hello"@.
      | ProjP ProjOrigin QName
        -- ^ Projection copattern.  Can only appear by itself.
      | IApplyP PatternInfo Term Term x
        -- ^ Path elimination pattern, like @VarP@ but keeps track of endpoints.
      | DefP PatternInfo QName [NamedArg (Pattern' x)]
        -- ^ Used for HITs, the QName should be the one from primHComp.
      deriving (Int -> Pattern' x -> ShowS
    [Pattern' x] -> ShowS
    Pattern' x -> [Char]
    (Int -> Pattern' x -> ShowS)
    -> (Pattern' x -> [Char])
    -> ([Pattern' x] -> ShowS)
    -> Show (Pattern' x)
    forall x. Show x => Int -> Pattern' x -> ShowS
    forall x. Show x => [Pattern' x] -> ShowS
    forall x. Show x => Pattern' x -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall x. Show x => Int -> Pattern' x -> ShowS
    showsPrec :: Int -> Pattern' x -> ShowS
    $cshow :: forall x. Show x => Pattern' x -> [Char]
    show :: Pattern' x -> [Char]
    $cshowList :: forall x. Show x => [Pattern' x] -> ShowS
    showList :: [Pattern' x] -> ShowS
    Show, (forall a b. (a -> b) -> Pattern' a -> Pattern' b)
    -> (forall a b. a -> Pattern' b -> Pattern' a) -> Functor Pattern'
    forall a b. a -> Pattern' b -> Pattern' a
    forall a b. (a -> b) -> Pattern' a -> Pattern' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
    fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
    $c<$ :: forall a b. a -> Pattern' b -> Pattern' a
    <$ :: forall a b. a -> Pattern' b -> Pattern' a
    Functor, (forall m. Monoid m => Pattern' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
    -> (forall a. (a -> a -> a) -> Pattern' a -> a)
    -> (forall a. (a -> a -> a) -> Pattern' a -> a)
    -> (forall a. Pattern' a -> [a])
    -> (forall a. Pattern' a -> Bool)
    -> (forall a. Pattern' a -> Int)
    -> (forall a. Eq a => a -> Pattern' a -> Bool)
    -> (forall a. Ord a => Pattern' a -> a)
    -> (forall a. Ord a => Pattern' a -> a)
    -> (forall a. Num a => Pattern' a -> a)
    -> (forall a. Num a => Pattern' a -> a)
    -> Foldable Pattern'
    forall a. Eq a => a -> Pattern' a -> Bool
    forall a. Num a => Pattern' a -> a
    forall a. Ord a => Pattern' a -> a
    forall m. Monoid m => Pattern' m -> m
    forall a. Pattern' a -> Bool
    forall a. Pattern' a -> Int
    forall a. Pattern' a -> [a]
    forall a. (a -> a -> a) -> Pattern' a -> a
    forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    forall a b. (a -> b -> b) -> b -> Pattern' 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 -> Int)
    -> (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
    $cfold :: forall m. Monoid m => Pattern' m -> m
    fold :: forall m. Monoid m => Pattern' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    $ctoList :: forall a. Pattern' a -> [a]
    toList :: forall a. Pattern' a -> [a]
    $cnull :: forall a. Pattern' a -> Bool
    null :: forall a. Pattern' a -> Bool
    $clength :: forall a. Pattern' a -> Int
    length :: forall a. Pattern' a -> Int
    $celem :: forall a. Eq a => a -> Pattern' a -> Bool
    elem :: forall a. Eq a => a -> Pattern' a -> Bool
    $cmaximum :: forall a. Ord a => Pattern' a -> a
    maximum :: forall a. Ord a => Pattern' a -> a
    $cminimum :: forall a. Ord a => Pattern' a -> a
    minimum :: forall a. Ord a => Pattern' a -> a
    $csum :: forall a. Num a => Pattern' a -> a
    sum :: forall a. Num a => Pattern' a -> a
    $cproduct :: forall a. Num a => Pattern' a -> a
    product :: forall a. Num a => Pattern' a -> a
    Foldable, Functor Pattern'
    Foldable Pattern'
    (Functor Pattern', Foldable Pattern') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Pattern' a -> f (Pattern' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Pattern' (f a) -> f (Pattern' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Pattern' a -> m (Pattern' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Pattern' (m a) -> m (Pattern' a))
    -> Traversable Pattern'
    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 => Pattern' (m a) -> m (Pattern' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pattern' a -> f (Pattern' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pattern' a -> f (Pattern' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pattern' a -> f (Pattern' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b)
    $csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
    sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
    Traversable, (forall x. Pattern' x -> Rep (Pattern' x) x)
    -> (forall x. Rep (Pattern' x) x -> Pattern' x)
    -> Generic (Pattern' x)
    forall x. Rep (Pattern' x) x -> Pattern' x
    forall x. Pattern' x -> Rep (Pattern' x) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall x x. Rep (Pattern' x) x -> Pattern' x
    forall x x. Pattern' x -> Rep (Pattern' x) x
    $cfrom :: forall x x. Pattern' x -> Rep (Pattern' x) x
    from :: forall x. Pattern' x -> Rep (Pattern' x) x
    $cto :: forall x x. Rep (Pattern' x) x -> Pattern' x
    to :: forall x. Rep (Pattern' x) x -> Pattern' x
    Generic)

    type Pattern = Pattern' PatVarName
        -- ^ The @PatVarName@ is a name suggestion.

    varP :: a -> Pattern' a
    varP :: forall a. a -> Pattern' a
    varP = PatternInfo -> a -> Pattern' a
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    defaultPatternInfo

    dotP :: Term -> Pattern' a
    dotP :: forall a. Term -> Pattern' a
    dotP = PatternInfo -> Term -> Pattern' a
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    defaultPatternInfo

    litP :: Literal -> Pattern' a
    litP :: forall a. Literal -> Pattern' a
    litP = PatternInfo -> Literal -> Pattern' a
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP PatternInfo
    defaultPatternInfo

    -- | Type used when numbering pattern variables.
    data DBPatVar = DBPatVar
      { DBPatVar -> [Char]
    dbPatVarName  :: PatVarName
      , DBPatVar -> Int
    dbPatVarIndex :: !Int
      } deriving (Int -> DBPatVar -> ShowS
    [DBPatVar] -> ShowS
    DBPatVar -> [Char]
    (Int -> DBPatVar -> ShowS)
    -> (DBPatVar -> [Char]) -> ([DBPatVar] -> ShowS) -> Show DBPatVar
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DBPatVar -> ShowS
    showsPrec :: Int -> DBPatVar -> ShowS
    $cshow :: DBPatVar -> [Char]
    show :: DBPatVar -> [Char]
    $cshowList :: [DBPatVar] -> ShowS
    showList :: [DBPatVar] -> ShowS
    Show, DBPatVar -> DBPatVar -> Bool
    (DBPatVar -> DBPatVar -> Bool)
    -> (DBPatVar -> DBPatVar -> Bool) -> Eq DBPatVar
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DBPatVar -> DBPatVar -> Bool
    == :: DBPatVar -> DBPatVar -> Bool
    $c/= :: DBPatVar -> DBPatVar -> Bool
    /= :: DBPatVar -> DBPatVar -> Bool
    Eq, (forall x. DBPatVar -> Rep DBPatVar x)
    -> (forall x. Rep DBPatVar x -> DBPatVar) -> Generic DBPatVar
    forall x. Rep DBPatVar x -> DBPatVar
    forall x. DBPatVar -> Rep DBPatVar x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DBPatVar -> Rep DBPatVar x
    from :: forall x. DBPatVar -> Rep DBPatVar x
    $cto :: forall x. Rep DBPatVar x -> DBPatVar
    to :: forall x. Rep DBPatVar x -> DBPatVar
    Generic)

    type DeBruijnPattern = Pattern' DBPatVar

    namedVarP :: PatVarName -> Named_ Pattern
    namedVarP :: [Char] -> Named_ Pattern
    namedVarP [Char]
    x = Maybe NamedName -> Pattern -> Named_ Pattern
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    named (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Pattern
    forall a. a -> Pattern' a
    varP [Char]
    x
      where named :: Maybe NamedName
    named = if [Char] -> Bool
    forall a. Underscore a => a -> Bool
    isUnderscore [Char]
    x then Maybe NamedName
    forall a. Maybe a
    Nothing else NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged [Char] -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged [Char] -> NamedName) -> Ranged [Char] -> NamedName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Ranged [Char]
    forall a. a -> Ranged a
    unranged [Char]
    x

    namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
    namedDBVarP :: Int -> [Char] -> Named_ DeBruijnPattern
    namedDBVarP Int
    m = ((Pattern -> DeBruijnPattern)
    -> Named_ Pattern -> Named_ DeBruijnPattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Pattern -> DeBruijnPattern)
     -> Named_ Pattern -> Named_ DeBruijnPattern)
    -> (([Char] -> DBPatVar) -> Pattern -> DeBruijnPattern)
    -> ([Char] -> DBPatVar)
    -> Named_ Pattern
    -> Named_ DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char] -> DBPatVar) -> Pattern -> DeBruijnPattern
    forall a b. (a -> b) -> Pattern' a -> Pattern' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (\[Char]
    x -> [Char] -> Int -> DBPatVar
    DBPatVar [Char]
    x Int
    m) (Named_ Pattern -> Named_ DeBruijnPattern)
    -> ([Char] -> Named_ Pattern) -> [Char] -> Named_ DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Named_ Pattern
    namedVarP

    -- | Make an absurd pattern with the given de Bruijn index.
    absurdP :: Int -> DeBruijnPattern
    absurdP :: Int -> DeBruijnPattern
    absurdP = PatternInfo -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> x -> Pattern' x
    VarP (PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    PatOAbsurd []) (DBPatVar -> DeBruijnPattern)
    -> (Int -> DBPatVar) -> Int -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Int -> DBPatVar
    DBPatVar [Char]
    absurdPatternName

    -- | The @ConPatternInfo@ states whether the constructor belongs to
    --   a record type (@True@) or data type (@False@).
    --   In the former case, the @PatOrigin@ of the @conPInfo@ says
    --   whether the record pattern orginates from the expansion of an
    --   implicit pattern.
    --   The @Type@ is the type of the whole record pattern.
    --   The scope used for the type is given by any outer scope
    --   plus the clause's telescope ('clauseTel').
    data ConPatternInfo = ConPatternInfo
      { ConPatternInfo -> PatternInfo
    conPInfo   :: PatternInfo
        -- ^ Information on the origin of the pattern.
      , ConPatternInfo -> Bool
    conPRecord :: Bool
        -- ^ @False@ if data constructor.
        --   @True@ if record constructor.
      , ConPatternInfo -> Bool
    conPFallThrough :: Bool
        -- ^ Should the match block on non-canonical terms or can it
        --   proceed to the catch-all clause?
      , ConPatternInfo -> Maybe (Arg Type)
    conPType   :: Maybe (Arg Type)
        -- ^ The type of the whole constructor pattern.
        --   Should be present (@Just@) if constructor pattern is
        --   is generated ordinarily by type-checking.
        --   Could be absent (@Nothing@) if pattern comes from some
        --   plugin (like Agsy).
        --   Needed e.g. for with-clause stripping.
      , ConPatternInfo -> Bool
    conPLazy :: Bool
        -- ^ Lazy patterns are generated by the forcing translation in the unifier
        --   ('Agda.TypeChecking.Rules.LHS.Unify.unifyStep') and are dropped by
        --   the clause compiler (TODO: not yet)
        --   ('Agda.TypeChecking.CompiledClause.Compile.compileClauses') when the
        --   variables they bind are unused. The GHC backend compiles lazy matches
        --   to lazy patterns in Haskell (TODO: not yet).
      }
      deriving (Int -> ConPatternInfo -> ShowS
    [ConPatternInfo] -> ShowS
    ConPatternInfo -> [Char]
    (Int -> ConPatternInfo -> ShowS)
    -> (ConPatternInfo -> [Char])
    -> ([ConPatternInfo] -> ShowS)
    -> Show ConPatternInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ConPatternInfo -> ShowS
    showsPrec :: Int -> ConPatternInfo -> ShowS
    $cshow :: ConPatternInfo -> [Char]
    show :: ConPatternInfo -> [Char]
    $cshowList :: [ConPatternInfo] -> ShowS
    showList :: [ConPatternInfo] -> ShowS
    Show, (forall x. ConPatternInfo -> Rep ConPatternInfo x)
    -> (forall x. Rep ConPatternInfo x -> ConPatternInfo)
    -> Generic ConPatternInfo
    forall x. Rep ConPatternInfo x -> ConPatternInfo
    forall x. ConPatternInfo -> Rep ConPatternInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ConPatternInfo -> Rep ConPatternInfo x
    from :: forall x. ConPatternInfo -> Rep ConPatternInfo x
    $cto :: forall x. Rep ConPatternInfo x -> ConPatternInfo
    to :: forall x. Rep ConPatternInfo x -> ConPatternInfo
    Generic)

    noConPatternInfo :: ConPatternInfo
    noConPatternInfo :: ConPatternInfo
    noConPatternInfo = PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo PatternInfo
    defaultPatternInfo Bool
    False Bool
    False Maybe (Arg Type)
    forall a. Maybe a
    Nothing Bool
    False

    -- | Build partial 'ConPatternInfo' from 'ConInfo'
    toConPatternInfo :: ConInfo -> ConPatternInfo
    toConPatternInfo :: ConInfo -> ConPatternInfo
    toConPatternInfo ConInfo
    ConORec = ConPatternInfo
    noConPatternInfo{ conPInfo = PatternInfo PatORec [] , conPRecord = True }
    toConPatternInfo ConInfo
    _ = ConPatternInfo
    noConPatternInfo

    -- | Build 'ConInfo' from 'ConPatternInfo'.
    fromConPatternInfo :: ConPatternInfo -> ConInfo
    fromConPatternInfo :: ConPatternInfo -> ConInfo
    fromConPatternInfo ConPatternInfo
    i = PatOrigin -> ConInfo
    patToConO (PatOrigin -> ConInfo) -> PatOrigin -> ConInfo
    forall a b. (a -> b) -> a -> b
    $ PatternInfo -> PatOrigin
    patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    i
      where
        patToConO :: PatOrigin -> ConOrigin
        patToConO :: PatOrigin -> ConInfo
    patToConO = \case
          PatOrigin
    PatOSystem -> ConInfo
    ConOSystem
          PatOrigin
    PatOSplit  -> ConInfo
    ConOSplit
          PatOSplitArg{} -> ConInfo
    ConOSystem
          PatOVar{}  -> ConInfo
    ConOSystem
          PatOrigin
    PatODot    -> ConInfo
    ConOSystem
          PatOrigin
    PatOWild   -> ConInfo
    ConOSystem
          PatOrigin
    PatOCon    -> ConInfo
    ConOCon
          PatOrigin
    PatORec    -> ConInfo
    ConORec
          PatOrigin
    PatOLit    -> ConInfo
    ConOCon
          PatOrigin
    PatOAbsurd -> ConInfo
    ConOSystem

    -- | Extract pattern variables in left-to-right order.
    --   A 'DotP' is also treated as variable (see docu for 'Clause').
    class PatternVars a where
      type PatternVarOut a
      patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]

    instance PatternVars (Arg (Pattern' a)) where
      type PatternVarOut (Arg (Pattern' a)) = a

      -- patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
      patternVars :: Arg (Pattern' a)
    -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
    patternVars (Arg ArgInfo
    i (VarP PatternInfo
    _ a
    x)   ) = [ArgInfo
    -> Either (PatternVarOut (Arg (Pattern' a))) Term
    -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Either (PatternVarOut (Arg (Pattern' a))) Term
     -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
    -> Either (PatternVarOut (Arg (Pattern' a))) Term
    -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
    forall a b. (a -> b) -> a -> b
    $ a -> Either a Term
    forall a b. a -> Either a b
    Left a
    x]
      patternVars (Arg ArgInfo
    i (DotP PatternInfo
    _ Term
    t)   ) = [ArgInfo
    -> Either (PatternVarOut (Arg (Pattern' a))) Term
    -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Either (PatternVarOut (Arg (Pattern' a))) Term
     -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
    -> Either (PatternVarOut (Arg (Pattern' a))) Term
    -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Either a Term
    forall a b. b -> Either a b
    Right Term
    t]
      patternVars (Arg ArgInfo
    _ (ConP ConHead
    _ ConPatternInfo
    _ [NamedArg (Pattern' a)]
    ps)) = [NamedArg (Pattern' a)]
    -> [Arg (Either (PatternVarOut [NamedArg (Pattern' a)]) Term)]
    forall a.
    PatternVars a =>
    a -> [Arg (Either (PatternVarOut a) Term)]
    patternVars [NamedArg (Pattern' a)]
    ps
      patternVars (Arg ArgInfo
    _ (DefP PatternInfo
    _ QName
    _ [NamedArg (Pattern' a)]
    ps)) = [NamedArg (Pattern' a)]
    -> [Arg (Either (PatternVarOut [NamedArg (Pattern' a)]) Term)]
    forall a.
    PatternVars a =>
    a -> [Arg (Either (PatternVarOut a) Term)]
    patternVars [NamedArg (Pattern' a)]
    ps
      patternVars (Arg ArgInfo
    _ (LitP PatternInfo
    _ Literal
    _)   ) = []
      patternVars (Arg ArgInfo
    _ ProjP{}      ) = []
      patternVars (Arg ArgInfo
    i (IApplyP PatternInfo
    _ Term
    _ Term
    _ a
    x)) = [ArgInfo
    -> Either (PatternVarOut (Arg (Pattern' a))) Term
    -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Either (PatternVarOut (Arg (Pattern' a))) Term
     -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
    -> Either (PatternVarOut (Arg (Pattern' a))) Term
    -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
    forall a b. (a -> b) -> a -> b
    $ a -> Either a Term
    forall a b. a -> Either a b
    Left a
    x]

    instance PatternVars (NamedArg (Pattern' a)) where
      type PatternVarOut (NamedArg (Pattern' a)) = a

      patternVars :: NamedArg (Pattern' a)
    -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)]
    patternVars = Arg (Pattern' a) -> [Arg (Either a Term)]
    Arg (Pattern' a)
    -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
    forall a.
    PatternVars a =>
    a -> [Arg (Either (PatternVarOut a) Term)]
    patternVars (Arg (Pattern' a) -> [Arg (Either a Term)])
    -> (NamedArg (Pattern' a) -> Arg (Pattern' a))
    -> NamedArg (Pattern' a)
    -> [Arg (Either a Term)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named_ (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a) -> Arg (Pattern' a)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named_ (Pattern' a) -> Pattern' a
    forall name a. Named name a -> a
    namedThing

    instance PatternVars a => PatternVars [a] where
      type PatternVarOut [a] = PatternVarOut a

      patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)]
    patternVars = (a -> [Arg (Either (PatternVarOut a) Term)])
    -> [a] -> [Arg (Either (PatternVarOut a) Term)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap a -> [Arg (Either (PatternVarOut a) Term)]
    forall a.
    PatternVars a =>
    a -> [Arg (Either (PatternVarOut a) Term)]
    patternVars

    -- | Retrieve the PatternInfo from a pattern
    patternInfo :: Pattern' x -> Maybe PatternInfo
    patternInfo :: forall x. Pattern' x -> Maybe PatternInfo
    patternInfo (VarP PatternInfo
    i x
    _)        = PatternInfo -> Maybe PatternInfo
    forall a. a -> Maybe a
    Just PatternInfo
    i
    patternInfo (DotP PatternInfo
    i Term
    _)        = PatternInfo -> Maybe PatternInfo
    forall a. a -> Maybe a
    Just PatternInfo
    i
    patternInfo (LitP PatternInfo
    i Literal
    _)        = PatternInfo -> Maybe PatternInfo
    forall a. a -> Maybe a
    Just PatternInfo
    i
    patternInfo (ConP ConHead
    _ ConPatternInfo
    ci [NamedArg (Pattern' x)]
    _)     = PatternInfo -> Maybe PatternInfo
    forall a. a -> Maybe a
    Just (PatternInfo -> Maybe PatternInfo)
    -> PatternInfo -> Maybe PatternInfo
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    ci
    patternInfo ProjP{}           = Maybe PatternInfo
    forall a. Maybe a
    Nothing
    patternInfo (IApplyP PatternInfo
    i Term
    _ Term
    _ x
    _) = PatternInfo -> Maybe PatternInfo
    forall a. a -> Maybe a
    Just PatternInfo
    i
    patternInfo (DefP PatternInfo
    i QName
    _ [NamedArg (Pattern' x)]
    _)      = PatternInfo -> Maybe PatternInfo
    forall a. a -> Maybe a
    Just PatternInfo
    i

    -- | Retrieve the origin of a pattern
    patternOrigin :: Pattern' x -> Maybe PatOrigin
    patternOrigin :: forall x. Pattern' x -> Maybe PatOrigin
    patternOrigin = (PatternInfo -> PatOrigin) -> Maybe PatternInfo -> Maybe PatOrigin
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap PatternInfo -> PatOrigin
    patOrigin (Maybe PatternInfo -> Maybe PatOrigin)
    -> (Pattern' x -> Maybe PatternInfo)
    -> Pattern' x
    -> Maybe PatOrigin
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern' x -> Maybe PatternInfo
    forall x. Pattern' x -> Maybe PatternInfo
    patternInfo

    instance IsProjP (Pattern' a) where
      isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP = \case
        ProjP ProjOrigin
    o QName
    d -> (ProjOrigin, AmbiguousQName) -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. a -> Maybe a
    Just (ProjOrigin
    o, QName -> AmbiguousQName
    unambiguous QName
    d)
        Pattern' a
    _ -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. Maybe a
    Nothing

    -----------------------------------------------------------------------------
    -- * Explicit substitutions
    -----------------------------------------------------------------------------

    -- | Substitutions.

    data Substitution' a

      = IdS
        -- ^ Identity substitution.
        --   @Γ ⊢ IdS : Γ@

      | EmptyS Impossible
        -- ^ Empty substitution, lifts from the empty context. First argument is @__IMPOSSIBLE__@.
        --   Apply this to closed terms you want to use in a non-empty context.
        --   @Γ ⊢ EmptyS : ()@

      | a :# Substitution' a
        -- ^ Substitution extension, ``cons''.
        --   @
        --     Γ ⊢ u : Aρ   Γ ⊢ ρ : Δ
        --     ----------------------
        --     Γ ⊢ u :# ρ : Δ, A
        --   @

      | Strengthen Impossible !Int (Substitution' a)
        -- ^ Strengthening substitution.  First argument is @__IMPOSSIBLE__@.
        --   In @'Strengthen err n ρ@ the number @n@ must be non-negative.
        --   This substitution should only be applied to values @t@ for
        --   which none of the variables @0@ up to @n - 1@ are free in
        --   @t[ρ]@, and in that case @n@ is subtracted from all free de
        --   Bruijn indices in @t[ρ]@.
        --        Γ ⊢ ρ : Δ    |Θ| = n
        --     ---------------------------
        --     Γ ⊢ Strengthen n ρ : Δ, Θ
        --   @

      | Wk !Int (Substitution' a)
        -- ^ Weakening substitution, lifts to an extended context.
        --   @
        --         Γ ⊢ ρ : Δ
        --     -------------------
        --     Γ, Ψ ⊢ Wk |Ψ| ρ : Δ
        --   @

      | Lift !Int (Substitution' a)
        -- ^ Lifting substitution.  Use this to go under a binder.
        --   @Lift 1 ρ == var 0 :# Wk 1 ρ@.
        --   @
        --            Γ ⊢ ρ : Δ
        --     -------------------------
        --     Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ
        --   @

      deriving ( Int -> Substitution' a -> ShowS
    [Substitution' a] -> ShowS
    Substitution' a -> [Char]
    (Int -> Substitution' a -> ShowS)
    -> (Substitution' a -> [Char])
    -> ([Substitution' a] -> ShowS)
    -> Show (Substitution' a)
    forall a. Show a => Int -> Substitution' a -> ShowS
    forall a. Show a => [Substitution' a] -> ShowS
    forall a. Show a => Substitution' a -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> Substitution' a -> ShowS
    showsPrec :: Int -> Substitution' a -> ShowS
    $cshow :: forall a. Show a => Substitution' a -> [Char]
    show :: Substitution' a -> [Char]
    $cshowList :: forall a. Show a => [Substitution' a] -> ShowS
    showList :: [Substitution' a] -> ShowS
    Show
               , (forall a b. (a -> b) -> Substitution' a -> Substitution' b)
    -> (forall a b. a -> Substitution' b -> Substitution' a)
    -> Functor Substitution'
    forall a b. a -> Substitution' b -> Substitution' a
    forall a b. (a -> b) -> Substitution' a -> Substitution' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Substitution' a -> Substitution' b
    fmap :: forall a b. (a -> b) -> Substitution' a -> Substitution' b
    $c<$ :: forall a b. a -> Substitution' b -> Substitution' a
    <$ :: forall a b. a -> Substitution' b -> Substitution' a
    Functor
               , (forall m. Monoid m => Substitution' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Substitution' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Substitution' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Substitution' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Substitution' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Substitution' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Substitution' a -> b)
    -> (forall a. (a -> a -> a) -> Substitution' a -> a)
    -> (forall a. (a -> a -> a) -> Substitution' a -> a)
    -> (forall a. Substitution' a -> [a])
    -> (forall a. Substitution' a -> Bool)
    -> (forall a. Substitution' a -> Int)
    -> (forall a. Eq a => a -> Substitution' a -> Bool)
    -> (forall a. Ord a => Substitution' a -> a)
    -> (forall a. Ord a => Substitution' a -> a)
    -> (forall a. Num a => Substitution' a -> a)
    -> (forall a. Num a => Substitution' a -> a)
    -> Foldable Substitution'
    forall a. Eq a => a -> Substitution' a -> Bool
    forall a. Num a => Substitution' a -> a
    forall a. Ord a => Substitution' a -> a
    forall m. Monoid m => Substitution' m -> m
    forall a. Substitution' a -> Bool
    forall a. Substitution' a -> Int
    forall a. Substitution' a -> [a]
    forall a. (a -> a -> a) -> Substitution' a -> a
    forall m a. Monoid m => (a -> m) -> Substitution' a -> m
    forall b a. (b -> a -> b) -> b -> Substitution' a -> b
    forall a b. (a -> b -> b) -> b -> Substitution' 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 -> Int)
    -> (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
    $cfold :: forall m. Monoid m => Substitution' m -> m
    fold :: forall m. Monoid m => Substitution' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Substitution' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Substitution' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Substitution' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Substitution' a -> a
    $ctoList :: forall a. Substitution' a -> [a]
    toList :: forall a. Substitution' a -> [a]
    $cnull :: forall a. Substitution' a -> Bool
    null :: forall a. Substitution' a -> Bool
    $clength :: forall a. Substitution' a -> Int
    length :: forall a. Substitution' a -> Int
    $celem :: forall a. Eq a => a -> Substitution' a -> Bool
    elem :: forall a. Eq a => a -> Substitution' a -> Bool
    $cmaximum :: forall a. Ord a => Substitution' a -> a
    maximum :: forall a. Ord a => Substitution' a -> a
    $cminimum :: forall a. Ord a => Substitution' a -> a
    minimum :: forall a. Ord a => Substitution' a -> a
    $csum :: forall a. Num a => Substitution' a -> a
    sum :: forall a. Num a => Substitution' a -> a
    $cproduct :: forall a. Num a => Substitution' a -> a
    product :: forall a. Num a => Substitution' a -> a
    Foldable
               , Functor Substitution'
    Foldable Substitution'
    (Functor Substitution', Foldable Substitution') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Substitution' a -> f (Substitution' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Substitution' (f a) -> f (Substitution' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Substitution' a -> m (Substitution' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Substitution' (m a) -> m (Substitution' a))
    -> Traversable Substitution'
    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 =>
    Substitution' (m a) -> m (Substitution' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Substitution' (f a) -> f (Substitution' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Substitution' a -> m (Substitution' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Substitution' a -> f (Substitution' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Substitution' a -> f (Substitution' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Substitution' a -> f (Substitution' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Substitution' (f a) -> f (Substitution' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Substitution' (f a) -> f (Substitution' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Substitution' a -> m (Substitution' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Substitution' a -> m (Substitution' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    Substitution' (m a) -> m (Substitution' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    Substitution' (m a) -> m (Substitution' a)
    Traversable
               , (forall x. Substitution' a -> Rep (Substitution' a) x)
    -> (forall x. Rep (Substitution' a) x -> Substitution' a)
    -> Generic (Substitution' a)
    forall x. Rep (Substitution' a) x -> Substitution' a
    forall x. Substitution' a -> Rep (Substitution' a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (Substitution' a) x -> Substitution' a
    forall a x. Substitution' a -> Rep (Substitution' a) x
    $cfrom :: forall a x. Substitution' a -> Rep (Substitution' a) x
    from :: forall x. Substitution' a -> Rep (Substitution' a) x
    $cto :: forall a x. Rep (Substitution' a) x -> Substitution' a
    to :: forall x. Rep (Substitution' a) x -> Substitution' a
    Generic
               )

    type Substitution = Substitution' Term
    type PatternSubstitution = Substitution' DeBruijnPattern

    infixr 4 :#

    instance Null (Substitution' a) where
      empty :: Substitution' a
    empty = Substitution' a
    forall a. Substitution' a
    IdS
      null :: Substitution' a -> Bool
    null Substitution' a
    IdS = Bool
    True
      null Substitution' a
    _   = Bool
    False

    ---------------------------------------------------------------------------
    -- * Views
    ---------------------------------------------------------------------------

    -- | View type as equality type.

    data EqualityView
      = EqualityViewType EqualityTypeData
          -- ^ A type of the form @u ≡ v@ decomposed into its parts.
          --   Used as type for the @rewrite@ expression.
      | OtherType Type
          -- ^ A reduced type used as type for a @with@ expression.
      | IdiomType Type
          -- ^ A reduced type used as type for the @with@ inspect idiom.

    data EqualityTypeData = EqualityTypeData
        { EqualityTypeData -> Range
    _eqtRange  :: Range       -- ^ Range of the @rewrite@ expression, if any.
        , EqualityTypeData -> Sort
    _eqtSort   :: Sort        -- ^ Sort of this type.
        , EqualityTypeData -> QName
    _eqtName   :: QName       -- ^ Builtin EQUALITY.
        , EqualityTypeData -> Args
    _eqtParams :: Args        -- ^ Hidden.  Empty or @Level@.
        , EqualityTypeData -> Arg Term
    _eqtType   :: Arg Term    -- ^ Hidden.
        , EqualityTypeData -> Arg Term
    _eqtLhs    :: Arg Term    -- ^ NotHidden.
        , EqualityTypeData -> Arg Term
    _eqtRhs    :: Arg Term    -- ^ NotHidden.
        }

    pattern EqualityType ::
         Range
      -> Sort
      -> QName
      -> Args
      -> Arg Term
      -> Arg Term
      -> Arg Term
      -> EqualityView
    pattern $mEqualityType :: forall {r}.
    EqualityView
    -> (Range
        -> Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> r)
    -> ((# #) -> r)
    -> r
    $bEqualityType :: Range
    -> Sort
    -> QName
    -> Args
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityView
    EqualityType{ EqualityView -> Range
    eqtRange, EqualityView -> Sort
    eqtSort, EqualityView -> QName
    eqtName, EqualityView -> Args
    eqtParams, EqualityView -> Arg Term
    eqtType, EqualityView -> Arg Term
    eqtLhs, EqualityView -> Arg Term
    eqtRhs } =
      EqualityViewType (EqualityTypeData eqtRange eqtSort eqtName eqtParams eqtType eqtLhs eqtRhs)

    {-# COMPLETE EqualityType, OtherType, IdiomType #-}

    isEqualityType :: EqualityView -> Bool
    isEqualityType :: EqualityView -> Bool
    isEqualityType EqualityType{} = Bool
    True
    isEqualityType OtherType{}    = Bool
    False
    isEqualityType IdiomType{}    = Bool
    False

    -- | View type as path type.

    data PathView
      = PathType
        { PathView -> Sort
    pathSort  :: Sort     -- ^ Sort of this type.
        , PathView -> QName
    pathName  :: QName    -- ^ Builtin PATH.
        , PathView -> Arg Term
    pathLevel :: Arg Term -- ^ Hidden
        , PathView -> Arg Term
    pathType  :: Arg Term -- ^ Hidden
        , PathView -> Arg Term
    pathLhs   :: Arg Term -- ^ NotHidden
        , PathView -> Arg Term
    pathRhs   :: Arg Term -- ^ NotHidden
        }
      | OType Type -- ^ reduced

    isPathType :: PathView -> Bool
    isPathType :: PathView -> Bool
    isPathType PathType{} = Bool
    True
    isPathType OType{}    = Bool
    False

    data IntervalView
          = IZero
          | IOne
          | IMin (Arg Term) (Arg Term)
          | IMax (Arg Term) (Arg Term)
          | INeg (Arg Term)
          | OTerm Term
          deriving Int -> IntervalView -> ShowS
    [IntervalView] -> ShowS
    IntervalView -> [Char]
    (Int -> IntervalView -> ShowS)
    -> (IntervalView -> [Char])
    -> ([IntervalView] -> ShowS)
    -> Show IntervalView
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IntervalView -> ShowS
    showsPrec :: Int -> IntervalView -> ShowS
    $cshow :: IntervalView -> [Char]
    show :: IntervalView -> [Char]
    $cshowList :: [IntervalView] -> ShowS
    showList :: [IntervalView] -> ShowS
    Show

    isIOne :: IntervalView -> Bool
    isIOne :: IntervalView -> Bool
    isIOne IntervalView
    IOne = Bool
    True
    isIOne IntervalView
    _ = Bool
    False

    ---------------------------------------------------------------------------
    -- * Absurd Lambda
    ---------------------------------------------------------------------------

    -- | Absurd lambdas are internally represented as identity
    --   with variable name "()".
    absurdBody :: Abs Term
    absurdBody :: Abs Term
    absurdBody = [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    absurdPatternName (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    0 []

    isAbsurdBody :: Abs Term -> Bool
    isAbsurdBody :: Abs Term -> Bool
    isAbsurdBody (Abs [Char]
    x (Var Int
    0 [])) = [Char] -> Bool
    isAbsurdPatternName [Char]
    x
    isAbsurdBody Abs Term
    _                  = Bool
    False

    absurdPatternName :: PatVarName
    absurdPatternName :: [Char]
    absurdPatternName = [Char]
    "()"

    isAbsurdPatternName :: PatVarName -> Bool
    isAbsurdPatternName :: [Char] -> Bool
    isAbsurdPatternName [Char]
    x = [Char]
    x [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    absurdPatternName

    ---------------------------------------------------------------------------
    -- * Smart constructors
    ---------------------------------------------------------------------------

    -- | An unapplied variable.
    var :: Nat -> Term
    var :: Int -> Term
    var Int
    i | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0    = Int -> Elims -> Term
    Var Int
    i []
          | Bool
    otherwise = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Add 'DontCare' is it is not already a @DontCare@.
    dontCare :: Term -> Term
    dontCare :: Term -> Term
    dontCare Term
    v =
      case Term
    v of
        DontCare{} -> Term
    v
        Term
    _          -> Term -> Term
    DontCare Term
    v

    type DummyTermKind = String

    -- | Construct a string representing the call-site that created the dummy thing.
    dummyLocName :: CallStack -> String
    dummyLocName :: CallStack -> [Char]
    dummyLocName CallStack
    cs = [Char] -> (CallSite -> [Char]) -> Maybe CallSite -> [Char]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ CallSite -> [Char]
    prettyCallSite (CallStack -> Maybe CallSite
    headCallSite CallStack
    cs)

    -- | Aux: A dummy term to constitute a dummy term/level/sort/type.
    dummyTermWith :: DummyTermKind -> CallStack -> Term
    dummyTermWith :: [Char] -> CallStack -> Term
    dummyTermWith [Char]
    kind CallStack
    cs = ([Char] -> Elims -> Term) -> Elims -> [Char] -> Term
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip [Char] -> Elims -> Term
    Dummy [] ([Char] -> Term) -> [Char] -> Term
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    kind, [Char]
    ": ", CallStack -> [Char]
    dummyLocName CallStack
    cs]

    __DUMMY_TERM_WITH__ :: HasCallStack => DummyTermKind -> Term
    __DUMMY_TERM_WITH__ :: HasCallStack => [Char] -> Term
    __DUMMY_TERM_WITH__ = (CallStack -> Term) -> Term
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> Term) -> Term)
    -> ([Char] -> CallStack -> Term) -> [Char] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> CallStack -> Term
    dummyTermWith

    -- | A dummy term created at location.
    --   Note: use macro __DUMMY_TERM__ !
    dummyTerm :: CallStack -> Term
    dummyTerm :: CallStack -> Term
    dummyTerm = [Char] -> CallStack -> Term
    dummyTermWith [Char]
    "dummyTerm"

    __DUMMY_TERM__ :: HasCallStack => Term
    __DUMMY_TERM__ :: HasCallStack => Term
    __DUMMY_TERM__ = (CallStack -> Term) -> Term
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Term
    dummyTerm

    -- | A dummy level to constitute a level/sort created at location.
    --   Note: use macro __DUMMY_LEVEL__ !
    dummyLevel :: CallStack -> Level
    dummyLevel :: CallStack -> Level
    dummyLevel = Term -> Level
    forall t. t -> Level' t
    atomicLevel (Term -> Level) -> (CallStack -> Term) -> CallStack -> Level
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> CallStack -> Term
    dummyTermWith [Char]
    "dummyLevel"

    __DUMMY_LEVEL__ :: HasCallStack => Level
    __DUMMY_LEVEL__ :: HasCallStack => Level
    __DUMMY_LEVEL__ = (CallStack -> Level) -> Level
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Level
    dummyLevel

    -- | A dummy sort created at location.
    --   Note: use macro __DUMMY_SORT__ !
    dummySort :: CallStack -> Sort
    dummySort :: CallStack -> Sort
    dummySort = [Char] -> Sort
    forall t. [Char] -> Sort' t
    DummyS ([Char] -> Sort) -> (CallStack -> [Char]) -> CallStack -> Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> [Char]
    dummyLocName

    __DUMMY_SORT__ :: HasCallStack => Sort
    __DUMMY_SORT__ :: HasCallStack => Sort
    __DUMMY_SORT__ = (CallStack -> Sort) -> Sort
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Sort
    dummySort

    -- | A dummy type created at location.
    --   Note: use macro __DUMMY_TYPE__ !
    dummyType :: CallStack -> Type
    dummyType :: CallStack -> Type
    dummyType CallStack
    cs = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (CallStack -> Sort
    dummySort CallStack
    cs) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ [Char] -> CallStack -> Term
    dummyTermWith [Char]
    "dummyType" CallStack
    cs

    __DUMMY_TYPE__ :: HasCallStack => Type
    __DUMMY_TYPE__ :: HasCallStack => Type
    __DUMMY_TYPE__ = (CallStack -> Type) -> Type
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Type
    dummyType

    -- | Context entries without a type have this dummy type.
    --   Note: use macro __DUMMY_DOM__ !
    dummyDom :: CallStack -> Dom Type
    dummyDom :: CallStack -> Dom Type
    dummyDom = Type -> Dom Type
    forall a. a -> Dom a
    defaultDom (Type -> Dom Type) -> (CallStack -> Type) -> CallStack -> Dom Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> Type
    dummyType

    __DUMMY_DOM__ :: HasCallStack => Dom Type
    __DUMMY_DOM__ :: HasCallStack => Dom Type
    __DUMMY_DOM__ = (CallStack -> Dom Type) -> Dom Type
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Dom Type
    dummyDom

    -- | Constant level @n@
    pattern ClosedLevel :: Integer -> Level
    pattern $mClosedLevel :: forall {r}. Level -> (Integer -> r) -> ((# #) -> r) -> r
    $bClosedLevel :: Integer -> Level
    ClosedLevel n = Max n []

    atomicLevel :: t -> Level' t
    atomicLevel :: forall t. t -> Level' t
    atomicLevel t
    a = Integer -> [PlusLevel' t] -> Level' t
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 [ Integer -> t -> PlusLevel' t
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    0 t
    a ]

    varSort :: Int -> Sort
    varSort :: Int -> Sort
    varSort Int
    n = Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> Level
    forall t. t -> Level' t
    atomicLevel (Term -> Level) -> Term -> Level
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    n

    tmSort :: Term -> Sort
    tmSort :: Term -> Sort
    tmSort Term
    t = Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> Level
    forall t. t -> Level' t
    atomicLevel Term
    t

    tmSSort :: Term -> Sort
    tmSSort :: Term -> Sort
    tmSSort Term
    t = Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Term -> Level
    forall t. t -> Level' t
    atomicLevel Term
    t

    -- | Given a constant @m@ and level @l@, compute @m + l@
    levelPlus :: Integer -> Level -> Level
    levelPlus :: Integer -> Level -> Level
    levelPlus Integer
    m (Max Integer
    n [PlusLevel' Term]
    as) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max (Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
    forall a b. (a -> b) -> a -> b
    $ (PlusLevel' Term -> PlusLevel' Term)
    -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' Term -> PlusLevel' Term
    pplus [PlusLevel' Term]
    as
      where pplus :: PlusLevel' Term -> PlusLevel' Term
    pplus (Plus Integer
    n Term
    l) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    n) Term
    l

    levelSuc :: Level -> Level
    levelSuc :: Level -> Level
    levelSuc = Integer -> Level -> Level
    levelPlus Integer
    1

    mkType :: Integer -> Sort
    mkType :: Integer -> Sort
    mkType Integer
    n = Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    n

    mkProp :: Integer -> Sort
    mkProp :: Integer -> Sort
    mkProp Integer
    n = Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    n

    mkSSet :: Integer -> Sort
    mkSSet :: Integer -> Sort
    mkSSet Integer
    n = Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    n

    impossibleTerm :: CallStack -> Term
    impossibleTerm :: CallStack -> Term
    impossibleTerm = ([Char] -> Elims -> Term) -> Elims -> [Char] -> Term
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip [Char] -> Elims -> Term
    Dummy [] ([Char] -> Term) -> (CallStack -> [Char]) -> CallStack -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Impossible -> [Char]
    forall a. Show a => a -> [Char]
    show (Impossible -> [Char])
    -> (CallStack -> Impossible) -> CallStack -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> Impossible
    Impossible

    ---------------------------------------------------------------------------
    -- * Sorts.
    ---------------------------------------------------------------------------

    isSort :: Term -> Maybe Sort
    isSort :: Term -> Maybe Sort
    isSort = \case
      Sort Sort
    s -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just Sort
    s
      Term
    _      -> Maybe Sort
    forall a. Maybe a
    Nothing

    -- | Get the flavor of the universe. 'Nothing' could also mean "don't know".
    sortUniv :: Sort' t -> Maybe Univ
    sortUniv :: forall t. Sort' t -> Maybe Univ
    sortUniv = \case
      Univ Univ
    u Level' t
    _ -> Univ -> Maybe Univ
    forall a. a -> Maybe a
    Just Univ
    u
      Inf  Univ
    u Integer
    _ -> Univ -> Maybe Univ
    forall a. a -> Maybe a
    Just Univ
    u
      Sort' t
    _        -> Maybe Univ
    forall a. Maybe a
    Nothing

    -- | Is this a Prop universe?  Answers are yes ('True') or maybe ('False').
    isProp :: Sort' t -> Bool
    isProp :: forall t. Sort' t -> Bool
    isProp = (Univ -> Maybe Univ
    forall a. a -> Maybe a
    Just Univ
    UProp Maybe Univ -> Maybe Univ -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe Univ -> Bool) -> (Sort' t -> Maybe Univ) -> Sort' t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort' t -> Maybe Univ
    forall t. Sort' t -> Maybe Univ
    sortUniv

    -- | Is this a strict universe inhabitable by data types?
    isStrictDataSort :: Sort' t -> Bool
    isStrictDataSort :: forall t. Sort' t -> Bool
    isStrictDataSort = Bool -> (Univ -> Bool) -> Maybe Univ -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False ((IsFibrant
    IsStrict IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (IsFibrant -> Bool) -> (Univ -> IsFibrant) -> Univ -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Univ -> IsFibrant
    univFibrancy) (Maybe Univ -> Bool) -> (Sort' t -> Maybe Univ) -> Sort' t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort' t -> Maybe Univ
    forall t. Sort' t -> Maybe Univ
    sortUniv

    -- | Turn a known 'UProp' sort into a 'UType' sort, leave others unchanged.
    propToType :: Sort' t -> Sort' t
    propToType :: forall t. Sort' t -> Sort' t
    propToType = \case
      Univ Univ
    UProp Level' t
    l -> Univ -> Level' t -> Sort' t
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    UType Level' t
    l
      Inf  Univ
    UProp Integer
    l -> Univ -> Integer -> Sort' t
    forall t. Univ -> Integer -> Sort' t
    Inf  Univ
    UType Integer
    l
      Sort' t
    s -> Sort' t
    s

    ---------------------------------------------------------------------------
    -- * Telescopes.
    ---------------------------------------------------------------------------

    -- | A traversal for the names in a telescope.
    mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
    mapAbsNamesM :: forall (m :: * -> *) a.
    Applicative m =>
    ([Char] -> m [Char]) -> Tele a -> m (Tele a)
    mapAbsNamesM [Char] -> m [Char]
    f Tele a
    EmptyTel                  = Tele a -> m (Tele a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Tele a
    forall a. Tele a
    EmptyTel
    mapAbsNamesM [Char] -> m [Char]
    f (ExtendTel a
    a (  Abs [Char]
    x Tele a
    b)) = a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel a
    a (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (  [Char] -> Tele a -> Abs (Tele a)
    forall a. [Char] -> a -> Abs a
    Abs ([Char] -> Tele a -> Abs (Tele a))
    -> m [Char] -> m (Tele a -> Abs (Tele a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> m [Char]
    f [Char]
    x m (Tele a -> Abs (Tele a)) -> m (Tele a) -> m (Abs (Tele a))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ([Char] -> m [Char]) -> Tele a -> m (Tele a)
    forall (m :: * -> *) a.
    Applicative m =>
    ([Char] -> m [Char]) -> Tele a -> m (Tele a)
    mapAbsNamesM [Char] -> m [Char]
    f Tele a
    b)
    mapAbsNamesM [Char] -> m [Char]
    f (ExtendTel a
    a (NoAbs [Char]
    x Tele a
    b)) = a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel a
    a (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Char] -> Tele a -> Abs (Tele a)
    forall a. [Char] -> a -> Abs a
    NoAbs ([Char] -> Tele a -> Abs (Tele a))
    -> m [Char] -> m (Tele a -> Abs (Tele a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> m [Char]
    f [Char]
    x m (Tele a -> Abs (Tele a)) -> m (Tele a) -> m (Abs (Tele a))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ([Char] -> m [Char]) -> Tele a -> m (Tele a)
    forall (m :: * -> *) a.
    Applicative m =>
    ([Char] -> m [Char]) -> Tele a -> m (Tele a)
    mapAbsNamesM [Char] -> m [Char]
    f Tele a
    b)
      -- Ulf, 2013-11-06: Last case is really impossible but I'd rather find out we
      --                  violated that invariant somewhere other than here.

    mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
    mapAbsNames :: forall a. ShowS -> Tele a -> Tele a
    mapAbsNames ShowS
    f = Identity (Tele a) -> Tele a
    forall a. Identity a -> a
    runIdentity (Identity (Tele a) -> Tele a)
    -> (Tele a -> Identity (Tele a)) -> Tele a -> Tele a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char] -> Identity [Char]) -> Tele a -> Identity (Tele a)
    forall (m :: * -> *) a.
    Applicative m =>
    ([Char] -> m [Char]) -> Tele a -> m (Tele a)
    mapAbsNamesM ([Char] -> Identity [Char]
    forall a. a -> Identity a
    Identity ([Char] -> Identity [Char]) -> ShowS -> [Char] -> Identity [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    f)

    -- Ulf, 2013-11-06
    -- The record parameter is named "" inside the record module so we can avoid
    -- printing it (issue 208), but we don't want that to show up in the type of
    -- the functions in the module (issue 892). This function is used on the record
    -- module telescope before adding it to a type in
    -- TypeChecking.Monad.Signature.addConstant (to handle functions defined in
    -- record modules) and TypeChecking.Rules.Record.checkProjection (to handle
    -- record projections).
    replaceEmptyName :: ArgName -> Tele a -> Tele a
    replaceEmptyName :: forall a. [Char] -> Tele a -> Tele a
    replaceEmptyName [Char]
    x = ShowS -> Tele a -> Tele a
    forall a. ShowS -> Tele a -> Tele a
    mapAbsNames (ShowS -> Tele a -> Tele a) -> ShowS -> Tele a -> Tele a
    forall a b. (a -> b) -> a -> b
    $ \ [Char]
    y -> if [Char] -> Bool
    forall a. Null a => a -> Bool
    null [Char]
    y then [Char]
    x else [Char]
    y

    -- | Telescope as list.
    type ListTel' a = [Dom (a, Type)]
    type ListTel = ListTel' ArgName

    telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
    telFromList' :: forall a. (a -> [Char]) -> ListTel' a -> Telescope
    telFromList' a -> [Char]
    f = (Dom (a, Type) -> Telescope -> Telescope)
    -> Telescope -> [Dom (a, Type)] -> Telescope
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    List.foldr Dom (a, Type) -> Telescope -> Telescope
    extTel Telescope
    forall a. Tele a
    EmptyTel
      where
        extTel :: Dom (a, Type) -> Telescope -> Telescope
    extTel dom :: Dom (a, Type)
    dom@Dom{unDom :: forall t e. Dom' t e -> e
    unDom = (a
    x, Type
    a)} = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Dom (a, Type)
    dom{unDom = a}) (Abs Telescope -> Telescope)
    -> (Telescope -> Abs Telescope) -> Telescope -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Telescope -> Abs Telescope
    forall a. [Char] -> a -> Abs a
    Abs (a -> [Char]
    f a
    x)

    -- | Convert a list telescope to a telescope.
    telFromList :: ListTel -> Telescope
    telFromList :: ListTel -> Telescope
    telFromList = ShowS -> ListTel -> Telescope
    forall a. (a -> [Char]) -> ListTel' a -> Telescope
    telFromList' ShowS
    forall a. a -> a
    id

    -- | Convert a telescope to its list form.
    telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
    telToList :: forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom t)
    EmptyTel                    = []
    telToList (ExtendTel Dom t
    arg (Abs [Char]
    x Tele (Dom t)
    tel)) = (t -> ([Char], t)) -> Dom t -> Dom ([Char], t)
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char]
    x,) Dom t
    arg Dom ([Char], t) -> [Dom ([Char], t)] -> [Dom ([Char], t)]
    forall a. a -> [a] -> [a]
    : Tele (Dom t) -> [Dom ([Char], t)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom t)
    tel
    telToList (ExtendTel Dom t
    _    NoAbs{}   ) = [Dom ([Char], t)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Lens to edit a 'Telescope' as a list.
    listTel :: Lens' Telescope ListTel
    listTel :: Lens' Telescope ListTel
    listTel ListTel -> f ListTel
    f = (ListTel -> Telescope) -> f ListTel -> f Telescope
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ListTel -> Telescope
    telFromList (f ListTel -> f Telescope)
    -> (Telescope -> f ListTel) -> Telescope -> f Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ListTel -> f ListTel
    f (ListTel -> f ListTel)
    -> (Telescope -> ListTel) -> Telescope -> f ListTel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList

    -- | Drop the types from a telescope.
    class TelToArgs a where
      telToArgs :: a -> [Arg ArgName]

    instance TelToArgs ListTel where
      telToArgs :: ListTel -> [Arg [Char]]
    telToArgs = (Dom ([Char], Type) -> Arg [Char]) -> ListTel -> [Arg [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Dom ([Char], Type) -> Arg [Char]) -> ListTel -> [Arg [Char]])
    -> (Dom ([Char], Type) -> Arg [Char]) -> ListTel -> [Arg [Char]]
    forall a b. (a -> b) -> a -> b
    $ \ Dom ([Char], Type)
    dom -> ArgInfo -> [Char] -> Arg [Char]
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom ([Char], Type) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom ([Char], Type)
    dom) (([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char]) -> ([Char], Type) -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom Dom ([Char], Type)
    dom)

    instance TelToArgs Telescope where
      telToArgs :: Telescope -> [Arg [Char]]
    telToArgs = ListTel -> [Arg [Char]]
    forall a. TelToArgs a => a -> [Arg [Char]]
    telToArgs (ListTel -> [Arg [Char]])
    -> (Telescope -> ListTel) -> Telescope -> [Arg [Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList

    -- | Constructing a singleton telescope.
    class SgTel a where
      sgTel :: a -> Telescope

    instance SgTel (ArgName, Dom Type) where
      sgTel :: ([Char], Dom Type) -> Telescope
    sgTel ([Char]
    x, !Dom Type
    dom) = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    dom (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Telescope -> Abs Telescope
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    x Telescope
    forall a. Tele a
    EmptyTel

    instance SgTel (Dom (ArgName, Type)) where
      sgTel :: Dom ([Char], Type) -> Telescope
    sgTel Dom ([Char], Type)
    dom = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd (([Char], Type) -> Type) -> Dom ([Char], Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom ([Char], Type)
    dom) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Telescope -> Abs Telescope
    forall a. [Char] -> a -> Abs a
    Abs (([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char]) -> ([Char], Type) -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom Dom ([Char], Type)
    dom) Telescope
    forall a. Tele a
    EmptyTel

    instance SgTel (Dom Type) where
      sgTel :: Dom Type -> Telescope
    sgTel Dom Type
    dom = ([Char], Dom Type) -> Telescope
    forall a. SgTel a => a -> Telescope
    sgTel (ShowS
    stringToArgName [Char]
    "_", Dom Type
    dom)

    ---------------------------------------------------------------------------
    -- * Simple operations on terms and types.
    ---------------------------------------------------------------------------

    -- | Removing a topmost 'DontCare' constructor.
    stripDontCare :: Term -> Term
    stripDontCare :: Term -> Term
    stripDontCare = \case
      DontCare Term
    v -> Term
    v
      Term
    v          -> Term
    v

    -- | Doesn't do any reduction.
    arity :: Type -> Nat
    arity :: Type -> Int
    arity Type
    t = case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
      Pi  Dom Type
    _ Abs Type
    b -> Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Type -> Int
    arity (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b)
      Term
    _       -> Int
    0

    -- | Suggest a name if available (i.e. name is not "_")
    class Suggest a where
      suggestName :: a -> Maybe String

    instance Suggest String where
      suggestName :: [Char] -> Maybe [Char]
    suggestName [Char]
    "_" = Maybe [Char]
    forall a. Maybe a
    Nothing
      suggestName  [Char]
    x  = [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    x

    instance Suggest (Abs b) where
      suggestName :: Abs b -> Maybe [Char]
    suggestName = [Char] -> Maybe [Char]
    forall a. Suggest a => a -> Maybe [Char]
    suggestName ([Char] -> Maybe [Char])
    -> (Abs b -> [Char]) -> Abs b -> Maybe [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs b -> [Char]
    forall a. Abs a -> [Char]
    absName

    instance Suggest Name where
      suggestName :: Name -> Maybe [Char]
    suggestName = [Char] -> Maybe [Char]
    forall a. Suggest a => a -> Maybe [Char]
    suggestName ([Char] -> Maybe [Char])
    -> (Name -> [Char]) -> Name -> Maybe [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Char]
    nameToArgName

    instance Suggest Term where
      suggestName :: Term -> Maybe [Char]
    suggestName (Lam ArgInfo
    _ Abs Term
    v) = Abs Term -> Maybe [Char]
    forall a. Suggest a => a -> Maybe [Char]
    suggestName Abs Term
    v
      suggestName Term
    _         = Maybe [Char]
    forall a. Maybe a
    Nothing

    -- Wrapping @forall a. (Suggest a) => a@ into a datatype because
    -- GHC doesn't support impredicative polymorphism
    data Suggestion = forall a. Suggest a => Suggestion a

    suggests :: [Suggestion] -> String
    suggests :: [Suggestion] -> [Char]
    suggests []     = [Char]
    "x"
    suggests (Suggestion a
    x : [Suggestion]
    xs) = [Char] -> Maybe [Char] -> [Char]
    forall a. a -> Maybe a -> a
    fromMaybe ([Suggestion] -> [Char]
    suggests [Suggestion]
    xs) (Maybe [Char] -> [Char]) -> Maybe [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe [Char]
    forall a. Suggest a => a -> Maybe [Char]
    suggestName a
    x

    ---------------------------------------------------------------------------
    -- * Eliminations.
    ---------------------------------------------------------------------------

    -- | Convert top-level postfix projections into prefix projections.
    unSpine :: Term -> Term
    unSpine :: Term -> Term
    unSpine = (ProjOrigin -> QName -> Bool) -> Term -> Term
    unSpine' ((ProjOrigin -> QName -> Bool) -> Term -> Term)
    -> (ProjOrigin -> QName -> Bool) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ \ProjOrigin
    _ QName
    _ -> Bool
    True

    -- | Convert 'Proj' projection eliminations
    --   according to their 'ProjOrigin' into
    --   'Def' projection applications.
    unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
    unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
    unSpine' ProjOrigin -> QName -> Bool
    p Term
    v =
      case Term -> Maybe (Elims -> Term, Elims)
    hasElims Term
    v of
        Just (Elims -> Term
    h, Elims
    es) -> (Elims -> Term) -> Elims -> Elims -> Term
    loop Elims -> Term
    h [] Elims
    es
        Maybe (Elims -> Term, Elims)
    Nothing      -> Term
    v
      where
        loop :: (Elims -> Term) -> Elims -> Elims -> Term
        loop :: (Elims -> Term) -> Elims -> Elims -> Term
    loop Elims -> Term
    h Elims
    res Elims
    es =
          case Elims
    es of
            []                     -> Term
    v
            Proj ProjOrigin
    o QName
    f : Elims
    es' | ProjOrigin -> QName -> Bool
    p ProjOrigin
    o QName
    f -> (Elims -> Term) -> Elims -> Elims -> Term
    loop (QName -> Elims -> Term
    Def QName
    f) [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    v)] Elims
    es'
            Elim' Term
    e        : Elims
    es'         -> (Elims -> Term) -> Elims -> Elims -> Term
    loop Elims -> Term
    h (Elim' Term
    e Elim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    res) Elims
    es'
          where v :: Term
    v = Elims -> Term
    h (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Elims
    forall a. [a] -> [a]
    reverse Elims
    res

    -- | A view distinguishing the neutrals @Var@, @Def@, and @MetaV@ which
    --   can be projected.
    hasElims :: Term -> Maybe (Elims -> Term, Elims)
    hasElims :: Term -> Maybe (Elims -> Term, Elims)
    hasElims Term
    v =
      case Term
    v of
        Var   Int
    i Elims
    es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
    forall a. a -> Maybe a
    Just (Int -> Elims -> Term
    Var   Int
    i, Elims
    es)
        Def   QName
    f Elims
    es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
    forall a. a -> Maybe a
    Just (QName -> Elims -> Term
    Def   QName
    f, Elims
    es)
        MetaV MetaId
    x Elims
    es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
    forall a. a -> Maybe a
    Just (MetaId -> Elims -> Term
    MetaV MetaId
    x, Elims
    es)
        Con{}      -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        Lit{}      -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        Lam{}      -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        Pi{}       -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        Sort{}     -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        Level{}    -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        DontCare{} -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing
        Dummy{}    -> Maybe (Elims -> Term, Elims)
    forall a. Maybe a
    Nothing

    ---------------------------------------------------------------------------
    -- * Type family for type-directed operations.
    ---------------------------------------------------------------------------

    -- @TypeOf a@ contains sufficient type information to do
    -- a type-directed traversal of @a@.
    type family TypeOf a

    type instance TypeOf Term        = Type                  -- Type of the term
    type instance TypeOf Elims       = (Type, Elims -> Term) -- Head symbol type + constructor
    type instance TypeOf (Abs Term)  = (Dom Type, Abs Type)  -- Domain type + codomain type
    type instance TypeOf (Abs Type)  = Dom Type              -- Domain type
    type instance TypeOf (Arg a)     = Dom (TypeOf a)
    type instance TypeOf (Dom a)     = TypeOf a
    type instance TypeOf Type        = ()
    type instance TypeOf Sort        = ()
    type instance TypeOf Level       = ()
    type instance TypeOf [PlusLevel] = ()
    type instance TypeOf PlusLevel   = ()

    ---------------------------------------------------------------------------
    -- * Null instances.
    ---------------------------------------------------------------------------

    instance Null (Tele a) where
      empty :: Tele a
    empty = Tele a
    forall a. Tele a
    EmptyTel
      null :: Tele a -> Bool
    null Tele a
    EmptyTel    = Bool
    True
      null ExtendTel{} = Bool
    False

    -- | A 'null' clause is one with no patterns and no rhs.
    --   Should not exist in practice.
    instance Null Clause where
      empty :: Clause
    empty = Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    Clause Range
    forall a. Null a => a
    empty Range
    forall a. Null a => a
    empty Telescope
    forall a. Null a => a
    empty NAPs
    forall a. Null a => a
    empty Maybe Term
    forall a. Null a => a
    empty Maybe (Arg Type)
    forall a. Null a => a
    empty Catchall
    forall a. Null a => a
    empty Maybe Bool
    forall a. Null a => a
    empty Maybe Bool
    forall a. Null a => a
    empty ExpandedEllipsis
    forall a. Null a => a
    empty Maybe ModuleName
    forall a. Null a => a
    empty
      null :: Clause -> Bool
    null (Clause Range
    _ Range
    _ Telescope
    tel NAPs
    pats Maybe Term
    body Maybe (Arg Type)
    _ Catchall
    _ Maybe Bool
    _ Maybe Bool
    _ ExpandedEllipsis
    _ Maybe ModuleName
    wm)
        =  Telescope -> Bool
    forall a. Null a => a -> Bool
    null Telescope
    tel
        Bool -> Bool -> Bool
    && NAPs -> Bool
    forall a. Null a => a -> Bool
    null NAPs
    pats
        Bool -> Bool -> Bool
    && Maybe Term -> Bool
    forall a. Null a => a -> Bool
    null Maybe Term
    body
        Bool -> Bool -> Bool
    && Maybe ModuleName -> Bool
    forall a. Null a => a -> Bool
    null Maybe ModuleName
    wm

    ---------------------------------------------------------------------------
    -- * Show instances.
    ---------------------------------------------------------------------------

    instance Show a => Show (Abs a) where
      showsPrec :: Int -> Abs a -> ShowS
    showsPrec Int
    p (Abs [Char]
    x a
    a) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> ShowS
    showString [Char]
    "Abs " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> ShowS
    forall a. Show a => a -> ShowS
    shows [Char]
    x ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> ShowS
    showString [Char]
    " " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    10 a
    a
      showsPrec Int
    p (NoAbs [Char]
    x a
    a) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> ShowS
    showString [Char]
    "NoAbs " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> ShowS
    forall a. Show a => a -> ShowS
    shows [Char]
    x ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> ShowS
    showString [Char]
    " " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    10 a
    a

    -- instance Show t => Show (Blocked t) where
    --   showsPrec p (Blocked m x) = showParen (p > 0) $
    --     showString "Blocked " . shows m . showString " " . showsPrec 10 x
    --   showsPrec p (NotBlocked x) = showsPrec p x

    ---------------------------------------------------------------------------
    -- * Sized instances and TermSize.
    ---------------------------------------------------------------------------

    -- | The size of a telescope is its length (as a list).
    instance Sized (Tele a) where
      size :: Tele a -> Int
    size  Tele a
    EmptyTel         = Int
    0
      size (ExtendTel a
    _ Abs (Tele a)
    tel) = Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Abs (Tele a) -> Int
    forall a. Sized a => a -> Int
    size Abs (Tele a)
    tel

      natSize :: Tele a -> Peano
    natSize Tele a
    EmptyTel          = Peano
    Zero
      natSize (ExtendTel a
    _ Abs (Tele a)
    tel) = Peano -> Peano
    Succ (Peano -> Peano) -> Peano -> Peano
    forall a b. (a -> b) -> a -> b
    $ Abs (Tele a) -> Peano
    forall a. Sized a => a -> Peano
    natSize Abs (Tele a)
    tel

    instance Sized a => Sized (Abs a) where
      size :: Abs a -> Int
    size    = a -> Int
    forall a. Sized a => a -> Int
    size    (a -> Int) -> (Abs a -> a) -> Abs a -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs a -> a
    forall a. Abs a -> a
    unAbs
      natSize :: Abs a -> Peano
    natSize = a -> Peano
    forall a. Sized a => a -> Peano
    natSize (a -> Peano) -> (Abs a -> a) -> Abs a -> Peano
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs a -> a
    forall a. Abs a -> a
    unAbs

    -- | The size of a term is roughly the number of nodes in its
    --   syntax tree.  This number need not be precise for logical
    --   correctness of Agda, it is only used for reporting
    --   (and maybe decisions regarding performance).
    --
    --   Not counting towards the term size are:
    --
    --     * sort and color annotations,
    --     * projections.
    --
    class TermSize a where
      termSize :: a -> Int
      termSize = Sum Int -> Int
    forall a. Sum a -> a
    getSum (Sum Int -> Int) -> (a -> Sum Int) -> a -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize

      tsize :: a -> Sum Int

    instance {-# OVERLAPPABLE #-} (Foldable t, TermSize a) => TermSize (t a) where
      tsize :: t a -> Sum Int
    tsize = (a -> Sum Int) -> t a -> Sum Int
    forall m a. Monoid m => (a -> m) -> t a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize

    instance TermSize Term where
      tsize :: Term -> Sum Int
    tsize = \case
        Var Int
    _ Elims
    vs    -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Elims -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Elims
    vs
        Def QName
    _ Elims
    vs    -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Elims -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Elims
    vs
        Con ConHead
    _ ConInfo
    _ Elims
    vs    -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Elims -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Elims
    vs
        MetaV MetaId
    _ Elims
    vs  -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Elims -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Elims
    vs
        Level Level
    l     -> Level -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Level
    l
        Lam ArgInfo
    _ Abs Term
    f     -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Abs Term -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Abs Term
    f
        Lit Literal
    _       -> Sum Int
    1
        Pi Dom Type
    a Abs Type
    b      -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Dom Type -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Dom Type
    a Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Abs Type -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Abs Type
    b
        Sort Sort
    s      -> Sort -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Sort
    s
        DontCare Term
    mv -> Term -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Term
    mv
        Dummy{}     -> Sum Int
    1

    instance TermSize Sort where
      tsize :: Sort -> Sum Int
    tsize = \case
        Univ Univ
    _ Level
    l  -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Level -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Level
    l
        Inf Univ
    _ Integer
    _   -> Sum Int
    1
        Sort
    SizeUniv  -> Sum Int
    1
        Sort
    LockUniv  -> Sum Int
    1
        Sort
    LevelUniv -> Sum Int
    1
        Sort
    IntervalUniv -> Sum Int
    1
        PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Dom' Term Term -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Dom' Term Term
    a Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Sort -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Sort
    s1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Abs Sort -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Abs Sort
    s2
        FunSort Sort
    s1 Sort
    s2 -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Sort -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Sort
    s1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Sort -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Sort
    s2
        UnivSort Sort
    s -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Sort -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Sort
    s
        MetaS MetaId
    _ Elims
    es -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Elims -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Elims
    es
        DefS QName
    _ Elims
    es  -> Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Elims -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Elims
    es
        DummyS{}   -> Sum Int
    1

    instance TermSize Level where
      tsize :: Level -> Sum Int
    tsize (Max Integer
    _ [PlusLevel' Term]
    as) = Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + [PlusLevel' Term] -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize [PlusLevel' Term]
    as

    instance TermSize PlusLevel where
      tsize :: PlusLevel' Term -> Sum Int
    tsize (Plus Integer
    _ Term
    a)      = Term -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Term
    a

    instance TermSize a => TermSize (Substitution' a) where
      tsize :: Substitution' a -> Sum Int
    tsize Substitution' a
    IdS                  = Sum Int
    1
      tsize (EmptyS Impossible
    _)           = Sum Int
    1
      tsize (Wk Int
    _ Substitution' a
    rho)           = Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Substitution' a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Substitution' a
    rho
      tsize (a
    t :# Substitution' a
    rho)           = Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize a
    t Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Substitution' a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Substitution' a
    rho
      tsize (Strengthen Impossible
    _ Int
    _ Substitution' a
    rho) = Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Substitution' a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Substitution' a
    rho
      tsize (Lift Int
    _ Substitution' a
    rho)         = Sum Int
    1 Sum Int -> Sum Int -> Sum Int
    forall a. Num a => a -> a -> a
    + Substitution' a -> Sum Int
    forall a. TermSize a => a -> Sum Int
    tsize Substitution' a
    rho

    ---------------------------------------------------------------------------
    -- * KillRange instances.
    ---------------------------------------------------------------------------

    instance KillRange DataOrRecord where
      killRange :: KillRangeT DataOrRecord
    killRange = KillRangeT DataOrRecord
    forall a. a -> a
    id

    instance KillRange ConHead where
      killRange :: ConHead -> ConHead
    killRange (ConHead QName
    c DataOrRecord
    d Induction
    i [Arg QName]
    fs) = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
    -> QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    c DataOrRecord
    d Induction
    i [Arg QName]
    fs

    instance KillRange Term where
      killRange :: Term -> Term
    killRange = \case
        Var Int
    i Elims
    vs    -> (Elims -> Term) -> Elims -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Int -> Elims -> Term
    Var Int
    i) Elims
    vs
        Def QName
    c Elims
    vs    -> (QName -> Elims -> Term) -> QName -> Elims -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> Elims -> Term
    Def QName
    c Elims
    vs
        Con ConHead
    c ConInfo
    ci Elims
    vs -> (ConHead -> ConInfo -> Elims -> Term)
    -> ConHead -> ConInfo -> Elims -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci Elims
    vs
        MetaV MetaId
    m Elims
    vs  -> (Elims -> Term) -> Elims -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (MetaId -> Elims -> Term
    MetaV MetaId
    m) Elims
    vs
        Lam ArgInfo
    i Abs Term
    f     -> (ArgInfo -> Abs Term -> Term) -> ArgInfo -> Abs Term -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i Abs Term
    f
        Lit Literal
    l       -> (Literal -> Term) -> Literal -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Literal -> Term
    Lit Literal
    l
        Level Level
    l     -> (Level -> Term) -> Level -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Level -> Term
    Level Level
    l
        Pi Dom Type
    a Abs Type
    b      -> (Dom Type -> Abs Type -> Term) -> Dom Type -> Abs Type -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Dom Type -> Abs Type -> Term
    Pi Dom Type
    a Abs Type
    b
        Sort Sort
    s      -> (Sort -> Term) -> Sort -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Sort -> Term
    Sort Sort
    s
        DontCare Term
    mv -> (Term -> Term) -> Term -> Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Term -> Term
    DontCare Term
    mv
        v :: Term
    v@Dummy{}   -> Term
    v

    instance KillRange Level where
      killRange :: Level -> Level
    killRange (Max Integer
    n [PlusLevel' Term]
    as) = ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n) [PlusLevel' Term]
    as

    instance KillRange PlusLevel where
      killRange :: PlusLevel' Term -> PlusLevel' Term
    killRange (Plus Integer
    n Term
    l) = (Term -> PlusLevel' Term) -> Term -> PlusLevel' Term
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n) Term
    l

    instance (KillRange a) => KillRange (Type' a) where
      killRange :: KillRangeT (Type' a)
    killRange (El Sort
    s a
    v) = (Sort -> a -> Type' a) -> Sort -> a -> Type' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Sort -> a -> Type' a
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s a
    v

    instance KillRange Sort where
      killRange :: Sort -> Sort
    killRange = \case
        Inf Univ
    u Integer
    n    -> Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    u Integer
    n
        Sort
    SizeUniv   -> Sort
    forall t. Sort' t
    SizeUniv
        Sort
    LockUniv   -> Sort
    forall t. Sort' t
    LockUniv
        Sort
    LevelUniv  -> Sort
    forall t. Sort' t
    LevelUniv
        Sort
    IntervalUniv -> Sort
    forall t. Sort' t
    IntervalUniv
        Univ Univ
    u Level
    a   -> (Level -> Sort) -> Level -> Sort
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u) Level
    a
        PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> (Dom' Term Term -> Sort -> Abs Sort -> Sort)
    -> Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2
        FunSort Sort
    s1 Sort
    s2 -> (Sort -> Sort -> Sort) -> Sort -> Sort -> Sort
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    s1 Sort
    s2
        UnivSort Sort
    s -> (Sort -> Sort) -> Sort -> Sort
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort Sort
    s
        MetaS MetaId
    x Elims
    es -> (Elims -> Sort) -> Elims -> Sort
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x) Elims
    es
        DefS QName
    d Elims
    es  -> (QName -> Elims -> Sort) -> QName -> Elims -> Sort
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d Elims
    es
        s :: Sort
    s@DummyS{} -> Sort
    s

    instance KillRange Substitution where
      killRange :: KillRangeT Substitution
    killRange Substitution
    IdS                    = Substitution
    forall a. Substitution' a
    IdS
      killRange (EmptyS Impossible
    err)           = Impossible -> Substitution
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    err
      killRange (Wk Int
    n Substitution
    rho)             = KillRangeT Substitution -> KillRangeT Substitution
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Int -> KillRangeT Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    Wk Int
    n) Substitution
    rho
      killRange (Term
    t :# Substitution
    rho)             = (Term -> KillRangeT Substitution)
    -> Term -> KillRangeT Substitution
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Term -> KillRangeT Substitution
    forall a. a -> Substitution' a -> Substitution' a
    (:#) Term
    t Substitution
    rho
      killRange (Strengthen Impossible
    err Int
    n Substitution
    rho) = KillRangeT Substitution -> KillRangeT Substitution
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Impossible -> Int -> KillRangeT Substitution
    forall a. Impossible -> Int -> Substitution' a -> Substitution' a
    Strengthen Impossible
    err Int
    n) Substitution
    rho
      killRange (Lift Int
    n Substitution
    rho)           = KillRangeT Substitution -> KillRangeT Substitution
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Int -> KillRangeT Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    Lift Int
    n) Substitution
    rho

    instance KillRange PatOrigin where
      killRange :: KillRangeT PatOrigin
    killRange = KillRangeT PatOrigin
    forall a. a -> a
    id

    instance KillRange PatternInfo where
      killRange :: KillRangeT PatternInfo
    killRange (PatternInfo PatOrigin
    o [Name]
    xs) = (PatOrigin -> [Name] -> PatternInfo)
    -> PatOrigin -> [Name] -> PatternInfo
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    o [Name]
    xs

    instance KillRange ConPatternInfo where
      killRange :: KillRangeT ConPatternInfo
    killRange (ConPatternInfo PatternInfo
    i Bool
    mr Bool
    b Maybe (Arg Type)
    mt Bool
    lz) = (Maybe (Arg Type) -> Bool -> ConPatternInfo)
    -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo PatternInfo
    i Bool
    mr Bool
    b) Maybe (Arg Type)
    mt Bool
    lz

    instance KillRange DBPatVar where
      killRange :: KillRangeT DBPatVar
    killRange (DBPatVar [Char]
    x Int
    i) = ([Char] -> Int -> DBPatVar) -> [Char] -> Int -> DBPatVar
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [Char] -> Int -> DBPatVar
    DBPatVar [Char]
    x Int
    i

    instance KillRange a => KillRange (Pattern' a) where
      killRange :: KillRangeT (Pattern' a)
    killRange Pattern' a
    p =
        case Pattern' a
    p of
          VarP PatternInfo
    o a
    x         -> (PatternInfo -> a -> Pattern' a) -> PatternInfo -> a -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatternInfo -> a -> Pattern' a
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    o a
    x
          DotP PatternInfo
    o Term
    v         -> (PatternInfo -> Term -> Pattern' a)
    -> PatternInfo -> Term -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatternInfo -> Term -> Pattern' a
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    o Term
    v
          ConP ConHead
    con ConPatternInfo
    info [NamedArg (Pattern' a)]
    ps -> (ConHead
     -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
    -> ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' a)]
    -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    con ConPatternInfo
    info [NamedArg (Pattern' a)]
    ps
          LitP PatternInfo
    o Literal
    l         -> (PatternInfo -> Literal -> Pattern' a)
    -> PatternInfo -> Literal -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatternInfo -> Literal -> Pattern' a
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP PatternInfo
    o Literal
    l
          ProjP ProjOrigin
    o QName
    q        -> (QName -> Pattern' a) -> QName -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (ProjOrigin -> QName -> Pattern' a
    forall x. ProjOrigin -> QName -> Pattern' x
    ProjP ProjOrigin
    o) QName
    q
          IApplyP PatternInfo
    o Term
    u Term
    t a
    x  -> (Term -> Term -> a -> Pattern' a)
    -> Term -> Term -> a -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (PatternInfo -> Term -> Term -> a -> Pattern' a
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    o) Term
    u Term
    t a
    x
          DefP PatternInfo
    o QName
    q [NamedArg (Pattern' a)]
    ps      -> (QName -> [NamedArg (Pattern' a)] -> Pattern' a)
    -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    o) QName
    q [NamedArg (Pattern' a)]
    ps

    instance KillRange Clause where
      killRange :: KillRangeT Clause
    killRange (Clause Range
    rl Range
    rf Telescope
    tel NAPs
    ps Maybe Term
    body Maybe (Arg Type)
    t Catchall
    catchall Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell Maybe ModuleName
    wm) =
        (Range
     -> Range
     -> Telescope
     -> NAPs
     -> Maybe Term
     -> Maybe (Arg Type)
     -> Catchall
     -> Maybe Bool
     -> Maybe Bool
     -> ExpandedEllipsis
     -> Maybe ModuleName
     -> Clause)
    -> Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    Clause Range
    rl Range
    rf Telescope
    tel NAPs
    ps Maybe Term
    body Maybe (Arg Type)
    t Catchall
    catchall Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell Maybe ModuleName
    wm

    instance KillRange a => KillRange (Tele a) where
      killRange :: KillRangeT (Tele a)
    killRange = (a -> a) -> KillRangeT (Tele a)
    forall a b. (a -> b) -> Tele a -> Tele b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    forall a. KillRange a => KillRangeT a
    killRange

    instance KillRange a => KillRange (Blocked a) where
      killRange :: KillRangeT (Blocked a)
    killRange = (a -> a) -> KillRangeT (Blocked a)
    forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    forall a. KillRange a => KillRangeT a
    killRange

    instance KillRange a => KillRange (Abs a) where
      killRange :: KillRangeT (Abs a)
    killRange = (a -> a) -> KillRangeT (Abs a)
    forall a b. (a -> b) -> Abs a -> Abs b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    forall a. KillRange a => KillRangeT a
    killRange

    -----------------------------------------------------------------------------
    -- * Simple pretty printing
    -----------------------------------------------------------------------------

    instance Pretty a => Pretty (Substitution' a) where
      prettyPrec :: Int -> Substitution' a -> Doc Aspects
    prettyPrec = Int -> Substitution' a -> Doc Aspects
    forall {t} {a}.
    (Ord t, Num t, Pretty a) =>
    t -> Substitution' a -> Doc Aspects
    pr
        where
        pr :: t -> Substitution' a -> Doc Aspects
    pr t
    p Substitution' a
    rho = case Substitution' a
    rho of
          Substitution' a
    IdS                -> Doc Aspects
    "idS"
          EmptyS Impossible
    err         -> Doc Aspects
    "emptyS"
          a
    t :# Substitution' a
    rho           -> Bool -> Doc Aspects -> Doc Aspects
    mparens (t
    p t -> t -> Bool
    forall a. Ord a => a -> a -> Bool
    > t
    2) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                                [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ t -> Substitution' a -> Doc Aspects
    pr t
    2 Substitution' a
    rho Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects
    ",", Int -> a -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    3 a
    t ]
          Strengthen Impossible
    _ Int
    n Substitution' a
    rho -> Bool -> Doc Aspects -> Doc Aspects
    mparens (t
    p t -> t -> Bool
    forall a. Ord a => a -> a -> Bool
    > t
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                                [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char]
    "strS " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> t -> Substitution' a -> Doc Aspects
    pr t
    10 Substitution' a
    rho
          Wk Int
    n Substitution' a
    rho           -> Bool -> Doc Aspects -> Doc Aspects
    mparens (t
    p t -> t -> Bool
    forall a. Ord a => a -> a -> Bool
    > t
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                                [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char]
    "wkS " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> t -> Substitution' a -> Doc Aspects
    pr t
    10 Substitution' a
    rho
          Lift Int
    n Substitution' a
    rho         -> Bool -> Doc Aspects -> Doc Aspects
    mparens (t
    p t -> t -> Bool
    forall a. Ord a => a -> a -> Bool
    > t
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                                [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char]
    "liftS " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> t -> Substitution' a -> Doc Aspects
    pr t
    10 Substitution' a
    rho

    instance Pretty Term where
      prettyPrec :: Int -> Term -> Doc Aspects
    prettyPrec Int
    p Term
    v =
        case Term
    v of
          Var Int
    x Elims
    els -> [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char]
    "@" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    x) Doc Aspects -> Elims -> Doc Aspects
    `pApp` Elims
    els
          Lam ArgInfo
    ai Abs Term
    b   ->
            Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
            [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "λ" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> ArgInfo
    -> (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a.
    LensHiding a =>
    a -> (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    prettyHiding ArgInfo
    ai Doc Aspects -> Doc Aspects
    forall a. a -> a
    id ([Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects)
    -> (Abs Term -> [Char]) -> Abs Term -> Doc Aspects
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs Term -> [Char]
    forall a. Abs a -> [Char]
    absName (Abs Term -> Doc Aspects) -> Abs Term -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Abs Term
    b) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "->"
                , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Term -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b) ]
          Lit Literal
    l                -> Literal -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Literal
    l
          Def QName
    q Elims
    els            -> QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty QName
    q Doc Aspects -> Elims -> Doc Aspects
    `pApp` Elims
    els
          Con ConHead
    c ConInfo
    ci Elims
    vs          -> QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (ConHead -> QName
    conName ConHead
    c) Doc Aspects -> Elims -> Doc Aspects
    `pApp` Elims
    vs
          Pi Dom Type
    a (NoAbs [Char]
    _ Type
    b)     -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
            [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Modality -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom Type
    a) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Type -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    1 (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "->"
                , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Type -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Type
    b ]
          Pi Dom Type
    a Abs Type
    b               -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
            [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ ArgInfo -> Doc Aspects -> Doc Aspects
    forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
    pDom (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a) (Modality -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom Type
    a) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text (Abs Type -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Type
    b) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ":" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Type -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "->"
                , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Type -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b) ]
          Sort Sort
    s      -> Int -> Sort -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p Sort
    s
          Level Level
    l     -> Int -> Level -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p Level
    l
          MetaV MetaId
    x Elims
    els -> MetaId -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty MetaId
    x Doc Aspects -> Elims -> Doc Aspects
    `pApp` Elims
    els
          DontCare Term
    v  -> Int -> Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p Term
    v
          Dummy [Char]
    s Elims
    es  -> Doc Aspects -> Doc Aspects
    parens ([Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text [Char]
    s) Doc Aspects -> Elims -> Doc Aspects
    `pApp` Elims
    es
        where
          pApp :: Doc Aspects -> Elims -> Doc Aspects
    pApp Doc Aspects
    d Elims
    els = Bool -> Doc Aspects -> Doc Aspects
    mparens (Bool -> Bool
    not (Elims -> Bool
    forall a. Null a => a -> Bool
    null Elims
    els) Bool -> Bool -> Bool
    && Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                       [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [Doc Aspects
    d, Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep ((Elim' Term -> Doc Aspects) -> Elims -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Elim' Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10) Elims
    els)]

    instance Pretty t => Pretty (Abs t) where
      pretty :: Abs t -> Doc Aspects
    pretty (Abs   [Char]
    x t
    t) = Doc Aspects
    "Abs"   Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> ([Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text [Char]
    x Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects
    ".") Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> t -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty t
    t
      pretty (NoAbs [Char]
    x t
    t) = Doc Aspects
    "NoAbs" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> ([Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text [Char]
    x Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects
    ".") Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> t -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty t
    t

    instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
      pretty :: Dom' t e -> Doc Aspects
    pretty Dom' t e
    dom = Doc Aspects
    pLock Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    pTac Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Dom' t e -> Doc Aspects -> Doc Aspects
    forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
    pDom Dom' t e
    dom (Modality -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom' t e -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom' t e
    dom) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> e -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom' t e -> e
    forall t e. Dom' t e -> e
    unDom Dom' t e
    dom))
        where
          pTac :: Doc Aspects
    pTac | Just t
    t <- Dom' t e -> Maybe t
    forall t e. Dom' t e -> Maybe t
    domTactic Dom' t e
    dom = Doc Aspects
    "@" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects -> Doc Aspects
    parens (Doc Aspects
    "tactic" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> t -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty t
    t)
               | Bool
    otherwise               = Doc Aspects
    forall a. Null a => a
    empty
          pLock :: Doc Aspects
    pLock | IsLock{} <- Dom' t e -> Lock
    forall a. LensLock a => a -> Lock
    getLock Dom' t e
    dom = Doc Aspects
    "@lock"
                | Bool
    otherwise = Doc Aspects
    forall a. Null a => a
    empty

    pDom :: LensHiding a => a -> Doc -> Doc
    pDom :: forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
    pDom a
    i =
      case a -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding a
    i of
        Hiding
    NotHidden  -> Doc Aspects -> Doc Aspects
    parens
        Hiding
    Hidden     -> Doc Aspects -> Doc Aspects
    braces
        Instance{} -> Doc Aspects -> Doc Aspects
    braces (Doc Aspects -> Doc Aspects)
    -> (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc Aspects -> Doc Aspects
    braces

    instance Pretty Clause where
      pretty :: Clause -> Doc Aspects
    pretty Clause{clauseTel :: Clause -> Telescope
    clauseTel = Telescope
    tel, namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps, clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    b, clauseType :: Clause -> Maybe (Arg Type)
    clauseType = Maybe (Arg Type)
    t} =
        [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    tel Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "|-"
            , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep ((Arg (Named_ DeBruijnPattern) -> Doc Aspects)
    -> NAPs -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Arg (Named_ DeBruijnPattern) -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10) NAPs
    ps) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "="
                           , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Maybe Term -> Maybe (Arg Type) -> Doc Aspects
    forall {a} {a}.
    (Pretty a, Pretty a) =>
    Maybe a -> Maybe a -> Doc Aspects
    pBody Maybe Term
    b Maybe (Arg Type)
    t ] ]
        where
          pBody :: Maybe a -> Maybe a -> Doc Aspects
    pBody Maybe a
    Nothing Maybe a
    _ = Doc Aspects
    "(absurd)"
          pBody (Just a
    b) Maybe a
    Nothing  = a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    b
          pBody (Just a
    b) (Just a
    t) = [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    b Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ":", Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    t ]

    instance Pretty a => Pretty (Tele (Dom a)) where
      pretty :: Tele (Dom a) -> Doc Aspects
    pretty Tele (Dom a)
    tel = [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep [ Dom a -> Doc Aspects -> Doc Aspects
    forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
    pDom Dom a
    a ([Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text [Char]
    x Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ":" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom a -> a
    forall t e. Dom' t e -> e
    unDom Dom a
    a)) | ([Char]
    x, Dom a
    a) <- Tele (Dom a) -> [([Char], Dom a)]
    forall {b}. Tele b -> [([Char], b)]
    telToList Tele (Dom a)
    tel ]
        where
          telToList :: Tele b -> [([Char], b)]
    telToList Tele b
    EmptyTel = []
          telToList (ExtendTel b
    a Abs (Tele b)
    tel) = (Abs (Tele b) -> [Char]
    forall a. Abs a -> [Char]
    absName Abs (Tele b)
    tel, b
    a) ([Char], b) -> [([Char], b)] -> [([Char], b)]
    forall a. a -> [a] -> [a]
    : Tele b -> [([Char], b)]
    telToList (Abs (Tele b) -> Tele b
    forall a. Abs a -> a
    unAbs Abs (Tele b)
    tel)

    prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
    prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc Aspects) -> Doc Aspects
    prettyPrecLevelSucs Int
    p Integer
    0 Int -> Doc Aspects
    d = Int -> Doc Aspects
    d Int
    p
    prettyPrecLevelSucs Int
    p Integer
    n Int -> Doc Aspects
    d = Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "lsuc" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Integer -> (Int -> Doc Aspects) -> Doc Aspects
    prettyPrecLevelSucs Int
    10 (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Int -> Doc Aspects
    d

    instance Pretty Level where
      prettyPrec :: Int -> Level -> Doc Aspects
    prettyPrec Int
    p (Max Integer
    n [PlusLevel' Term]
    as) =
        case [PlusLevel' Term]
    as of
          []  -> Doc Aspects
    prettyN
          [PlusLevel' Term
    a] | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 -> Int -> PlusLevel' Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p PlusLevel' Term
    a
          [PlusLevel' Term]
    _   -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ (Doc Aspects -> Doc Aspects -> Doc Aspects)
    -> [Doc Aspects] -> Doc Aspects
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    List.foldr1 (\Doc Aspects
    a Doc Aspects
    b -> Doc Aspects
    "lub" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    a Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    b) ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
            [ Doc Aspects
    prettyN | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 ] [Doc Aspects] -> [Doc Aspects] -> [Doc Aspects]
    forall a. [a] -> [a] -> [a]
    ++ (PlusLevel' Term -> Doc Aspects)
    -> [PlusLevel' Term] -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> PlusLevel' Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10) [PlusLevel' Term]
    as
        where
          prettyN :: Doc Aspects
    prettyN = Int -> Integer -> (Int -> Doc Aspects) -> Doc Aspects
    prettyPrecLevelSucs Int
    p Integer
    n (Doc Aspects -> Int -> Doc Aspects
    forall a b. a -> b -> a
    const Doc Aspects
    "lzero")

    instance Pretty PlusLevel where
      prettyPrec :: Int -> PlusLevel' Term -> Doc Aspects
    prettyPrec Int
    p (Plus Integer
    n Term
    a) = Int -> Integer -> (Int -> Doc Aspects) -> Doc Aspects
    prettyPrecLevelSucs Int
    p Integer
    n ((Int -> Doc Aspects) -> Doc Aspects)
    -> (Int -> Doc Aspects) -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ \Int
    p -> Int -> Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p Term
    a

    instance Pretty Sort where
      prettyPrec :: Int -> Sort -> Doc Aspects
    prettyPrec Int
    p Sort
    s =
        case Sort
    s of
          Univ Univ
    u (ClosedLevel Integer
    n) -> [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Integer -> ShowS
    forall {a}. (Eq a, Num a, Show a) => a -> ShowS
    suffix Integer
    n ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Univ -> [Char]
    showUniv Univ
    u
          Univ Univ
    u Level
    l -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text (Univ -> [Char]
    showUniv Univ
    u) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Level -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10 Level
    l
          Inf Univ
    u Integer
    n -> [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Integer -> ShowS
    forall {a}. (Eq a, Num a, Show a) => a -> ShowS
    suffix Integer
    n ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Univ -> [Char]
    showUniv Univ
    u [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "ω"
          Sort
    SizeUniv -> Doc Aspects
    "SizeUniv"
          Sort
    LockUniv -> Doc Aspects
    "LockUniv"
          Sort
    LevelUniv -> Doc Aspects
    "LevelUniv"
          Sort
    IntervalUniv -> Doc Aspects
    "IntervalUniv"
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
            Doc Aspects
    "piSort" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> ArgInfo -> Doc Aspects -> Doc Aspects
    forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
    pDom (Dom' Term Term -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom' Term Term
    a) ([Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text (Abs Sort -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Sort
    s2) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ":" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Term -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Dom' Term Term -> Term
    forall t e. Dom' t e -> e
    unDom Dom' Term Term
    a) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ":" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Sort -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Sort
    s1)
                          Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects -> Doc Aspects
    parens (Sort -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (Abs Sort -> Sort
    forall a. Abs a -> a
    unAbs Abs Sort
    s2))
          FunSort Sort
    a Sort
    b -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
            Doc Aspects
    "funSort" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Sort -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10 Sort
    a Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Sort -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10 Sort
    b
          UnivSort Sort
    s -> Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "univSort" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Sort -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10 Sort
    s
          MetaS MetaId
    x Elims
    es -> Int -> Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p (Term -> Doc Aspects) -> Term -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    es
          DefS QName
    d Elims
    es  -> Int -> Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p (Term -> Doc Aspects) -> Term -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    d Elims
    es
          DummyS [Char]
    s   -> Doc Aspects -> Doc Aspects
    parens (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text [Char]
    s
       where
         suffix :: a -> ShowS
    suffix a
    n = Bool -> ShowS -> ShowS
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (a
    n a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    0) ([Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    n)

    instance Pretty Type where
      prettyPrec :: Int -> Type -> Doc Aspects
    prettyPrec Int
    p (El Sort
    _ Term
    a) = Int -> Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    p Term
    a

    instance Pretty DBPatVar where
      prettyPrec :: Int -> DBPatVar -> Doc Aspects
    prettyPrec Int
    _ DBPatVar
    x = [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ ShowS
    patVarNameToString (DBPatVar -> [Char]
    dbPatVarName DBPatVar
    x) [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "@" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x)

    instance Pretty a => Pretty (Pattern' a) where
      prettyPrec :: Int -> Pattern' a -> Doc Aspects
    prettyPrec Int
    n (VarP PatternInfo
    _o a
    x)   = Int -> a -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    n a
    x
      prettyPrec Int
    _ (DotP PatternInfo
    _o Term
    t)   = Doc Aspects
    "." Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Int -> Term -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10 Term
    t
      prettyPrec Int
    n (ConP ConHead
    c ConPatternInfo
    i [NamedArg (Pattern' a)]
    nps)= Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 Bool -> Bool -> Bool
    && Bool -> Bool
    not ([NamedArg (Pattern' a)] -> Bool
    forall a. Null a => a -> Bool
    null [NamedArg (Pattern' a)]
    nps)) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
        (Doc Aspects
    lazy Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty (ConHead -> QName
    conName ConHead
    c)) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep ((Arg (Pattern' a) -> Doc Aspects)
    -> [Arg (Pattern' a)] -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Arg (Pattern' a) -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10) [Arg (Pattern' a)]
    ps)
        where ps :: [Arg (Pattern' a)]
    ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
    -> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a) -> Arg (Pattern' a)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName (Pattern' a) -> Pattern' a
    forall name a. Named name a -> a
    namedThing) [NamedArg (Pattern' a)]
    nps
              lazy :: Doc Aspects
    lazy | ConPatternInfo -> Bool
    conPLazy ConPatternInfo
    i = Doc Aspects
    "~"
                   | Bool
    otherwise  = Doc Aspects
    forall a. Null a => a
    empty
      prettyPrec Int
    n (DefP PatternInfo
    o QName
    q [NamedArg (Pattern' a)]
    nps)= Bool -> Doc Aspects -> Doc Aspects
    mparens (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 Bool -> Bool -> Bool
    && Bool -> Bool
    not ([NamedArg (Pattern' a)] -> Bool
    forall a. Null a => a -> Bool
    null [NamedArg (Pattern' a)]
    nps)) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
        QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty QName
    q Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep ((Arg (Pattern' a) -> Doc Aspects)
    -> [Arg (Pattern' a)] -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Arg (Pattern' a) -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    10) [Arg (Pattern' a)]
    ps)
        where ps :: [Arg (Pattern' a)]
    ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
    -> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a) -> Arg (Pattern' a)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName (Pattern' a) -> Pattern' a
    forall name a. Named name a -> a
    namedThing) [NamedArg (Pattern' a)]
    nps
      -- -- Version with printing record type:
      -- prettyPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
      --   text (show $ conName c) <+> fsep (map (pretty . namedArg) ps)
      --   where
      --     b = maybe False (== ConOSystem) $ conPRecord i
      --     prTy d = caseMaybe (conPType i) d $ \ t -> d  <+> ":" <+> pretty t
      prettyPrec Int
    _ (LitP PatternInfo
    _ Literal
    l)    = Literal -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Literal
    l
      prettyPrec Int
    _ (ProjP ProjOrigin
    _o QName
    q)  = [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char]
    "." [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q)
      prettyPrec Int
    n (IApplyP PatternInfo
    _o Term
    _ Term
    _ a
    x) = Int -> a -> Doc Aspects
    forall a. Pretty a => Int -> a -> Doc Aspects
    prettyPrec Int
    n a
    x
    --  prettyPrec n (IApplyP _o u0 u1 x) = text "@[" <> prettyPrec 0 u0 <> text ", " <> prettyPrec 0 u1 <> text "]" <> prettyPrec n x

    instance Pretty a => Pretty (Blocked a) where
      pretty :: Blocked a -> Doc Aspects
    pretty = \case
        NotBlocked NotBlocked' Term
    ReallyNotBlocked a
    a -> a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    a
        NotBlocked NotBlocked' Term
    nb a
    a -> a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    a Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> (Doc Aspects
    "[ blocked on" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> NotBlocked' Term -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty NotBlocked' Term
    nb Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "]")
        Blocked     Blocker
    b a
    a -> a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    a Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> (Doc Aspects
    "[ stuck on" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Blocker -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty  Blocker
    b Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "]")

    -----------------------------------------------------------------------------
    -- * NFData instances
    -----------------------------------------------------------------------------

    -- Note: only strict in the shape of the terms.

    instance NFData Term where
      rnf :: Term -> ()
    rnf = \case
        Var Int
    _ Elims
    es   -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    es
        Lam ArgInfo
    _ Abs Term
    b    -> Term -> ()
    forall a. NFData a => a -> ()
    rnf (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b)
        Lit Literal
    l      -> Literal -> ()
    forall a. NFData a => a -> ()
    rnf Literal
    l
        Def QName
    _ Elims
    es   -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    es
        Con ConHead
    _ ConInfo
    _ Elims
    vs -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    vs
        Pi Dom Type
    a Abs Type
    b     -> (Type, Type) -> ()
    forall a. NFData a => a -> ()
    rnf (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a, Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b)
        Sort Sort
    s     -> Sort -> ()
    forall a. NFData a => a -> ()
    rnf Sort
    s
        Level Level
    l    -> Level -> ()
    forall a. NFData a => a -> ()
    rnf Level
    l
        MetaV MetaId
    _ Elims
    es -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    es
        DontCare Term
    v -> Term -> ()
    forall a. NFData a => a -> ()
    rnf Term
    v
        Dummy [Char]
    _ Elims
    es -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    es

    instance NFData Type where
      rnf :: Type -> ()
    rnf (El Sort
    s Term
    v) = (Sort, Term) -> ()
    forall a. NFData a => a -> ()
    rnf (Sort
    s, Term
    v)

    instance NFData Sort where
      rnf :: Sort -> ()
    rnf = \case
        Univ Univ
    _ Level
    l   -> Level -> ()
    forall a. NFData a => a -> ()
    rnf Level
    l
        Inf Univ
    _ Integer
    _  -> ()
        Sort
    SizeUniv -> ()
        Sort
    LockUniv -> ()
        Sort
    LevelUniv -> ()
        Sort
    IntervalUniv -> ()
        PiSort Dom' Term Term
    a Sort
    b Abs Sort
    c -> (Dom' Term Term, Sort, Sort) -> ()
    forall a. NFData a => a -> ()
    rnf (Dom' Term Term
    a, Sort
    b, Abs Sort -> Sort
    forall a. Abs a -> a
    unAbs Abs Sort
    c)
        FunSort Sort
    a Sort
    b -> (Sort, Sort) -> ()
    forall a. NFData a => a -> ()
    rnf (Sort
    a, Sort
    b)
        UnivSort Sort
    a -> Sort -> ()
    forall a. NFData a => a -> ()
    rnf Sort
    a
        MetaS MetaId
    _ Elims
    es -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    es
        DefS QName
    _ Elims
    es  -> Elims -> ()
    forall a. NFData a => a -> ()
    rnf Elims
    es
        DummyS [Char]
    _   -> ()

    instance NFData Level where
      rnf :: Level -> ()
    rnf (Max Integer
    n [PlusLevel' Term]
    as) = (Integer, [PlusLevel' Term]) -> ()
    forall a. NFData a => a -> ()
    rnf (Integer
    n, [PlusLevel' Term]
    as)

    instance NFData PlusLevel where
      rnf :: PlusLevel' Term -> ()
    rnf (Plus Integer
    n Term
    l) = (Integer, Term) -> ()
    forall a. NFData a => a -> ()
    rnf (Integer
    n, Term
    l)

    instance NFData e => NFData (Dom e) where
      rnf :: Dom e -> ()
    rnf (Dom ArgInfo
    a Maybe NamedName
    c Bool
    d Maybe Term
    e e
    f) = ArgInfo -> ()
    forall a. NFData a => a -> ()
    rnf ArgInfo
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe NamedName -> ()
    forall a. NFData a => a -> ()
    rnf Maybe NamedName
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Bool -> ()
    forall a. NFData a => a -> ()
    rnf Bool
    d () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe Term -> ()
    forall a. NFData a => a -> ()
    rnf Maybe Term
    e () -> () -> ()
    forall a b. a -> b -> b
    `seq` e -> ()
    forall a. NFData a => a -> ()
    rnf e
    f

    instance NFData a => NFData (DataOrRecord' a)
    instance NFData ConHead
    instance NFData a => NFData (Abs a)
    instance NFData a => NFData (Tele a)
    instance NFData IsFibrant
    instance NFData Clause
    instance NFData PatternInfo
    instance NFData PatOrigin
    instance NFData x => NFData (Pattern' x)
    instance NFData DBPatVar
    instance NFData ConPatternInfo
    instance NFData a => NFData (Substitution' a)