    -- Each function here should either have an INLINE or a SPECIALIZE pragma.
    --
    module Agda.TypeChecking.Pretty
        ( module Agda.TypeChecking.Pretty
        , module Reexport
        ) where

    import Prelude hiding ( null )

    import Control.Applicative  (liftA2)
    import Control.Monad
    import Control.Monad.Except

    import qualified Data.Foldable as Fold
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Maybe
    import Data.String    ()
    import Data.Semigroup (Semigroup((<>)))
    import Data.Text      (Text)

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty ( Pretty, prettyShow )
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Syntax.Fixity
    import Agda.Syntax.Internal
    import Agda.Syntax.Literal
    import Agda.Syntax.Translation.InternalToAbstract
    import Agda.Syntax.Translation.ReflectedToAbstract
    import Agda.Syntax.Translation.AbstractToConcrete
    import qualified Agda.Syntax.Translation.AbstractToConcrete as Reexport (MonadAbsToCon)
    import qualified Agda.Syntax.Translation.ReflectedToAbstract as R
    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Abstract.Pretty as AP
    import Agda.Syntax.Concrete.Pretty (bracesAndSemicolons)
    import qualified Agda.Syntax.Concrete.Pretty as CP
    import qualified Agda.Syntax.Info as A
    import Agda.Syntax.Scope.Base  (AbstractName(..))
    import Agda.Syntax.Scope.Monad (withContextPrecedence)
    import Agda.Syntax.TopLevelModuleName

    import Agda.TypeChecking.Coverage.SplitTree
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.DiscrimTree.Types
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope

    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
    import Agda.Utils.List1 ( List1, pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Null
    import Agda.Utils.Trie
    import Agda.Utils.Permutation ( Permutation )
    import qualified Agda.Utils.Maybe.Strict as S
    import Agda.Utils.Size ( Sized, natSize )

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Wrappers for pretty printing combinators
    ---------------------------------------------------------------------------

    type Doc = P.Doc

    comma, colon, equals :: Applicative m => m Doc
    comma :: forall (m :: * -> *). Applicative m => m Doc
    comma  = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    P.comma        ; {-# INLINE comma  #-}
    colon :: forall (m :: * -> *). Applicative m => m Doc
    colon  = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    P.colon        ; {-# INLINE colon  #-}
    equals :: forall (m :: * -> *). Applicative m => m Doc
    equals = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    P.equals       ; {-# INLINE equals #-}

    {-# INLINE pretty #-}
    pretty :: (Applicative m, P.Pretty a) => a -> m Doc
    pretty :: forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> m Doc) -> (a -> Doc) -> a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty

    {-# INLINE prettyA #-}
    prettyA :: (ToConcrete a, P.Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
    prettyA :: forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA = a -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    AP.prettyA

    {-# INLINE prettyAs #-}
    -- Triggers error: [GHC-69441] RULE left-hand side too complicated to desugar: ...
    -- {-# SPECIALIZE prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], P.Pretty ce) => a -> TCM Doc #-}
    prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], P.Pretty ce, MonadAbsToCon m) => a -> m Doc
    prettyAs :: forall a ce (m :: * -> *).
    (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
    a -> m Doc
    prettyAs = a -> m Doc
    forall a ce (m :: * -> *).
    (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
    a -> m Doc
    AP.prettyAs

    fwords, text, multiLineText :: Applicative m => String -> m Doc
    fwords :: forall (m :: * -> *). Applicative m => String -> m Doc
    fwords        = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Doc
    P.fwords        ; {-# INLINE fwords        #-}
    text :: forall (m :: * -> *). Applicative m => String -> m Doc
    text          = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Doc
    forall a. String -> Doc a
    P.text          ; {-# INLINE text          #-}
    multiLineText :: forall (m :: * -> *). Applicative m => String -> m Doc
    multiLineText = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Doc
    P.multiLineText ; {-# INLINE multiLineText #-}

    {-# INLINE pwords #-}
    pwords :: Applicative m => String -> [m Doc]
    pwords :: forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords = (Doc -> m Doc) -> [Doc] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Doc] -> [m Doc]) -> (String -> [Doc]) -> String -> [m Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [Doc]
    P.pwords

    sep, fsep, hsep, hcat, vcat, vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
    sep :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep  = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.sep  (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable  ; {-# SPECIALIZE NOINLINE sep  :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE sep  :: List1 (TCM Doc) -> TCM Doc #-}
    fsep :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.fsep (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable  ; {-# SPECIALIZE NOINLINE fsep :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE fsep :: List1 (TCM Doc) -> TCM Doc #-}
    hsep :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.hsep (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable  ; {-# SPECIALIZE NOINLINE hsep :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE hsep :: List1 (TCM Doc) -> TCM Doc #-}
    hcat :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hcat = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.hcat (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable  ; {-# SPECIALIZE NOINLINE hcat :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE hcat :: List1 (TCM Doc) -> TCM Doc #-}
    vcat :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.vcat (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable  ; {-# SPECIALIZE NOINLINE vcat :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE vcat :: List1 (TCM Doc) -> TCM Doc #-}
    vsep :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vsep = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    P.vsep (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable  ; {-# SPECIALIZE NOINLINE vsep :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE vsep :: List1 (TCM Doc) -> TCM Doc #-}

    {-# INLINE sequenceAFoldable #-}
    -- | @sequenceAFoldable == sequenceA . Fold.toList@
    sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]
    sequenceAFoldable :: forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable = (m a -> m [a] -> m [a]) -> m [a] -> t (m a) -> m [a]
    forall a b. (a -> b -> b) -> b -> t a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Fold.foldr ((a -> [a] -> [a]) -> m a -> m [a] -> m [a]
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (:)) ([a] -> m [a]
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [])

    {-# INLINE hang #-}
    hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
    hang :: forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang m Doc
    p Int
    n m Doc
    q = Doc -> Int -> Doc -> Doc
    forall a. Doc a -> Int -> Doc a -> Doc a
    P.hang (Doc -> Int -> Doc -> Doc) -> m Doc -> m (Int -> Doc -> Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Doc
    p m (Int -> Doc -> Doc) -> m Int -> m (Doc -> Doc)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> m Int
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Int
    n m (Doc -> Doc) -> m Doc -> m Doc
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m Doc
    q

    infixl 6 <+>, <?>
    infixl 5 $$, $+$

    ($$), ($+$), (<+>), (<?>) :: Applicative m => m Doc -> m Doc -> m Doc
    ($$ ) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    (P.$$)   ; {-# INLINE ($$)  #-}
    $+$ :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    ($+$) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    (P.$+$)  ; {-# INLINE ($+$) #-}
    <+> :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    (<+>) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    (P.<+>)  ; {-# INLINE (<+>) #-}
    <?> :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    (<?>) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Doc -> Doc -> Doc
    (P.<?>)  ; {-# INLINE (<?>) #-}

    nest :: Functor m => Int -> m Doc -> m Doc
    nest :: forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc -> Doc) -> m Doc -> m Doc)
    -> (Int -> Doc -> Doc) -> Int -> m Doc -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    P.nest    ; {-# INLINE nest  #-}

    braces, dbraces, brackets, parens, parensNonEmpty
      , doubleQuotes, quotes :: Functor m => m Doc -> m Doc
    braces :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    braces         = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    P.braces         ; {-# INLINE braces         #-}
    dbraces :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    dbraces        = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    CP.dbraces       ; {-# INLINE dbraces        #-}
    brackets :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    brackets       = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    P.brackets       ; {-# INLINE brackets       #-}
    parens :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens         = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    P.parens         ; {-# INLINE parens         #-}
    parensNonEmpty :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    parensNonEmpty = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    P.parensNonEmpty ; {-# INLINE parensNonEmpty #-}
    doubleQuotes :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    doubleQuotes   = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    P.doubleQuotes   ; {-# INLINE doubleQuotes   #-}
    quotes :: forall (m :: * -> *). Functor m => m Doc -> m Doc
    quotes         = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Doc -> Doc
    P.quotes         ; {-# INLINE quotes         #-}

    pshow :: (Applicative m, Show a) => a -> m Doc
    pshow :: forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
    pshow = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> m Doc) -> (a -> Doc) -> a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc
    forall a. Show a => a -> Doc
    P.pshow                 ; {-# INLINE pshow          #-}

    pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc
    pluralS :: forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
    pluralS = (Doc -> Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc -> Doc) -> m Doc -> m Doc)
    -> (a -> Doc -> Doc) -> a -> m Doc -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc -> Doc
    forall a. Sized a => a -> Doc -> Doc
    P.pluralS             ; {-# INLINE pluralS        #-}

    -- | Comma-separated list in brackets.
    {-# INLINE prettyList #-}
    prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
    prettyList :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList = ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t (m Doc) -> m [Doc]
    forall (m :: * -> *) (t :: * -> *) a.
    (Applicative m, Foldable t) =>
    t (m a) -> m [a]
    sequenceAFoldable

    -- | 'prettyList' without the brackets.
    {-# SPECIALIZE prettyList_ :: [TCM Doc]       -> TCM Doc #-}
    {-# SPECIALIZE prettyList_ :: List1 (TCM Doc) -> TCM Doc #-}
    prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
    prettyList_ :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> (t (m Doc) -> [m Doc]) -> t (m Doc) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m Doc -> t (m Doc) -> [m Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma

    {-# INLINABLE punctuate #-}
    {-# SPECIALIZE punctuate :: TCM Doc -> [TCM Doc] -> [TCM Doc] #-}
    {-# SPECIALIZE punctuate :: TCM Doc -> List1 (TCM Doc) -> [TCM Doc] #-}
    punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
    punctuate :: forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    d t (m Doc)
    ts
      | [m Doc] -> Bool
    forall a. Null a => a -> Bool
    null [m Doc]
    ds   = []
      | Bool
    otherwise = (m Doc -> m Doc -> m Doc) -> [m Doc] -> [m Doc] -> [m Doc]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    (<>) [m Doc]
    ds (Int -> m Doc -> [m Doc]
    forall a. Int -> a -> [a]
    replicate Int
    n m Doc
    d [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    forall a. Null a => a
    empty])
      where
        ds :: [m Doc]
    ds = t (m Doc) -> [m Doc]
    forall a. t a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList t (m Doc)
    ts
        n :: Int
    n  = [m Doc] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [m Doc]
    ds Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1

    {-# SPECIALIZE superscript :: Int -> TCM Doc #-}
    superscript :: Applicative m => Int -> m Doc
    superscript :: forall (m :: * -> *). Applicative m => Int -> m Doc
    superscript = String -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (String -> m Doc) -> (Int -> String) -> Int -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    forall a. [a] -> [a]
    reverse (String -> String) -> (Int -> String) -> Int -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> String
    go where
      digit :: Int -> Char
    digit = (String
    "⁰¹²³⁴⁵⁶⁷⁸⁹" String -> Int -> Char
    forall a. HasCallStack => [a] -> Int -> a
    !!)
      go :: Int -> String
    go Int
    k
        | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    9    = [Int -> Char
    digit Int
    k]
        | Bool
    otherwise = Int -> Char
    digit (Int
    k Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    10)Char -> String -> String
    forall a. a -> [a] -> [a]
    :Int -> String
    go (Int
    k Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` Int
    10)

    ---------------------------------------------------------------------------
    -- * The PrettyTCM class
    ---------------------------------------------------------------------------

    type MonadPretty m = MonadAbsToCon m

    -- This instance is to satify the constraints of superclass MonadPretty:
    -- | This instance is more specific than a generic instance
    -- @Semigroup a => Semigroup (TCM a)@.
    instance {-# OVERLAPPING #-} Semigroup (TCM Doc) where
      <> :: TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    (<>) = (Doc -> Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a b c. (a -> b -> c) -> TCMT IO a -> TCMT IO b -> TCMT IO c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    (<>) ; {-# INLINE (<>) #-}

    class PrettyTCM a where
      prettyTCM :: MonadPretty m => a -> m Doc

    -- | Pretty print with a given context precedence
    prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
    prettyTCMCtx :: forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    p = Precedence -> m Doc -> m Doc
    forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence Precedence
    p (m Doc -> m Doc) -> (a -> m Doc) -> a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM

    instance {-# OVERLAPPING #-} PrettyTCM String where prettyTCM :: forall (m :: * -> *). MonadPretty m => String -> m Doc
    prettyTCM = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text   ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Text                       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Text -> m Doc
    prettyTCM = Text -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Bool                       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Bool -> m Doc
    prettyTCM = Bool -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM C.Name                     where prettyTCM :: forall (m :: * -> *). MonadPretty m => Name -> m Doc
    prettyTCM = Name -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM C.QName                    where prettyTCM :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM = QName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM C.ImportedName             where prettyTCM :: forall (m :: * -> *). MonadPretty m => ImportedName -> m Doc
    prettyTCM = ImportedName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM C.LHS                      where prettyTCM :: forall (m :: * -> *). MonadPretty m => LHS -> m Doc
    prettyTCM = LHS -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM TopLevelModuleName         where prettyTCM :: forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
    prettyTCM = TopLevelModuleName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Comparison                 where prettyTCM :: forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
    prettyTCM = Comparison -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Literal                    where prettyTCM :: forall (m :: * -> *). MonadPretty m => Literal -> m Doc
    prettyTCM = Literal -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Nat                        where prettyTCM :: forall (m :: * -> *). MonadPretty m => Int -> m Doc
    prettyTCM = Int -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM ProblemId                  where prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemId -> m Doc
    prettyTCM = ProblemId -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Range                      where prettyTCM :: forall (m :: * -> *). MonadPretty m => Range -> m Doc
    prettyTCM = Range -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM CheckpointId               where prettyTCM :: forall (m :: * -> *). MonadPretty m => CheckpointId -> m Doc
    prettyTCM = CheckpointId -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM InteractionId              where prettyTCM :: forall (m :: * -> *). MonadPretty m => InteractionId -> m Doc
    prettyTCM = InteractionId -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Relevance                  where prettyTCM :: forall (m :: * -> *). MonadPretty m => Relevance -> m Doc
    prettyTCM = Relevance -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Quantity                   where prettyTCM :: forall (m :: * -> *). MonadPretty m => Quantity -> m Doc
    prettyTCM = Quantity -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM Erased                     where prettyTCM :: forall (m :: * -> *). MonadPretty m => Erased -> m Doc
    prettyTCM = Erased -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM ModalPolarity              where prettyTCM :: forall (m :: * -> *). MonadPretty m => ModalPolarity -> m Doc
    prettyTCM = ModalPolarity -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}
    instance PrettyTCM PolarityModality           where prettyTCM :: forall (m :: * -> *). MonadPretty m => PolarityModality -> m Doc
    prettyTCM = PolarityModality -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ; {-# INLINE prettyTCM #-}

    instance PrettyTCM A.Expr                     where prettyTCM :: forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM = Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA; {-# INLINE prettyTCM #-}
    instance PrettyTCM A.Pattern                  where prettyTCM :: forall (m :: * -> *). MonadPretty m => Pattern -> m Doc
    prettyTCM = Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA; {-# INLINE prettyTCM #-}
    instance PrettyTCM A.TypedBinding             where prettyTCM :: forall (m :: * -> *). MonadPretty m => TypedBinding -> m Doc
    prettyTCM = TypedBinding -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA; {-# INLINE prettyTCM #-}

    instance PrettyTCM Term               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM = Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Expr -> m Doc) -> (Term -> m Expr) -> Term -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Term -> m Expr
    Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify         ; {-# SPECIALIZE prettyTCM :: Term              -> TCM Doc #-}
    instance PrettyTCM Type               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM = Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Expr -> m Doc) -> (Type -> m Expr) -> Type -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Type -> m Expr
    Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify         ; {-# SPECIALIZE prettyTCM :: Type              -> TCM Doc #-}
    instance PrettyTCM Sort               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM = Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Expr -> m Doc) -> (Sort -> m Expr) -> Sort -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Sort -> m Expr
    Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify         ; {-# SPECIALIZE prettyTCM :: Sort              -> TCM Doc #-}
    instance PrettyTCM DisplayTerm        where prettyTCM :: forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
    prettyTCM = Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Expr -> m Doc) -> (DisplayTerm -> m Expr) -> DisplayTerm -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< DisplayTerm -> m Expr
    DisplayTerm -> m (ReifiesTo DisplayTerm)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    DisplayTerm -> m (ReifiesTo DisplayTerm)
    reify         ; {-# SPECIALIZE prettyTCM :: DisplayTerm       -> TCM Doc #-}
    instance PrettyTCM NamedClause        where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
    prettyTCM = Clause -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Clause -> m Doc)
    -> (NamedClause -> m Clause) -> NamedClause -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< NamedClause -> m Clause
    NamedClause -> m (ReifiesTo NamedClause)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    NamedClause -> m (ReifiesTo NamedClause)
    reify         ; {-# SPECIALIZE prettyTCM :: NamedClause       -> TCM Doc #-}
    instance PrettyTCM (QNamed Clause)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
    prettyTCM = Clause -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Clause -> m Doc)
    -> (QNamed Clause -> m Clause) -> QNamed Clause -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< QNamed Clause -> m Clause
    QNamed Clause -> m (ReifiesTo (QNamed Clause))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    QNamed Clause -> m (ReifiesTo (QNamed Clause))
    reify         ; {-# SPECIALIZE prettyTCM :: (QNamed Clause)   -> TCM Doc #-}
    instance PrettyTCM Level              where prettyTCM :: forall (m :: * -> *). MonadPretty m => Level -> m Doc
    prettyTCM = Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Expr -> m Doc) -> (Level -> m Expr) -> Level -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Term -> m Expr
    Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Term -> m Expr) -> (Level -> Term) -> Level -> m Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Level -> Term
    Level ; {-# SPECIALIZE prettyTCM :: Level             -> TCM Doc #-}
    instance PrettyTCM (Named_ Term)      where prettyTCM :: forall (m :: * -> *). MonadPretty m => Named_ Term -> m Doc
    prettyTCM = Named (WithOrigin (Ranged String)) Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Named (WithOrigin (Ranged String)) Expr -> m Doc)
    -> (Named_ Term -> m (Named (WithOrigin (Ranged String)) Expr))
    -> Named_ Term
    -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Named_ Term -> m (Named (WithOrigin (Ranged String)) Expr)
    Named_ Term -> m (ReifiesTo (Named_ Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Named_ Term -> m (ReifiesTo (Named_ Term))
    reify         ; {-# SPECIALIZE prettyTCM :: (Named_ Term)     -> TCM Doc #-}
    instance PrettyTCM (Arg Term)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM = Arg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg Expr -> m Doc)
    -> (Arg Term -> m (Arg Expr)) -> Arg Term -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Arg Term -> m (Arg Expr)
    Arg Term -> m (ReifiesTo (Arg Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Term -> m (ReifiesTo (Arg Term))
    reify         ; {-# SPECIALIZE prettyTCM :: (Arg Term)        -> TCM Doc #-}
    instance PrettyTCM (Arg Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
    prettyTCM = Arg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg Expr -> m Doc)
    -> (Arg Type -> m (Arg Expr)) -> Arg Type -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Arg Type -> m (Arg Expr)
    Arg Type -> m (ReifiesTo (Arg Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Type -> m (ReifiesTo (Arg Type))
    reify         ; {-# SPECIALIZE prettyTCM :: (Arg Type)        -> TCM Doc #-}
    instance PrettyTCM (Arg Bool)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
    prettyTCM = Arg Bool -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg Bool -> m Doc)
    -> (Arg Bool -> m (Arg Bool)) -> Arg Bool -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Arg Bool -> m (Arg Bool)
    Arg Bool -> m (ReifiesTo (Arg Bool))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Bool -> m (ReifiesTo (Arg Bool))
    reify         ; {-# SPECIALIZE prettyTCM :: (Arg Bool)        -> TCM Doc #-}
    instance PrettyTCM (Arg String)       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg String -> m Doc
    prettyTCM = Arg String -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg String -> m Doc)
    -> (Arg String -> m (Arg String)) -> Arg String -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Arg String -> m (Arg String)
    Arg String -> m (ReifiesTo (Arg String))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg String -> m (ReifiesTo (Arg String))
    reify         ; {-# SPECIALIZE prettyTCM :: (Arg String)      -> TCM Doc #-}
    instance PrettyTCM (Arg A.Expr)       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Expr -> m Doc
    prettyTCM = Arg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg Expr -> m Doc)
    -> (Arg Expr -> m (Arg Expr)) -> Arg Expr -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Arg Expr -> m (Arg Expr)
    Arg Expr -> m (ReifiesTo (Arg Expr))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Expr -> m (ReifiesTo (Arg Expr))
    reify         ; {-# SPECIALIZE prettyTCM :: (Arg A.Expr)      -> TCM Doc #-}
    instance PrettyTCM (NamedArg A.Expr)  where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
    prettyTCM = NamedArg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (NamedArg Expr -> m Doc)
    -> (NamedArg Expr -> m (NamedArg Expr)) -> NamedArg Expr -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< NamedArg Expr -> m (NamedArg Expr)
    NamedArg Expr -> m (ReifiesTo (NamedArg Expr))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    NamedArg Expr -> m (ReifiesTo (NamedArg Expr))
    reify         ; {-# SPECIALIZE prettyTCM :: (NamedArg A.Expr) -> TCM Doc #-}
    instance PrettyTCM (NamedArg Term)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Term -> m Doc
    prettyTCM = NamedArg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (NamedArg Expr -> m Doc)
    -> (NamedArg Term -> m (NamedArg Expr)) -> NamedArg Term -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< NamedArg Term -> m (NamedArg Expr)
    NamedArg Term -> m (ReifiesTo (NamedArg Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    NamedArg Term -> m (ReifiesTo (NamedArg Term))
    reify         ; {-# SPECIALIZE prettyTCM :: (NamedArg Term)   -> TCM Doc #-}
    instance PrettyTCM (Dom Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
    prettyTCM = Arg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg Expr -> m Doc)
    -> (Dom Type -> m (Arg Expr)) -> Dom Type -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Dom Type -> m (Arg Expr)
    Dom Type -> m (ReifiesTo (Dom Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Dom Type -> m (ReifiesTo (Dom Type))
    reify         ; {-# SPECIALIZE prettyTCM :: (Dom Type)        -> TCM Doc #-}
    instance PrettyTCM ContextEntry       where prettyTCM :: forall (m :: * -> *). MonadPretty m => ContextEntry -> m Doc
    prettyTCM = TypedBinding -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (TypedBinding -> m Doc)
    -> (ContextEntry -> m TypedBinding) -> ContextEntry -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< ContextEntry -> m TypedBinding
    ContextEntry -> m (ReifiesTo ContextEntry)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    ContextEntry -> m (ReifiesTo ContextEntry)
    reify         ; {-# SPECIALIZE prettyTCM :: ContextEntry      -> TCM Doc #-}

    instance PrettyTCM Permutation        where prettyTCM :: forall (m :: * -> *). MonadPretty m => Permutation -> m Doc
    prettyTCM = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc)
    -> (Permutation -> String) -> Permutation -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Permutation -> String
    forall a. Show a => a -> String
    show               ; {-# SPECIALIZE prettyTCM :: Permutation       -> TCM Doc #-}
    instance PrettyTCM Polarity           where prettyTCM :: forall (m :: * -> *). MonadPretty m => Polarity -> m Doc
    prettyTCM = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> (Polarity -> String) -> Polarity -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Polarity -> String
    forall a. Show a => a -> String
    show               ; {-# SPECIALIZE prettyTCM :: Polarity          -> TCM Doc #-}
    instance PrettyTCM IsForced           where prettyTCM :: forall (m :: * -> *). MonadPretty m => IsForced -> m Doc
    prettyTCM = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> (IsForced -> String) -> IsForced -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IsForced -> String
    forall a. Show a => a -> String
    show               ; {-# SPECIALIZE prettyTCM :: IsForced          -> TCM Doc #-}

    instance PrettyTCM Name         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Name -> m Doc
    prettyTCM = (Name -> Doc) -> m Name -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (m Name -> m Doc) -> (Name -> m Name) -> Name -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> m Name
    Name -> m (ConOfAbs Name)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ ; {-# SPECIALIZE prettyTCM :: Name          -> TCM Doc #-}
    instance PrettyTCM QName        where prettyTCM :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM = (QName -> Doc) -> m QName -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap QName -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (m QName -> m Doc) -> (QName -> m QName) -> QName -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> m QName
    QName -> m (ConOfAbs QName)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ ; {-# SPECIALIZE prettyTCM :: QName         -> TCM Doc #-}
    instance PrettyTCM ModuleName   where prettyTCM :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
    prettyTCM = (QName -> Doc) -> m QName -> m Doc
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap QName -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (m QName -> m Doc)
    -> (ModuleName -> m QName) -> ModuleName -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> m QName
    ModuleName -> m (ConOfAbs ModuleName)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ ; {-# SPECIALIZE prettyTCM :: ModuleName    -> TCM Doc #-}

    instance PrettyTCM AbstractName where prettyTCM :: forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
    prettyTCM = QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (QName -> m Doc)
    -> (AbstractName -> QName) -> AbstractName -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName           ; {-# SPECIALIZE prettyTCM :: AbstractName -> TCM Doc #-}
    instance PrettyTCM ConHead      where prettyTCM :: forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM = QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (QName -> m Doc) -> (ConHead -> QName) -> ConHead -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName             ; {-# SPECIALIZE prettyTCM :: ConHead      -> TCM Doc #-}
    instance PrettyTCM DBPatVar     where prettyTCM :: forall (m :: * -> *). MonadPretty m => DBPatVar -> m Doc
    prettyTCM = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Term -> m Doc) -> (DBPatVar -> Term) -> DBPatVar -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var (Int -> Term) -> (DBPatVar -> Int) -> DBPatVar -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DBPatVar -> Int
    dbPatVarIndex ; {-# SPECIALIZE prettyTCM :: DBPatVar     -> TCM Doc #-}
    instance PrettyTCM EqualityView where prettyTCM :: forall (m :: * -> *). MonadPretty m => EqualityView -> m Doc
    prettyTCM = Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Type -> m Doc) -> (EqualityView -> Type) -> EqualityView -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EqualityView -> Type
    forall a. EqualityUnview a => a -> Type
    equalityUnview      ; {-# SPECIALIZE prettyTCM :: EqualityView -> TCM Doc #-}

    -- Functors

    instance (PrettyTCM a, Subst a) => PrettyTCM (Abs a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Abs a -> m Doc
    prettyTCM Abs a
    a = Abs a -> (a -> m Doc) -> m Doc
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ Abs a
    a a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Abs a -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (Closure a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Closure a -> m Doc
    prettyTCM Closure a
    cl = Closure a -> (a -> m Doc) -> m Doc
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure a
    cl a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Closure a -> TCM Doc #-}

    instance {-# OVERLAPPABLE #-} PrettyTCM a => PrettyTCM [a] where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => [a] -> m Doc
    prettyTCM = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([m Doc] -> m Doc) -> ([a] -> [m Doc]) -> [a] -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m Doc) -> [a] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => [a] -> TCM Doc #-}

    instance {-# OVERLAPPABLE #-} PrettyTCM a => PrettyTCM (List1 a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => List1 a -> m Doc
    prettyTCM = NonEmpty (m Doc) -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList (NonEmpty (m Doc) -> m Doc)
    -> (List1 a -> NonEmpty (m Doc)) -> List1 a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m Doc) -> List1 a -> NonEmpty (m Doc)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => [a] -> TCM Doc #-}

    instance {-# OVERLAPPABLE #-} PrettyTCM a => PrettyTCM (Maybe a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Maybe a -> m Doc
    prettyTCM = m Doc -> (a -> m Doc) -> Maybe a -> m Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m Doc
    forall a. Null a => a
    empty a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Maybe a -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (Set a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Set a -> m Doc
    prettyTCM = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    braces (m Doc -> m Doc) -> (Set a -> m Doc) -> Set a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ([m Doc] -> m Doc) -> (Set a -> [m Doc]) -> Set a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m Doc) -> [a] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM ([a] -> [m Doc]) -> (Set a -> [a]) -> Set a -> [m Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set a -> [a]
    forall a. Set a -> [a]
    Set.toList
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Set a -> TCM Doc #-}

    instance (PrettyTCM a, PrettyTCM b) => PrettyTCM (a,b) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => (a, b) -> m Doc
    prettyTCM (a
    a, b
    b) = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> b -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => b -> m Doc
    prettyTCM b
    b
    {-# SPECIALIZE prettyTCM :: (PrettyTCM a, PrettyTCM b) => (a, b) -> TCM Doc #-}

    instance (PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a,b,c) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => (a, b, c) -> m Doc
    prettyTCM (a
    a, b
    b, c
    c) = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $
        a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> b -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => b -> m Doc
    prettyTCM b
    b m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> c -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => c -> m Doc
    prettyTCM c
    c
    {-# SPECIALIZE prettyTCM :: (PrettyTCM a, PrettyTCM b, PrettyTCM c) => (a, b, c) -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (MaybeReduced a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => MaybeReduced a -> m Doc
    prettyTCM = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM (a -> m Doc) -> (MaybeReduced a -> a) -> MaybeReduced a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MaybeReduced a -> a
    forall a. MaybeReduced a -> a
    ignoreReduced
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => MaybeReduced a -> TCM Doc #-}

    instance (Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Substitution' a -> m Doc
    prettyTCM Substitution' a
    IdS        = m Doc
    "idS"
      prettyTCM (Wk Int
    m Substitution' a
    IdS) = m Doc
    "wkS" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Int
    m
      prettyTCM (EmptyS Impossible
    _) = m Doc
    "emptyS"
      prettyTCM Substitution' a
    rho = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    u m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution' a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Substitution' a -> m Doc
    prettyTCM Substitution' a
    rho1
        where
          (Substitution' a
    rho1, Substitution' a
    rho2) = Int -> Substitution' a -> (Substitution' a, Substitution' a)
    forall a.
    Int -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS Int
    1 Substitution' a
    rho
          u :: a
    u            = Substitution' a -> Int -> a
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution' a
    rho2 Int
    0
    {-# SPECIALIZE prettyTCM :: (Pretty a, PrettyTCM a, EndoSubst a) => Substitution' a -> TCM Doc #-}

    instance PrettyTCM Clause where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Clause -> m Doc
    prettyTCM Clause
    cl = do
        x <- Name -> QName
    qualify_ (Name -> QName) -> m Name -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => String -> m Name
    freshName_ (String
    "<unnamedclause>" :: String)
        prettyTCM (QNamed x cl)
    {-# SPECIALIZE prettyTCM :: Clause -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (Judgement a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Judgement a -> m Doc
    prettyTCM (HasType a
    a Comparison
    cmp Type
    t) = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
      prettyTCM (IsSort  a
    a Type
    t) = m Doc
    "Sort" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Judgement a -> TCM Doc #-}

    instance PrettyTCM MetaId where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    x = do
        mn <- MetaId -> m String
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m String
    getMetaNameSuggestion MetaId
    x
        prettyTCM $ NamedMeta mn x
    {-# SPECIALIZE prettyTCM :: MetaId -> TCM Doc #-}

    instance PrettyTCM NamedMeta where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedMeta -> m Doc
    prettyTCM (NamedMeta String
    s MetaId
    m) = do
        current <- m ModuleNameHash
    forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash
        prefix  <-
          if metaModule m == current
          then return empty
          else do
            modName <- BiMap.invLookup (metaModule m) <$>
                       useR stTopLevelModuleNames
            return $ case modName of
              Maybe RawTopLevelModuleName
    Nothing      -> m Doc
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Just RawTopLevelModuleName
    modName -> RawTopLevelModuleName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty RawTopLevelModuleName
    modName m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "."
        let inBetween = case String
    s of
              String
    ""  -> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "_"
              String
    "_" -> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "_"
              String
    s   -> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> String -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_"
        prefix <> inBetween <> text (show (metaId m))
    {-# SPECIALIZE prettyTCM :: NamedMeta -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (Blocked a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Blocked a -> m Doc
    prettyTCM (Blocked Blocker
    x a
    a) = (m Doc
    "[" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "]") m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocker -> String
    forall a. Pretty a => a -> String
    P.prettyShow Blocker
    x)
      prettyTCM (NotBlocked NotBlocked' Term
    _ a
    x) = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    x
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Blocked a -> TCM Doc #-}

    instance (PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Map k v -> m Doc
    prettyTCM Map k v
    m = m Doc
    "Map" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    braces ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc -> [m Doc] -> [m Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma
        [ m Doc -> Int -> m Doc -> m Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang (k -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => k -> m Doc
    prettyTCM k
    k m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "=") Int
    2 (v -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => v -> m Doc
    prettyTCM v
    v) | (k
    k, v
    v) <- Map k v -> [(k, v)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map k v
    m ])
    {-# SPECIALIZE prettyTCM :: (PrettyTCM k, PrettyTCM v) => Map k v -> TCM Doc  #-}

    -- instance {-# OVERLAPPING #-} PrettyTCM ArgName where
    --   prettyTCM = text . P.prettyShow

    -- instance (Reify a e, ToConcrete e c, P.Pretty c, PrettyTCM a) => PrettyTCM (Elim' a) where
    instance PrettyTCM Elim where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM (IApply Term
    x Term
    y Term
    v) = m Doc
    "I$" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
      prettyTCM (Apply Arg Term
    v) = m Doc
    "$" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM Arg Term
    v
      prettyTCM (Proj ProjOrigin
    _ QName
    f)= m Doc
    "." m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f
    {-# SPECIALIZE prettyTCM :: Elim -> TCM Doc #-}

    deriving instance (PrettyTCM x, PrettyTCM a) => PrettyTCM (Boundary' x a)

    instance PrettyTCM Modality where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Modality -> m Doc
    prettyTCM Modality
    mod = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
        [ Quantity -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Quantity -> m Doc
    prettyTCM (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Modality
    mod)
        , Relevance -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Relevance -> m Doc
    prettyTCM (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod)
        , PolarityModality -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => PolarityModality -> m Doc
    prettyTCM (Modality -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity Modality
    mod)
        ]
    {-# SPECIALIZE prettyTCM :: Modality -> TCM Doc #-}

    instance PrettyTCM Blocker where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM (UnblockOnAll Set Blocker
    us) = m Doc
    "all" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc -> [m Doc] -> [m Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    "," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> m Doc) -> [Blocker] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM ([Blocker] -> [m Doc]) -> [Blocker] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us)
      prettyTCM (UnblockOnAny Set Blocker
    us) = m Doc
    "any" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc -> [m Doc] -> [m Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    "," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> m Doc) -> [Blocker] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM ([Blocker] -> [m Doc]) -> [Blocker] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us)
      prettyTCM (UnblockOnMeta MetaId
    m) = MetaId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m
      prettyTCM (UnblockOnProblem ProblemId
    p) = m Doc
    "problem" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ProblemId -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ProblemId
    p
      prettyTCM (UnblockOnDef QName
    q) = m Doc
    "definition" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    q
    {-# SPECIALIZE prettyTCM :: Blocker -> TCM Doc #-}

    instance PrettyTCM CompareAs where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
    prettyTCM (AsTermsOf Type
    a) = m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Precedence -> Type -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx Type
    a
      prettyTCM CompareAs
    AsSizes       = m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Type -> m Doc) -> m Type -> m Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType
      prettyTCM CompareAs
    AsTypes       = m Doc
    forall a. Null a => a
    empty
    {-# SPECIALIZE prettyTCM :: CompareAs -> TCM Doc #-}

    instance PrettyTCM TypeCheckingProblem where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
    prettyTCM (CheckExpr Comparison
    cmp Expr
    e Type
    a) =
        [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":?", Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a ]
      prettyTCM (CheckArgs Comparison
    _ ExpandHidden
    _ Expr
    _ [NamedArg Expr]
    es Type
    t0 Type
    t1 ArgsCheckState CheckedTarget -> TCM Term
    _) =
        [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc
    "_ :" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t0
            , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Expr -> m Doc) -> [NamedArg Expr] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Expr]
    es
            , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc
    ":?" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t1 ]
      prettyTCM (CheckProjAppToKnownPrincipalArg Comparison
    cmp Expr
    e ProjOrigin
    _ List1 QName
    _ Expr
    _ [NamedArg Expr]
    _ Type
    t Int
    _ Term
    _ Type
    _ PrincipalArgTypeMetas
    _) = TypeCheckingProblem -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
    prettyTCM (Comparison -> Expr -> Type -> TypeCheckingProblem
    CheckExpr Comparison
    cmp Expr
    e Type
    t)
      prettyTCM (CheckLambda Comparison
    cmp (Arg ArgInfo
    ai (List1 (WithHiding Name)
    xs, Maybe Type
    mt)) Expr
    e Type
    t) =
        [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    CP.lambda m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              (ArgInfo -> Doc -> Doc
    forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance ArgInfo
    ai (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
               ArgInfo -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding ArgInfo
    ai (if Maybe Type -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe Type
    mt Bool -> Bool -> Bool
    && List1 (WithHiding Name) -> Peano
    forall a. Sized a => a -> Peano
    natSize List1 (WithHiding Name)
    xs Peano -> Peano -> Bool
    forall a. Eq a => a -> a -> Bool
    == Peano
    1 then Doc -> Doc
    forall a. a -> a
    id
                                   else Doc -> Doc
    P.parens) (Doc -> Doc) -> m Doc -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
                  (WithHiding Name -> m Doc) -> [WithHiding Name] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map WithHiding Name -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => WithHiding Name -> m Doc
    prettyTCM (List1 (WithHiding Name) -> [Item (List1 (WithHiding Name))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (WithHiding Name)
    xs) [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                  Maybe Type -> [m Doc] -> (Type -> [m Doc]) -> [m Doc]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Type
    mt [] (\ Type
    a -> [m Doc
    ":", Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a])) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    CP.arrow m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              Expr -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM Expr
    e m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              m Doc
    ":?"
            , Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
            ]
      prettyTCM (DoQuoteTerm Comparison
    _ Term
    v Type
    _) = do
        e <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v
        prettyTCM (A.App A.defaultAppInfo_ (A.QuoteTerm A.exprNoRange) (defaultNamedArg e))
      prettyTCM (DisambiguateConstructor (ConstructorDisambiguationData QName
    c0 List1 (QName, Type, ConHead)
    cands [NamedArg Expr]
    args Type
    t) ConHead -> TCM Term
    _) = do
        let e :: Expr
    e = (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
    A.App AppInfo
    forall a. Null a => a
    empty) (AmbiguousQName -> Expr
    A.Con (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    c0) [NamedArg Expr]
    args
        m Doc
    "ambiguous constructor" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
    {-# SPECIALIZE prettyTCM :: TypeCheckingProblem -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (WithHiding a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => WithHiding a -> m Doc
    prettyTCM (WithHiding Hiding
    h a
    a) = Hiding -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding Hiding
    h Doc -> Doc
    forall a. a -> a
    id (Doc -> Doc) -> m Doc -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => WithHiding a -> TCM Doc #-}

    instance PrettyTCM Telescope where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    tel = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.fsep ([Doc] -> Doc)
    -> ([Maybe TypedBinding] -> [Doc]) -> [Maybe TypedBinding] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe TypedBinding -> Doc) -> [Maybe TypedBinding] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Maybe TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty ([Maybe TypedBinding] -> Doc) -> m [Maybe TypedBinding] -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          Telescope -> m [Maybe TypedBinding]
    forall (m :: * -> *).
    MonadAbsToCon m =>
    Telescope -> m [Maybe TypedBinding]
    abstractToConcreteTelescope (Telescope -> m [Maybe TypedBinding])
    -> m Telescope -> m [Maybe TypedBinding]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Telescope -> m (ReifiesTo Telescope)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Telescope -> m (ReifiesTo Telescope)
    reify Telescope
    tel
    {-# SPECIALIZE prettyTCM :: Telescope -> TCM Doc #-}

    newtype PrettyContext = PrettyContext Context

    instance PrettyTCM PrettyContext where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => PrettyContext -> m Doc
    prettyTCM (PrettyContext Context
    ctx) = Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM (Telescope -> m Doc) -> Telescope -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Context -> Telescope
    contextToTel Context
    ctx
    {-# SPECIALIZE prettyTCM :: PrettyContext -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (Pattern' a) where
      prettyTCM :: forall m. MonadPretty m => Pattern' a -> m Doc
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
    prettyTCM (IApplyP PatternInfo
    _ Term
    _ Term
    _ a
    x)    = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    x
      prettyTCM (VarP PatternInfo
    _ a
    x)    = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    x
      prettyTCM (DotP PatternInfo
    _ Term
    t)    = m Doc
    ".(" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ")"
      prettyTCM (DefP PatternInfo
    o QName
    q [NamedArg (Pattern' a)]
    ps) = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $
            QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((NamedArg (Pattern' a) -> m Doc)
    -> [NamedArg (Pattern' a)] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern' a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
    prettyTCM (Pattern' a -> m Doc)
    -> (NamedArg (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a)
    -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg) [NamedArg (Pattern' a)]
    ps)
      prettyTCM (ConP ConHead
    c ConPatternInfo
    i [NamedArg (Pattern' a)]
    ps) = -- (if b then braces else parens) $ prTy $
            m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $
            ConHead -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((NamedArg (Pattern' a) -> m Doc)
    -> [NamedArg (Pattern' a)] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern' a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
    prettyTCM (Pattern' a -> m Doc)
    -> (NamedArg (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a)
    -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg) [NamedArg (Pattern' a)]
    ps)
          where
            -- NONE OF THESE BINDINGS IS USED AT THE MOMENT:
            b :: Bool
    b = ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    i Bool -> Bool -> Bool
    && PatternInfo -> PatOrigin
    patOrigin (ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    i) PatOrigin -> PatOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= PatOrigin
    PatOCon
            showRec :: m Doc -- Defined, but currently not used
            showRec :: m Doc
    showRec = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ m Doc
    "record"
              , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons ([Doc] -> Doc) -> m [Doc] -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg QName -> NamedArg (Pattern' a) -> m Doc)
    -> [Arg QName] -> [NamedArg (Pattern' a)] -> m [Doc]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Arg QName -> NamedArg (Pattern' a) -> m Doc
    showField (ConHead -> [Arg QName]
    conFields ConHead
    c) [NamedArg (Pattern' a)]
    ps
              ]
            showField :: Arg QName -> NamedArg (Pattern' a) -> m Doc -- NB:: Defined but not used
            showField :: Arg QName -> NamedArg (Pattern' a) -> m Doc
    showField (Arg ArgInfo
    ai QName
    x) NamedArg (Pattern' a)
    p =
              [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Name -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Name -> m Doc
    prettyTCM (QName -> Name
    A.qnameName QName
    x) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "=" , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Pattern' a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
    prettyTCM (Pattern' a -> m Doc) -> Pattern' a -> m Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' a)
    p ]
            showCon :: m Doc -- NB:: Defined but not used
            showCon :: m Doc
    showCon = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc -> m Doc
    prTy (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ ConHead -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((NamedArg (Pattern' a) -> m Doc)
    -> [NamedArg (Pattern' a)] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern' a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
    prettyTCM (Pattern' a -> m Doc)
    -> (NamedArg (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a)
    -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg) [NamedArg (Pattern' a)]
    ps)
            prTy :: m Doc -> m Doc
    prTy m Doc
    d = Maybe (Arg Type) -> m Doc -> (Arg Type -> m Doc) -> m Doc
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (ConPatternInfo -> Maybe (Arg Type)
    conPType ConPatternInfo
    i) m Doc
    d ((Arg Type -> m Doc) -> m Doc) -> (Arg Type -> m Doc) -> m Doc
    forall a b. (a -> b) -> a -> b
    $ \ Arg Type
    t -> m Doc
    d  m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Arg Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
    prettyTCM Arg Type
    t
      prettyTCM (LitP PatternInfo
    _ Literal
    l)    = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Literal -> String
    forall a. Pretty a => a -> String
    P.prettyShow Literal
    l)
      prettyTCM (ProjP ProjOrigin
    _ QName
    q)   = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String
    "." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    P.prettyShow QName
    q)
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => Pattern' a -> TCM Doc #-}

    {-# SPECIALIZE prettyTCMPatterns :: [NamedArg DeBruijnPattern] -> TCM [Doc] #-}
    -- | Proper pretty printing of patterns:
    prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
    prettyTCMPatterns :: forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m [Doc]
    prettyTCMPatterns = (NamedArg Pattern -> m Doc) -> [NamedArg Pattern] -> m [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM NamedArg Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA ([NamedArg Pattern] -> m [Doc])
    -> ([NamedArg DeBruijnPattern] -> m [NamedArg Pattern])
    -> [NamedArg DeBruijnPattern]
    -> m [Doc]
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
    forall (m :: * -> *).
    MonadReify m =>
    [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
    reifyPatterns

    {-# SPECIALIZE prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> TCM Doc #-}
    prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
    prettyTCMPatternList :: forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m Doc
    prettyTCMPatternList = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([m Doc] -> m Doc)
    -> ([NamedArg Pattern] -> [m Doc]) -> [NamedArg Pattern] -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NamedArg Pattern -> m Doc) -> [NamedArg Pattern] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA ([NamedArg Pattern] -> m Doc)
    -> ([NamedArg DeBruijnPattern] -> m [NamedArg Pattern])
    -> [NamedArg DeBruijnPattern]
    -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
    forall (m :: * -> *).
    MonadReify m =>
    [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
    reifyPatterns

    -- | For unquote.
    {-# SPECIALIZE prettyR :: (R.ToAbstract r, PrettyTCM (R.AbsOfRef r)) => r -> TCM Doc #-}
    prettyR :: (R.ToAbstract r, PrettyTCM (R.AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
    prettyR :: forall r (m :: * -> *).
    (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
     MonadError TCErr m) =>
    r -> m Doc
    prettyR = AbsOfRef r -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => AbsOfRef r -> m Doc
    prettyTCM (AbsOfRef r -> m Doc) -> (r -> m (AbsOfRef r)) -> r -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< r -> m (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstractWithoutImplicit

    instance PrettyTCM (Elim' DisplayTerm) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim' DisplayTerm -> m Doc
    prettyTCM (IApply DisplayTerm
    x DisplayTerm
    y DisplayTerm
    v) = m Doc
    "$" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> DisplayTerm -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
    prettyTCM DisplayTerm
    v
      prettyTCM (Apply Arg DisplayTerm
    v) = m Doc
    "$" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> DisplayTerm -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
    prettyTCM (Arg DisplayTerm -> DisplayTerm
    forall e. Arg e -> e
    unArg Arg DisplayTerm
    v)
      prettyTCM (Proj ProjOrigin
    _ QName
    f)= m Doc
    "." m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f
    {-# SPECIALIZE prettyTCM :: Elim' DisplayTerm -> TCM Doc #-}

    instance PrettyTCM NLPat where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM (PVar Int
    x [Arg Int]
    bvs) = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Int -> Elims -> Term
    Var Int
    x ((Arg Int -> Elim) -> [Arg Int] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> (Arg Int -> Arg Term) -> Arg Int -> Elim
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Term) -> Arg Int -> Arg Term
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> Term
    var) [Arg Int]
    bvs))
      prettyTCM (PDef QName
    f PElims
    es) = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $
        QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((Elim' NLPat -> m Doc) -> PElims -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim' NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
    prettyTCM PElims
    es)
      prettyTCM (PLam ArgInfo
    i Abs NLPat
    u)  = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
        [ m Doc
    "λ"
        , ArgInfo -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding ArgInfo
    i Doc -> Doc
    forall a. a -> a
    id (Doc -> Doc) -> m Doc -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Abs NLPat -> String
    forall a. Abs a -> String
    absName Abs NLPat
    u)
        , m Doc
    "→"
        , String -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
    addContext (Abs NLPat -> String
    forall a. Abs a -> String
    absName Abs NLPat
    u) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM (NLPat -> m Doc) -> NLPat -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Abs NLPat -> NLPat
    forall a. Subst a => Abs a -> a
    absBody Abs NLPat
    u
        ]
      prettyTCM (PPi Dom NLPType
    a Abs NLPType
    b)   = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
        [ Dom NLPType -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding Dom NLPType
    a Doc -> Doc
    P.parens (Doc -> Doc) -> m Doc -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> String -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Abs NLPType -> String
    forall a. Abs a -> String
    absName Abs NLPType
    b, m Doc
    ":", NLPType -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPType -> m Doc
    prettyTCM (NLPType -> m Doc) -> NLPType -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Dom NLPType -> NLPType
    forall t e. Dom' t e -> e
    unDom Dom NLPType
    a ]
        , m Doc
    "→"
        , String -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
    addContext (Abs NLPType -> String
    forall a. Abs a -> String
    absName Abs NLPType
    b) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ NLPType -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPType -> m Doc
    prettyTCM (NLPType -> m Doc) -> NLPType -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Abs NLPType -> NLPType
    forall a. Abs a -> a
    unAbs Abs NLPType
    b
        ]
      prettyTCM (PSort NLPSort
    s)        = NLPSort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
    prettyTCM NLPSort
    s
      prettyTCM (PBoundVar Int
    i []) = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Int -> Term
    var Int
    i)
      prettyTCM (PBoundVar Int
    i PElims
    es) = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Int -> Term
    var Int
    i) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((Elim' NLPat -> m Doc) -> PElims -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim' NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
    prettyTCM PElims
    es)
      prettyTCM (PTerm Term
    t)   = m Doc
    "." m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t)
    {-# SPECIALIZE prettyTCM :: NLPat -> TCM Doc #-}

    instance PrettyTCM NLPType where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPType -> m Doc
    prettyTCM (NLPType NLPSort
    s NLPat
    a) = NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM NLPat
    a
    {-# SPECIALIZE prettyTCM :: NLPType -> TCM Doc #-}

    instance PrettyTCM NLPSort where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
    prettyTCM = \case
        PUniv Univ
    u NLPat
    l -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Univ -> String
    showUniv Univ
    u) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM NLPat
    l
          -- Andreas, 2023-05-11, preserving Jesper's printing hack for now...
        PInf Univ
    u Integer
    n  -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM (Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    u Integer
    n :: Sort)
        NLPSort
    PSizeUniv -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM (Sort
    forall t. Sort' t
    SizeUniv :: Sort)
        NLPSort
    PLockUniv -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM (Sort
    forall t. Sort' t
    LockUniv :: Sort)
        NLPSort
    PLevelUniv -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM (Sort
    forall t. Sort' t
    LevelUniv :: Sort)
        NLPSort
    PIntervalUniv -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM (Sort
    forall t. Sort' t
    IntervalUniv :: Sort)
    {-# SPECIALIZE prettyTCM :: NLPSort -> TCM Doc #-}

    instance PrettyTCM (Elim' NLPat) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
    prettyTCM (IApply NLPat
    x NLPat
    y NLPat
    v) = NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM NLPat
    v
      prettyTCM (Apply Arg NLPat
    v) = Arg NLPat -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding Arg NLPat
    v Doc -> Doc
    forall a. a -> a
    id (Doc -> Doc) -> m Doc -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM (Arg NLPat -> NLPat
    forall e. Arg e -> e
    unArg Arg NLPat
    v)
      prettyTCM (Proj ProjOrigin
    _ QName
    f)= m Doc
    "." m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f
    {-# SPECIALIZE prettyTCM :: Elim' NLPat -> TCM Doc #-}

    instance PrettyTCM (Type' NLPat) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Type' NLPat -> m Doc
    prettyTCM = NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM (NLPat -> m Doc) -> (Type' NLPat -> NLPat) -> Type' NLPat -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type' NLPat -> NLPat
    forall t a. Type'' t a -> a
    unEl
    {-# SPECIALIZE prettyTCM :: Type' NLPat -> TCM Doc #-}

    instance PrettyTCM RewriteRule where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => RewriteRule -> m Doc
    prettyTCM (RewriteRule QName
    q Telescope
    gamma QName
    f PElims
    ps Term
    rhs Type
    b Bool
    _c TopLevelModuleName
    _top) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
        [ QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
        , Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    gamma m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    " |- "
        , Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM (QName -> PElims -> NLPat
    PDef QName
    f PElims
    ps)
          , m Doc
    " --> "
          , Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    rhs
          , m Doc
    " : "
          , Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    b
          ]
        ]
    {-# SPECIALIZE prettyTCM :: RewriteRule -> TCM Doc #-}

    instance PrettyTCM Occurrence where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Occurrence -> m Doc
    prettyTCM Occurrence
    occ  = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> String -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "-[" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Occurrence -> String
    forall a. Pretty a => a -> String
    prettyShow Occurrence
    occ String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "]->"
    {-# SPECIALIZE prettyTCM :: Occurrence -> TCM Doc #-}

    -- | Pairing something with a node (for printing only).
    data WithNode n a = WithNode n a

    -- | Pretty-print something paired with a (printable) node.
    -- | This intermediate typeclass exists to avoid UndecidableInstances.
    class PrettyTCMWithNode a where
      prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc

    instance PrettyTCMWithNode Occurrence where
      prettyTCMWithNode :: forall n (m :: * -> *).
    (PrettyTCM n, MonadPretty m) =>
    WithNode n Occurrence -> m Doc
    prettyTCMWithNode (WithNode n
    n Occurrence
    o) = Occurrence -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Occurrence -> m Doc
    prettyTCM Occurrence
    o m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> n -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => n -> m Doc
    prettyTCM n
    n

    instance (PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Graph n e -> m Doc
    prettyTCM Graph n e
    g = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ ((n, Map n e) -> m Doc) -> [(n, Map n e)] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (n, Map n e) -> m Doc
    forall {m :: * -> *} {a} {a} {n}.
    (MonadFresh NameId m, MonadInteractionPoints m,
     MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
     Semigroup (m Doc), PrettyTCMWithNode a, PrettyTCM a,
     PrettyTCM n) =>
    (a, Map n a) -> m Doc
    pr ([(n, Map n e)] -> [m Doc]) -> [(n, Map n e)] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ Map n (Map n e) -> [(n, Map n e)]
    forall k a. Map k a -> [(k, a)]
    Map.assocs (Map n (Map n e) -> [(n, Map n e)])
    -> Map n (Map n e) -> [(n, Map n e)]
    forall a b. (a -> b) -> a -> b
    $ Graph n e -> Map n (Map n e)
    forall n e. Graph n e -> Map n (Map n e)
    Graph.graph Graph n e
    g
        where
          pr :: (a, Map n a) -> m Doc
    pr (a
    n, Map n a
    es) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    n
            , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ ((n, a) -> m Doc) -> [(n, a)] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (WithNode n a -> m Doc
    forall a n (m :: * -> *).
    (PrettyTCMWithNode a, PrettyTCM n, MonadPretty m) =>
    WithNode n a -> m Doc
    forall n (m :: * -> *).
    (PrettyTCM n, MonadPretty m) =>
    WithNode n a -> m Doc
    prettyTCMWithNode (WithNode n a -> m Doc)
    -> ((n, a) -> WithNode n a) -> (n, a) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (n -> a -> WithNode n a) -> (n, a) -> WithNode n a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry n -> a -> WithNode n a
    forall n a. n -> a -> WithNode n a
    WithNode) ([(n, a)] -> [m Doc]) -> [(n, a)] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ Map n a -> [(n, a)]
    forall k a. Map k a -> [(k, a)]
    Map.assocs Map n a
    es
            ]
    {-# SPECIALIZE NOINLINE prettyTCM :: (PrettyTCM n, PrettyTCMWithNode e) => (Graph n e) -> TCM Doc #-}

    instance PrettyTCM SplitTag where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitTag -> m Doc
    prettyTCM (SplitCon QName
    c)  = QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    c
      prettyTCM (SplitLit Literal
    l)  = Literal -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Literal -> m Doc
    prettyTCM Literal
    l
      prettyTCM SplitTag
    SplitCatchall = Doc -> m Doc
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc
    forall a. Underscore a => a
    underscore
    {-# SPECIALIZE prettyTCM :: SplitTag -> TCM Doc #-}

    instance PrettyTCM Candidate where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    prettyTCM Candidate
    c = case Candidate -> CandidateKind
    candidateKind Candidate
    c of
        (GlobalCandidate QName
    q) -> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
        CandidateKind
    LocalCandidate      -> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Term -> m Doc) -> Term -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Candidate -> Term
    candidateTerm Candidate
    c
    {-# SPECIALIZE prettyTCM :: Candidate -> TCM Doc #-}

    instance PrettyTCM Key where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Key -> m Doc
    prettyTCM = \case
        RigidK QName
    q Int
    a -> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> Int -> m Doc
    forall (m :: * -> *). Applicative m => Int -> m Doc
    superscript Int
    a
        LocalK Int
    i Int
    a -> m Doc
    "@" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> Int -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Int
    i m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> Int -> m Doc
    forall (m :: * -> *). Applicative m => Int -> m Doc
    superscript Int
    a
        PiK Hiding
    h      -> m Doc
    "Pi" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Hiding -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Hiding
    h
        Key
    ConstK     -> m Doc
    "Const"
        Key
    SortK      -> m Doc
    "Sort"
        Key
    FlexK      -> m Doc
    "_"
    {-# SPECIALIZE prettyTCM :: Key -> TCM Doc #-}

    instance PrettyTCM a => PrettyTCM (DiscrimTree a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
    prettyTCM = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc)
    -> (DiscrimTree a -> [m Doc]) -> DiscrimTree a -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m Doc -> DiscrimTree a -> [m Doc]
    forall {m :: * -> *} {a}.
    (IsString (m Doc), PrettyTCM a, MonadFresh NameId m,
     MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
     Null (m Doc), Semigroup (m Doc)) =>
    m Doc -> DiscrimTree a -> [m Doc]
    go m Doc
    "  " where
        go :: m Doc -> DiscrimTree a -> [m Doc]
    go m Doc
    ind DiscrimTree a
    EmptyDT     = [m Doc
    "fail"]
        go m Doc
    ind (DoneDT Set a
    it) = [m Doc
    "done" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Set a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Set a -> m Doc
    prettyTCM Set a
    it]
        go m Doc
    ind (CaseDT Int
    var Map Key (DiscrimTree a)
    branches DiscrimTree a
    fallthrough) =
          [m Doc
    "case" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Int -> m Doc
    prettyTCM Int
    var m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "of"]
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ ((Key, DiscrimTree a) -> [m Doc])
    -> [(Key, DiscrimTree a)] -> [m Doc]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\(Key
    k, DiscrimTree a
    v) -> m Doc -> m Doc -> DiscrimTree a -> [m Doc]
    abduct m Doc
    ind (Key -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Key -> m Doc
    prettyTCM Key
    k m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    " →") DiscrimTree a
    v) (Map Key (DiscrimTree a) -> [(Key, DiscrimTree a)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Key (DiscrimTree a)
    branches)
          [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ (Bool -> [()]
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (DiscrimTree a -> Bool
    forall a. Null a => a -> Bool
    null DiscrimTree a
    fallthrough)) [()] -> [m Doc] -> [m Doc]
    forall a b. [a] -> [b] -> [b]
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> m Doc -> m Doc -> DiscrimTree a -> [m Doc]
    abduct m Doc
    ind (m Doc
    "* →") DiscrimTree a
    fallthrough)

        abduct :: m Doc -> m Doc -> DiscrimTree a -> [m Doc]
    abduct m Doc
    ind m Doc
    f DiscrimTree a
    v | (m Doc
    l:[m Doc]
    ls) <- m Doc -> DiscrimTree a -> [m Doc]
    go m Doc
    ind DiscrimTree a
    v = ((m Doc
    ind m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    f) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    l)m Doc -> [m Doc] -> [m Doc]
    forall a. a -> [a] -> [a]
    :(m Doc -> m Doc) -> [m Doc] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (m Doc
    ind m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <>) [m Doc]
    ls
        abduct m Doc
    ind m Doc
    _ DiscrimTree a
    _ = [m Doc]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    {-# SPECIALIZE prettyTCM :: PrettyTCM a => DiscrimTree a -> TCM Doc #-}