    module Agda.TypeChecking.Pretty.Constraint where

    import Prelude hiding (null)

    import qualified Data.Set as Set
    import qualified Data.List as List
    import Data.Function

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Info     as A
    import Agda.Syntax.Fixity
    import Agda.Syntax.Translation.InternalToAbstract
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Null
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Impossible

    prettyConstraint :: MonadPretty m => ProblemConstraint -> m Doc
    prettyConstraint :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
    prettyConstraint ProblemConstraint
    c = m Doc -> m Doc
    forall (m :: * -> *). MonadPretty m => m Doc -> m Doc
    f (Lens' Bool TCState -> (Bool -> Bool) -> m Doc -> m Doc
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' Bool TCState
    stInstantiateBlocking (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ ProblemConstraint -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ProblemConstraint
    c)
      where
        r :: Range
    r   = ProblemConstraint -> Range
    forall a. HasRange a => a -> Range
    getRange ProblemConstraint
    c
        f :: MonadPretty m => m Doc -> m Doc
        f :: forall (m :: * -> *). MonadPretty m => m Doc -> m Doc
    f m Doc
    d = if Doc -> Bool
    forall a. Null a => a -> Bool
    null (Doc -> Bool) -> Doc -> Bool
    forall a b. (a -> b) -> a -> b
    $ Range -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty Range
    r
              then m Doc
    d
              else m Doc
    d m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    4 (m Doc
    "[ at" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Range -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Range
    r m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "]")

    interestingConstraint :: ProblemConstraint -> Bool
    interestingConstraint :: ProblemConstraint -> Bool
    interestingConstraint ProblemConstraint
    pc = Constraint -> Bool
    go (Constraint -> Bool) -> Constraint -> Bool
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    pc)
      where
        go :: Constraint -> Bool
    go UnBlock{} = Bool
    False
        go Constraint
    _         = Bool
    True

    prettyInterestingConstraints :: MonadPretty m => [ProblemConstraint] -> m [Doc]
    prettyInterestingConstraints :: forall (m :: * -> *).
    MonadPretty m =>
    [ProblemConstraint] -> m [Doc]
    prettyInterestingConstraints [ProblemConstraint]
    cs = (ProblemConstraint -> m Doc) -> [ProblemConstraint] -> m [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (ProblemConstraint -> m Doc
    forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
    prettyConstraint (ProblemConstraint -> m Doc)
    -> (ProblemConstraint -> ProblemConstraint)
    -> ProblemConstraint
    -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> ProblemConstraint
    stripPids) ([ProblemConstraint] -> m [Doc]) -> [ProblemConstraint] -> m [Doc]
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> ProblemConstraint -> Ordering)
    -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Bool -> Bool -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Bool -> Bool -> Ordering)
    -> (ProblemConstraint -> Bool)
    -> ProblemConstraint
    -> ProblemConstraint
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` ProblemConstraint -> Bool
    isBlocked) [ProblemConstraint]
    cs'
      where
        isBlocked :: ProblemConstraint -> Bool
    isBlocked = Bool -> Bool
    not (Bool -> Bool)
    -> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set ProblemId -> Bool
    forall a. Null a => a -> Bool
    null (Set ProblemId -> Bool)
    -> (ProblemConstraint -> Set ProblemId)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> Set ProblemId
    allBlockingProblems (Blocker -> Set ProblemId)
    -> (ProblemConstraint -> Blocker)
    -> ProblemConstraint
    -> Set ProblemId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker
        cs' :: [ProblemConstraint]
    cs' = (ProblemConstraint -> Bool)
    -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ProblemConstraint -> Bool
    interestingConstraint [ProblemConstraint]
    cs
        interestingPids :: Set ProblemId
    interestingPids = [Set ProblemId] -> Set ProblemId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set ProblemId] -> Set ProblemId)
    -> [Set ProblemId] -> Set ProblemId
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> Set ProblemId)
    -> [ProblemConstraint] -> [Set ProblemId]
    forall a b. (a -> b) -> [a] -> [b]
    map (Blocker -> Set ProblemId
    allBlockingProblems (Blocker -> Set ProblemId)
    -> (ProblemConstraint -> Blocker)
    -> ProblemConstraint
    -> Set ProblemId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker) [ProblemConstraint]
    cs'
        stripPids :: ProblemConstraint -> ProblemConstraint
    stripPids (PConstr Set ProblemId
    pids Blocker
    unblock Closure Constraint
    c) = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
    forall a. Ord a => Set a -> Set a -> Set a
    Set.intersection Set ProblemId
    pids Set ProblemId
    interestingPids) Blocker
    unblock Closure Constraint
    c

    instance PrettyTCM ProblemConstraint where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
    prettyTCM (PConstr Set ProblemId
    pids Blocker
    unblock Closure Constraint
    c) = Closure Constraint -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Closure Constraint
    c m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parensNonEmpty ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [Blocker -> m Doc
    blockedOn Blocker
    unblock, [ProblemId] -> m Doc
    forall {m :: * -> *} {a}.
    (Null (m Doc), IsString (m Doc), PrettyTCM a, PureTCM m,
     MonadInteractionPoints m, MonadFresh NameId m,
     MonadStConcreteNames m, Semigroup (m Doc)) =>
    [a] -> m Doc
    prPids (Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList Set ProblemId
    pids)])
        where
          prPids :: [a] -> m Doc
    prPids []    = m Doc
    forall a. Null a => a
    empty
          prPids [a
    pid] = m Doc
    "belongs to problem" 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
    prettyTCM a
    pid
          prPids [a]
    pids  = m Doc
    "belongs to problems" 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 (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
    $ (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
    prettyTCM [a]
    pids)

          comma :: m Doc
    comma | Set ProblemId -> Bool
    forall a. Null a => a -> Bool
    null Set ProblemId
    pids = m Doc
    forall a. Null a => a
    empty
                | Bool
    otherwise = m Doc
    ","

          blockedOn :: Blocker -> m Doc
    blockedOn (UnblockOnAll Set Blocker
    bs) | Set Blocker -> Bool
    forall a. Set a -> Bool
    Set.null Set Blocker
    bs = m Doc
    forall a. Null a => a
    empty
          blockedOn (UnblockOnAny Set Blocker
    bs) | Set Blocker -> Bool
    forall a. Set a -> Bool
    Set.null Set Blocker
    bs = m Doc
    "stuck" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    comma
          blockedOn Blocker
    u = m Doc
    "blocked on" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Blocker -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Blocker
    u m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    comma)

    instance PrettyTCM Constraint where
        prettyTCM :: forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
    prettyTCM = \case
            ValueCmp Comparison
    cmp CompareAs
    ty Term
    s Term
    t -> m Doc -> Term -> Term -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp (Comparison -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Comparison
    cmp) Term
    s Term
    t m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> CompareAs -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM CompareAs
    ty
            ValueCmpOnFace Comparison
    cmp Term
    p Type
    ty Term
    s Term
    t ->
                [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    p m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "|"
                    , m Doc -> Term -> Term -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp (Comparison -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Comparison
    cmp) Term
    s Term
    t ]
                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
    <+> Precedence -> Type -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx Type
    ty)
            ElimCmp [Polarity]
    cmps [IsForced]
    fs Type
    t Term
    v [Elim]
    us [Elim]
    vs -> m Doc -> [Elim] -> [Elim] -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp m Doc
    "~~" [Elim]
    us [Elim]
    vs   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
    <+> Precedence -> Type -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx Type
    t)
            LevelCmp Comparison
    cmp Level
    a Level
    b         -> m Doc -> Level -> Level -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp (Comparison -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Comparison
    cmp) Level
    a Level
    b
            SortCmp Comparison
    cmp Sort
    s1 Sort
    s2        -> m Doc -> Sort -> Sort -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp (Comparison -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Comparison
    cmp) Sort
    s1 Sort
    s2
            UnBlock MetaId
    m   -> do
                -- BlockedConst t <- mvInstantiation <$> lookupMeta m
                MetaInstantiation
    mi <- MetaVariable -> MetaInstantiation
    mvInstantiation (MetaVariable -> MetaInstantiation)
    -> m MetaVariable -> m MetaInstantiation
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
                case MetaInstantiation
    mi of
                  BlockedConst Term
    t -> m Doc -> MetaId -> Term -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp m Doc
    ":=" MetaId
    m Term
    t
                  PostponedTypeCheckingProblem Closure TypeCheckingProblem
    cl -> Closure TypeCheckingProblem
    -> (TypeCheckingProblem -> m Doc) -> m Doc
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure TypeCheckingProblem
    cl ((TypeCheckingProblem -> m Doc) -> m Doc)
    -> (TypeCheckingProblem -> m Doc) -> m Doc
    forall a b. (a -> b) -> a -> b
    $ \TypeCheckingProblem
    p ->
                    m Doc -> MetaId -> TypeCheckingProblem -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp m Doc
    ":=" MetaId
    m TypeCheckingProblem
    p
                  Open{}  -> m Doc
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  OpenInstance{} -> m Doc
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  InstV{} -> m Doc
    forall a. Null a => a
    empty
                  -- Andreas, 2017-01-11, issue #2637:
                  -- The size solver instantiates some metas with infinity
                  -- without cleaning up the UnBlock constraints.
                  -- Thus, this case is not IMPOSSIBLE.
                  --
                  -- InstV args t -> do
                  --   reportS "impossible" 10
                  --     [ "UnBlock meta " ++ show m ++ " surprisingly has InstV instantiation:"
                  --     , show m ++ show args ++ " := " ++ show t
                  --     ]
                  --   __IMPOSSIBLE__
            FindInstance MetaId
    m Maybe [Candidate]
    mcands -> do
                Type
    t <- MetaId -> m Type
    forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
     HasBuiltins m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    m
                TelV Tele (Dom Type)
    tel Type
    _ <- Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
    telViewUpTo' (-Int
    1) Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Type
    t
                [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ m Doc
    "Resolve instance argument" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> m Doc -> MetaId -> Type -> m Doc
    forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp m Doc
    ":" MetaId
    m Type
    t
                      -- #4071: Non-visible arguments to the meta are in scope of the candidates add
                      --        those here to not get out of scope deBruijn indices when printing
                      --        unsolved constraints.
                    , Tele (Dom Type) -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel m Doc
    cands
                    ]
              where
                cands :: m Doc
    cands =
                  case Maybe [Candidate]
    mcands of
                    Maybe [Candidate]
    Nothing -> m Doc
    "No candidates yet"
                    Just [Candidate]
    cnds ->
                      m Doc -> Int -> m Doc -> m Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang m Doc
    "Candidates" 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 -> Int -> m Doc -> m Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang (Candidate -> m Doc
    forall {p}. (IsString p, Null p) => Candidate -> p
    overlap Candidate
    c m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Candidate -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":") Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $
                                Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Candidate -> Type
    candidateType Candidate
    c) | Candidate
    c <- [Candidate]
    cnds ]
                  where overlap :: Candidate -> p
    overlap Candidate
    c | Candidate -> Bool
    candidateOverlappable Candidate
    c = p
    "overlap"
                                  | Bool
    otherwise               = p
    forall a. Null a => a
    empty
            IsEmpty Range
    r Type
    t ->
                m Doc
    "Is empty:" 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
    t
            CheckSizeLtSat Term
    t ->
                m Doc
    "Is not empty type of sizes:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> Precedence -> Term -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx Term
    t
            CheckFunDef Delayed
    d DefInfo
    i QName
    q [Clause]
    cs TCErr
    err -> do
                Type
    t <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
                [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ m Doc
    "Check definition of" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 -> 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
    prettyTCM Type
    t
                     , 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
    "stuck because" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> TCErr -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM TCErr
    err ]
            HasBiggerSort Sort
    a -> m Doc
    "Has bigger sort:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    a
            HasPTSRule Dom Type
    a Abs Sort
    b -> m Doc
    "Has PTS rule:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> case Abs Sort
    b of
              NoAbs ArgName
    _ Sort
    b -> (Dom Type, Sort) -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Dom Type
    a,Sort
    b)
              Abs ArgName
    x Sort
    b   -> m Doc
    "(" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> (Dom Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    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
    <+> ArgName -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ArgName
    x (Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    b)) m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ")"
            UnquoteTactic Term
    v Term
    _ Type
    _ -> do
              Expr
    e <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    v
              Expr -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (AppInfo -> Expr -> NamedArg Expr -> Expr
    A.App AppInfo
    A.defaultAppInfo_ (ExprInfo -> Expr
    A.Unquote ExprInfo
    A.exprNoRange) (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    e))
            CheckMetaInst MetaId
    x -> do
              MetaVariable
    m <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
              case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    m of
                HasType{ jMetaType :: forall a. Judgement a -> Type
    jMetaType = Type
    t } -> MetaId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    x 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
    prettyTCM Type
    t
                IsSort{} -> MetaId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    x m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "is a sort"
            CheckType Type
    t ->
              Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "is a well-formed type"
            CheckLockedVars Term
    t Type
    ty Arg Term
    lk Type
    lk_ty -> do
              m Doc
    "Lock" 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
    prettyTCM Arg Term
    lk 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
    <+> Precedence -> Term -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx Term
    t 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
    prettyTCM Type
    ty
            UsableAtModality Modality
    mod Term
    t -> m Doc
    "Is usable at" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Modality -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Modality
    mod 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
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    t

          where
            prettyCmp
              :: (PrettyTCM a, PrettyTCM b, MonadPretty m)
              => m Doc -> a -> b -> m Doc
            prettyCmp :: forall a b (m :: * -> *).
    (PrettyTCM a, PrettyTCM b, MonadPretty m) =>
    m Doc -> a -> b -> m Doc
    prettyCmp m Doc
    cmp a
    x b
    y = Precedence -> a -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx a
    x m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> (m Doc
    cmp m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Precedence -> b -> m Doc
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    Precedence -> a -> m Doc
    prettyTCMCtx Precedence
    TopCtx b
    y)