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

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

interestingConstraint :: ProblemConstraint -> Bool
interestingConstraint :: ProblemConstraint -> Bool
interestingConstraint ProblemConstraint
pc = Constraint -> Bool
go forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyConstraint forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> ProblemConstraint
stripPids) forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Set ProblemId
allBlockingProblems forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker
    cs' :: [ProblemConstraint]
cs' = forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
interestingConstraint [ProblemConstraint]
cs
    interestingPids :: Set ProblemId
interestingPids = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Blocker -> Set ProblemId
allBlockingProblems 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 (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set ProblemId
pids Set ProblemId
interestingPids) Blocker
unblock Closure Constraint
c

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 =
  forall (m :: * -> *) a. Monad m => a -> m a
return Doc
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall {a} {f :: * -> *}. (Pretty a, Applicative f) => a -> f Doc
prange Range
r
      , forall (m :: * -> *). Functor m => m Doc -> m Doc
parensNonEmpty forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ Blocker -> m Doc
blockedOn Blocker
unblock
          , 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 (forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f ProblemId
pids)
          ]
      ]
  where
  prPids :: [a] -> m Doc
prPids []    = forall a. Null a => a
empty
  prPids [a
pid] = m Doc
"belongs to problem" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
pid
  prPids [a]
pids  = m Doc
"belongs to problems" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [a]
pids)

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

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

  prange :: a -> f Doc
prange a
r | forall a. Null a => a -> Bool
null String
s    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Null a => a
empty
           | Bool
otherwise = forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
" [ at " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" ]"
    where s :: String
s = 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) =
    forall (m :: * -> *) (f :: * -> *).
(MonadPretty m, Foldable f, Null (f ProblemId)) =>
Range -> f ProblemId -> Blocker -> Doc -> m Doc
prettyRangeConstraint forall a. Range' a
noRange Set ProblemId
pids Blocker
unblock forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 ->
            forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|"
                , forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t ]
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
"~~" [Elim]
us [Elim]
vs   forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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         -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Level
a Level
b
        SortCmp Comparison
cmp Sort
s1 Sort
s2        -> forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (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 <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
            case MetaInstantiation
mi of
              BlockedConst Term
t -> 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 -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl forall a b. (a -> b) -> a -> b
$ \TypeCheckingProblem
p ->
                forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":=" MetaId
m TypeCheckingProblem
p
              Open{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
              OpenInstance{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
              InstV{} -> 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 <- forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
            TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) forall a. LensHiding a => a -> Bool
notVisible Type
t
            forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"Resolve instance argument" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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.
                , 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 ->
                  forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang m Doc
"Candidates" Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                    [ forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (forall {a}. (IsString a, Null a) => Candidate -> a
overlap Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") Int
2 forall a b. (a -> b) -> a -> b
$
                            forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Candidate -> Type
candidateType Candidate
c) | Candidate
c <- [Candidate]
cnds ]
              where overlap :: Candidate -> a
overlap Candidate
c | Candidate -> Bool
candidateOverlappable Candidate
c = a
"overlap"
                              | Bool
otherwise               = forall a. Null a => a
empty
        IsEmpty Range
r Type
t ->
            m Doc
"Is empty:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
            forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ m Doc
"Check definition of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
                 , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ m Doc
"stuck because" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err ]
        HasBiggerSort Sort
a -> m Doc
"Has bigger sort:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> case Abs Sort
b of
          NoAbs String
_ Sort
b -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Dom Type
a,Sort
b)
          Abs String
x Sort
b   -> m Doc
"(" forall a. Semigroup a => a -> a -> a
<> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"," forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext String
x (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
b)) forall a. Semigroup a => a -> a -> a
<> m Doc
")"
        UnquoteTactic Term
v Term
_ Type
_ -> do
          Expr
e <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
          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) (forall a. a -> NamedArg a
defaultNamedArg Expr
e))
        CheckDataSort QName
q Sort
s -> do
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ m Doc
"Sort", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s, m Doc
"of", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q, m Doc
"admits data/record definitions." ]
        CheckMetaInst MetaId
x -> do
          MetaVariable
m <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
          case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m of
            HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            IsSort{} -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"is a sort"
        CheckType Type
t ->
          forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Term
lk forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty
        UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
mod Term
t -> m Doc
"Is usable at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Verbalize a => a -> String
verbalize Modality
mod) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"modality:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 = forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx a
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
cmp forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx b
y)