    module Agda.TypeChecking.Pretty.Constraint where

    import Prelude hiding (null)

    import qualified Data.Set as Set
    import Data.Foldable (Foldable)
    import qualified Data.Foldable as Foldable
    import qualified Data.List as List
    import Data.Function (on)

    import Control.Monad

    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.Syntax.Common.Pretty as P
    import Agda.Utils.Impossible

    {-# SPECIALIZE prettyConstraint :: ProblemConstraint -> TCM Doc #-}
    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' TCState Bool -> (Bool -> Bool) -> m Doc -> m Doc
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    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
    forall (m :: * -> *). MonadPretty m => ProblemConstraint -> 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
    forall (m :: * -> *). MonadPretty m => Range -> m Doc
    prettyTCM Range
    r m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "]")

    {-# SPECIALIZE interestingConstraint :: ProblemConstraint -> TCM Bool #-}
    interestingConstraint :: MonadPretty m => ProblemConstraint -> m Bool
    interestingConstraint :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Bool
    interestingConstraint ProblemConstraint
    pc =
      case Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    pc) of
        UnBlock MetaId
    m -> MetaId -> m MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    m m MetaInstantiation -> (MetaInstantiation -> m Bool) -> m Bool
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          PostponedTypeCheckingProblem Closure TypeCheckingProblem
    cl -> Closure TypeCheckingProblem
    -> (TypeCheckingProblem -> m Bool) -> m Bool
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure TypeCheckingProblem
    cl \case
            DisambiguateConstructor{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            TypeCheckingProblem
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          MetaInstantiation
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Constraint
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

    {-# SPECIALIZE prettyInterestingConstraints :: [ProblemConstraint] -> TCM [Doc] #-}
    prettyInterestingConstraints :: MonadPretty m => [ProblemConstraint] -> m [Doc]
    prettyInterestingConstraints :: forall (m :: * -> *).
    MonadPretty m =>
    [ProblemConstraint] -> m [Doc]
    prettyInterestingConstraints [ProblemConstraint]
    cs = do
      cs' <- (ProblemConstraint -> m Bool)
    -> [ProblemConstraint] -> m [ProblemConstraint]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM ProblemConstraint -> m Bool
    forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Bool
    interestingConstraint [ProblemConstraint]
    cs
      let
        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
        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 (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
      mapM (prettyConstraint . stripPids) $ List.sortBy (compare `on` isBlocked) cs'

    prettyRangeConstraint ::
      (MonadPretty m, Foldable f, Null (f ProblemId)) => Range -> f ProblemId -> Blocker -> Doc -> m Doc
    prettyRangeConstraint :: forall (m :: * -> *) (f :: * -> *).
    (MonadPretty m, Foldable f, Null (f ProblemId)) =>
    Range -> f ProblemId -> Blocker -> Doc -> m Doc
    prettyRangeConstraint Range
    r f ProblemId
    pids Blocker
    unblock Doc
    c =
      Doc -> m Doc
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc
    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
    sep [ Range -> m Doc
    forall {a} {f :: * -> *}. (Pretty a, Applicative f) => a -> f Doc
    prange Range
    r
          , m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parensNonEmpty (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
              [ Blocker -> m Doc
    blockedOn Blocker
    unblock
              , [ProblemId] -> m Doc
    forall {m :: * -> *} {a}.
    (Null (m Doc), IsString (m Doc), PrettyTCM a, MonadFresh NameId m,
     MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
     Semigroup (m Doc)) =>
    [a] -> m Doc
    prPids (f ProblemId -> [ProblemId]
    forall a. f a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Foldable.toList f 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
    forall (m :: * -> *). 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
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM [a]
    pids)

      comma :: m Doc
    comma | f ProblemId -> Bool
    forall a. Null a => a -> Bool
    null f 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
    forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM Blocker
    u m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    comma)

      prange :: a -> f Doc
    prange a
    r | String -> Bool
    forall a. Null a => a -> Bool
    null String
    s    = Doc -> f Doc
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc
    forall a. Null a => a
    empty
               | Bool
    otherwise = String -> f Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> f Doc) -> String -> f Doc
    forall a b. (a -> b) -> a -> b
    $ String
    " [ at " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ]"
        where s :: String
    s = a -> String
    forall a. Pretty a => a -> String
    P.prettyShow a
    r

    instance PrettyTCM ProblemConstraint where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
    prettyTCM (PConstr Set ProblemId
    pids Blocker
    unblock Closure Constraint
    c) =
        Range -> Set ProblemId -> Blocker -> Doc -> m Doc
    forall (m :: * -> *) (f :: * -> *).
    (MonadPretty m, Foldable f, Null (f ProblemId)) =>
    Range -> f ProblemId -> Blocker -> Doc -> m Doc
    prettyRangeConstraint Range
    forall a. Range' a
    noRange Set ProblemId
    pids Blocker
    unblock (Doc -> m Doc) -> m Doc -> m Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Closure Constraint -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Closure Constraint -> m Doc
    prettyTCM Closure Constraint
    c

    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
    forall (m :: * -> *). MonadPretty m => Comparison -> 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
    forall (m :: * -> *). MonadPretty m => CompareAs -> 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Comparison -> 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
    forall (m :: * -> *). MonadPretty m => Comparison -> 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
    forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
    prettyTCM Comparison
    cmp) Sort
    s1 Sort
    s2
            UnBlock MetaId
    m   -> do
                MetaId -> m MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    m m MetaInstantiation -> (MetaInstantiation -> m Doc) -> m Doc
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                  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 :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    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
                  OpenMeta{}  -> 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 Range
    _ MetaId
    m Maybe [Candidate]
    mcands -> do
              t <- MetaId -> m Type
    forall (m :: * -> *).
    (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
     MonadTCEnv m, ReadTCState m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    m
              TelV tel _ <- telViewUpTo' (-1) notVisible t
              sep [ "Resolve instance argument" <?> prettyCmp ":" m 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.
                  , addContext tel cands
                  ]
              where
                overlap :: Candidate -> a
    overlap Candidate
    c = case Candidate -> OverlapMode
    candidateOverlap Candidate
    c of
                  OverlapMode
    FieldOverlap   -> a
    "overlap"
                  OverlapMode
    Incoherent     -> a
    "[incoherent]"
                  OverlapMode
    Overlappable   -> a
    "[overlappable]"
                  OverlapMode
    Overlapping    -> a
    "[overlapping]"
                  OverlapMode
    Overlaps       -> a
    "[overlaps]"
                  OverlapMode
    DefaultOverlap -> a
    forall a. Null a => a
    empty

                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 {a}. (IsString a, Null a) => Candidate -> a
    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
    forall (m :: * -> *). MonadPretty m => Candidate -> 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Candidate -> Type
    candidateType Candidate
    c)
                    | Candidate
    c <- [Candidate]
    cnds
                    ]

            ResolveInstanceHead QName
    q ->
                m Doc
    "Resolve target type of instance: " 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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
            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 DefInfo
    i QName
    q [Clause]
    cs TCErr
    err -> do
                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
                vcat [ "Check definition of" <+> prettyTCM q <+> ":" <+> prettyTCM t
                     , nest 2 $ "stuck because" <?> prettyTCM 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
    forall (m :: * -> *). MonadPretty m => Sort -> 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 String
    _ Sort
    b -> (Dom Type, Sort) -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => (Dom Type, Sort) -> m Doc
    prettyTCM (Dom Type
    a,Sort
    b)
              Abs String
    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
    forall (m :: * -> *). MonadPretty m => Dom Type -> 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
    <+> 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 String
    x (Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> 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
              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.Unquote A.exprNoRange) (defaultNamedArg e))
            CheckDataSort QName
    q Sort
    s -> do
              [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ m Doc
    "Sort", Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM Sort
    s, m Doc
    "of", 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
    "admits data/record definitions." ]
            CheckMetaInst MetaId
    x -> do
              m <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x
              case mvJudgement 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
    forall (m :: * -> *). MonadPretty m => MetaId -> 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
                IsSort{} -> MetaId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    forall (m :: * -> *). MonadPretty m => Arg Term -> 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    ty
            UsableAtModality WhyCheckModality
    _ Maybe Sort
    ms 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
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Modality -> String
    forall a. Verbalize a => a -> String
    verbalize Modality
    mod) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "modality:" 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
    t
              -- TODO: print @ms : Maybe Sort@ as well?

          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)