module Agda.TypeChecking.Pretty.Warning where

import Prelude hiding ( null )

import Control.Monad ( guard, filterM, forM, (<=<) )

import Data.Char ( toLower )
import qualified Data.Foldable as Fold
import Data.Function (on)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set  as Set
import qualified Data.Text as T

import Agda.TypeChecking.Monad.Base
import qualified Agda.TypeChecking.Monad.Base.Warning as W
import Agda.TypeChecking.Monad.Builtin
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Constraints
import Agda.TypeChecking.Monad.State ( getScope )
import Agda.TypeChecking.Monad ( localTCState, enterClosure )
import Agda.TypeChecking.Positivity () --instance only
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call () -- instance PrettyTCM CallInfo
import {-# SOURCE #-} Agda.TypeChecking.Pretty.Constraint (prettyInterestingConstraints, interestingConstraint)
import Agda.TypeChecking.Warnings (MonadWarning, isUnsolvedWarning, onlyShowIfUnsolved, classifyWarning, WhichWarnings(..), warning_)
import {-# SOURCE #-} Agda.TypeChecking.MetaVars

import Agda.Syntax.Common
  ( ImportedName'(..), fromImportedName, partitionImportedNames
  , IsOpaque(OpaqueDef, TransparentDef)
  , ProjOrigin(..)
  , getHiding
  )
import Agda.Syntax.Common.Pretty ( Pretty, prettyShow, singPlural )
import qualified Agda.Syntax.Common.Pretty as P
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base ( concreteNamesInScope, NameOrModule(..) )
import Agda.Syntax.Translation.InternalToAbstract

import Agda.Interaction.Options
import Agda.Interaction.Options.Errors
import Agda.Interaction.Options.Warnings

import Agda.Utils.FileName ( filePath )
import Agda.Utils.Functor  ( (<.>) )
import Agda.Utils.Lens
import Agda.Utils.List ( editDistance )
import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Singleton
import qualified Agda.Utils.Set1 as Set1

import Agda.Utils.Impossible

instance PrettyTCM TCWarning where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM w :: TCWarning
w@(TCWarning CallStack
loc Range
_ Warning
_ Doc
doc [Char]
_ Bool
_) = Doc
doc Doc -> m () -> m Doc
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
    [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"warning" VerboseLevel
2 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Warning raised at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CallStack -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc

{-# SPECIALIZE prettyWarning :: Warning -> TCM Doc #-}
prettyWarning :: MonadPretty m => Warning -> m Doc
prettyWarning :: forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning = \case

    UnsolvedMetaVariables Set1 Range
ms  ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved metas at the following locations:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (Range -> m Doc) -> List1 Range -> 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 Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (List1 Range -> NonEmpty (m Doc))
-> List1 Range -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 Range -> List1 Range
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 Range
ms)

    UnsolvedInteractionMetas Set1 Range
is ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved interaction metas at the following locations:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (Range -> m Doc) -> List1 Range -> 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 Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (List1 Range -> NonEmpty (m Doc))
-> List1 Range -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 Range -> List1 Range
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 Range
is)

    InteractionMetaBoundaries Set1 Range
is ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Interaction meta(s) at the following location(s) have unsolved boundary constraints:" )
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (Range -> m Doc) -> List1 Range -> 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 Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (List1 Range -> NonEmpty (m Doc))
-> List1 Range -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 Range -> List1 Range
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 Range
is)

    UnsolvedConstraints List1 ProblemConstraint
cs -> do
      pcs <- [ProblemConstraint] -> m [Doc]
forall (m :: * -> *).
MonadPretty m =>
[ProblemConstraint] -> m [Doc]
prettyInterestingConstraints ([ProblemConstraint] -> m [Doc]) -> [ProblemConstraint] -> m [Doc]
forall a b. (a -> b) -> a -> b
$ List1 ProblemConstraint -> [Item (List1 ProblemConstraint)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ProblemConstraint
cs
      if null pcs
        then fsep $ pwords "Unsolved constraints"  -- #4065: keep minimal warning text
        else vcat
          [ fsep $ pwords "Failed to solve the following constraints:"
          , nest 2 $ return $ P.vcat $ List.nub pcs
          ]

    TerminationIssue List1 TerminationError
because -> do
      dropTopLevel <- m (QName -> QName)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
      vcat
        [ fwords "Termination checking failed for the following functions:"
        , nest 2 $ fsep $ punctuate comma $
            map (pretty . dropTopLevel) $
              concatMap termErrFunctions because
        , fwords "Problematic calls:"
        , nest 2 $ fmap (P.vcat . List.nub) $
            mapM prettyTCM $ List.sortOn getRange $
              concatMap termErrCalls because
        ]

    UnreachableClauses QName
_f List1 Range
pss -> m Doc
"Unreachable" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> List1 Range -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 Range
pss m Doc
"clause"

    CoverageIssue QName
f List1 (Telescope, [NamedArg DeBruijnPattern])
pss -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Incomplete pattern matching for"
          , [ 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 a. Semigroup a => a -> a -> a
<> m Doc
"." ]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Missing cases:"
          ]
        , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Telescope, [NamedArg DeBruijnPattern]) -> m Doc)
-> List1 (Telescope, [NamedArg DeBruijnPattern])
-> 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 (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display List1 (Telescope, [NamedArg DeBruijnPattern])
pss
        ]
      where
        display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc) -> NamedClause -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> NamedClause) -> Clause -> NamedClause
forall a b. (a -> b) -> a -> b
$
          Clause
forall a. Null a => a
empty { clauseTel = tel, namedClausePats = ps }

    CoverageNoExactSplit QName
f List1 Clause
cs -> NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (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 ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Exact splitting is enabled, but the following" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ List1 Clause -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 Clause
cs m Doc
"clause" ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
            [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"could not be preserved as definitional equalities in the translation to a case tree:"
           ) m Doc -> NonEmpty (m Doc) -> NonEmpty (m Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<|
      (Clause -> m Doc) -> List1 Clause -> 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 (VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Clause -> m Doc) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True) List1 Clause
cs

    InlineNoExactSplit QName
f Clause
c -> [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
$
      [ [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
$
          [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Exact splitting is enabled, but the following clause" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
          [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is no longer a definitional equality because it was translated to a copattern match:"
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Clause -> m Doc) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> m Doc) -> Clause -> m Doc
forall a b. (a -> b) -> a -> b
$ Clause
c
      ]

    NotStrictlyPositive QName
d Seq OccursWhere
ocs -> [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
$
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not strictly positive, because it occurs"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Seq OccursWhere -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
prettyTCM Seq OccursWhere
ocs]

    ConstructorDoesNotFitInData QName
c Sort
s1 Sort
s2 TCErr
err -> m Doc
msg m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
      case TCErr
err of
        TypeError CallStack
_loc TCState
s Closure TypeError
e -> (TCState -> TCState) -> m Doc -> m Doc
forall a. (TCState -> TCState) -> m a -> m a
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> (TypeError -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
e \ TypeError
e ->
          m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc
"Reason:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM TypeError
e)
        TCErr
_ ->
          TCErr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
      where
        msg :: m Doc
msg = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ m Doc
"Constructor" 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
c
          , m Doc
"of 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
s1
          , (m Doc
"does not fit into data type of 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
s2) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."
          ]

    CoinductiveEtaRecord QName
name -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not switching on eta-equality for coinductive records."
      , [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"If you must, use pragma" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ m Doc
"{-# ETA", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name, m Doc
"#-}" ]
      ]

    UnsupportedIndexedMatch Doc
doc -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"This clause uses pattern-matching features that are not yet supported by Cubical Agda,"
           [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"the function to which it belongs will not compute when applied to transports."
             )
      , m Doc
""
      , m Doc
"Reason:" 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
doc
      , m Doc
""
      ]

    CantGeneralizeOverSorts Set1 MetaId
ms -> do
      rms <- [MetaId] -> (MetaId -> m (Range, MetaId)) -> m [(Range, MetaId)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Set1 MetaId -> [MetaId]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Set1 MetaId
ms) \ MetaId
x -> (,MetaId
x) (Range -> (Range, MetaId)) -> m Range -> m (Range, MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x
      vcat
            [ text "Cannot generalize over unsolved sort metas:"
            , nest 2 $ vcat [ prettyTCM x <+> text "at" <+> pretty r | (r,x) <- List.sort rms ]
            , fsep $ pwords "Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

    Warning
AbsurdPatternRequiresAbsentRHS -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"The right-hand side must be omitted if there " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"is an absurd pattern, () or {}, in the left-hand side."

    OldBuiltin BuiltinId
old BuiltinId
new -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"Builtin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
old [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" no longer exists. " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"It is now bound by BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
new

    BuiltinDeclaresIdentifier BuiltinId
b -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BuiltinId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" declares an identifier " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"(no longer expects an already defined identifier)"

    Warning
EmptyRewritePragma -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Empty REWRITE pragma"

    Warning
EmptyWhere         -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Empty `where' block (ignored)"

    -- TODO: linearity
    -- FixingQuantity s q q' -> fsep $ concat
    --   [ pwords "Replacing illegal quantity", [ pretty q ], pwords s, [ "by", pretty q' ] ]

    FixingRelevance [Char]
s Relevance
r Relevance
r' ->  [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Replacing illegal relevance", [ Relevance -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p Relevance
r ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
s, [ m Doc
"by", Relevance -> m Doc
forall {m :: * -> *} {a}.
(Applicative m, Verbalize a) =>
a -> m Doc
p Relevance
r' ]
      ]
      where p :: a -> m Doc
p a
r = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"`" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize a
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"

    IllformedAsClause [Char]
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([Char] -> [m Doc]) -> [Char] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"`as' must be followed by an identifier" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s

    ClashesViaRenaming NameOrModule
nm Set1 Name
xs -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
      [ [ case NameOrModule
nm of NameOrModule
NameNotModule -> m Doc
"Name"; NameOrModule
ModuleNotName -> m Doc
"Module" ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"clashes introduced by `renaming':"
      , (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM ([Name] -> [m Doc]) -> [Name] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set1 Name -> [Name]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Set1 Name
xs
      ]

    UselessPatternDeclarationForRecord [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
      [ [Char]
"`pattern' attribute ignored for", [Char]
s, [Char]
"record" ]
      -- the @s@ is a qualifier like "eta" or "coinductive"

    Warning
UselessPublic -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Keyword `public' is ignored here"

    UselessHiding List1 ImportedName
xs -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring names in `hiding' directive:"
      , m Doc -> NonEmpty (m Doc) -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," (NonEmpty (m Doc) -> [m Doc]) -> NonEmpty (m Doc) -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (ImportedName -> m Doc) -> List1 ImportedName -> 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 ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 ImportedName
xs
      ]

    UselessInline QName
q -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It is pointless for INLINE'd function" [m Doc] -> [m Doc] -> [m Doc]
forall 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
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to have a separate Haskell definition"

    Warning
WrongInstanceDeclaration -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instances should be of type {Γ} → C, where C evaluates to a postulated name or the name of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"a data or record type, so `instance' is ignored here."

    InstanceWithExplicitArg QName
q -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance declarations with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so making" [m Doc] -> [m Doc] -> [m Doc]
forall 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
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"into an instance has no effect."

    InstanceNoOutputTypeName Doc
b -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance arguments whose type is not {Γ} → C, where C evaluates to a postulated type, " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a parameter type or the name of a data or record type, are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has no effect."

    InstanceArgWithExplicitArg Doc
b -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Instance arguments with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so having an instance argument" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has no effect."

    InversionDepthReached QName
f -> do
      maxDepth <- m VerboseLevel
forall (m :: * -> *). HasOptions m => m VerboseLevel
maxInversionDepth
      fsep $ pwords "Refusing to invert pattern matching of" ++ [prettyTCM f] ++
             pwords ("because the maximum depth (" ++ show maxDepth ++ ") has been reached.") ++
             pwords "Most likely this means you have an unsatisfiable constraint, but it could" ++
             pwords "also mean that you need to increase the maximum depth using the flag" ++
             pwords "--inversion-max-depth=N"

    NoGuardednessFlag QName
q ->
      [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
$ [ 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. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared coinductive, but option" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"--guardedness is not enabled. Coinductive functions on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"this type will likely be rejected by the termination" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"checker unless this flag is enabled."

    InvalidCharacterLiteral Char
c -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Invalid character literal" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ Char -> [Char]
forall a. Show a => a -> [Char]
show Char
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(surrogate code points are not supported)"

    UselessPragma Range
_r Doc
d -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    SafeFlagPostulate Name
e -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot postulate" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with safe flag"

    SafeFlagPragma Set [Char]
sset -> [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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[Char]]
-> ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural ([Char] -> [[Char]]
words ([Char] -> [[Char]]) -> [[Char]] -> [[Char]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [[Char]]
xs) [Char] -> [Char]
forall a. a -> a
id ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s") [Char]
"The --safe mode does not allow OPTIONS pragma" ]
      , ([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [[Char]]
xs
      ]
      where xs :: [[Char]]
xs = Set [Char] -> [[Char]]
forall a. Set a -> [a]
Set.toAscList Set [Char]
sset

    Warning
SafeFlagWithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot use primEraseEquality with safe and without-K flags.")

    Warning
WithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Using primEraseEquality with the without-K flag is inconsistent.")

    ConflictingPragmaOptions [Char]
a [Char]
b -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
      [ [Char]
"Conflicting options", [Char] -> [Char]
yes [Char]
a, [Char]
"and", [Char] -> [Char]
no [Char]
b, [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
yes [Char]
a, [Char]
"implies", [Char] -> [Char]
yes [Char]
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")."
      , [Char]
"Ignoring", [Char] -> [Char]
no [Char]
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"." ]
      where
        yes :: [Char] -> [Char]
yes [Char]
s = [Char]
"--" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
        no :: [Char] -> [Char]
no (Char
'n' : Char
'o' : Char
'-' : [Char]
s) = [Char]
"--" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
        no [Char]
s                     = [Char]
"--no-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s

    OptionWarning OptionWarning
ow -> OptionWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OptionWarning
ow

    ParseWarning ParseWarning
pw -> ParseWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ParseWarning
pw

    DuplicateInterfaceFiles AbsolutePath
selected AbsolutePath
ignored -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"There are two interface files:"
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
selected
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
ignored
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Using" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
selected] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"for now but please remove at least one of them."
      ]

    DeprecationWarning [Char]
old [Char]
new [Char]
version -> [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
$
      [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
old] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has been deprecated. Use" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
new] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
      [Char]
"instead. This will be an error in Agda" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
version m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    NicifierIssue DeclarationWarning
w -> DeclarationWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeclarationWarning
w

    UserWarning BackendName
str -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (BackendName -> [Char]
T.unpack BackendName
str)

    ModuleDoesntExport QName
m [Name]
names [Name]
modules List1 ImportedName
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"doesn't export the following:"
      , Bool -> (ImportedName -> m Doc) -> [ImportedName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False ([Name] -> ImportedName -> m Doc
forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
names)   [ImportedName]
ys
      , Bool -> (ImportedName -> m Doc) -> [ImportedName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False ([Name] -> ImportedName -> m Doc
forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
modules) [ImportedName]
ms
      ]
      where
      ys, ms :: [C.ImportedName]
      ys :: [ImportedName]
ys            = (Name -> ImportedName) -> [Name] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ImportedName
forall n m. n -> ImportedName' n m
ImportedName   [Name]
ys0
      ms :: [ImportedName]
ms            = (Name -> ImportedName) -> [Name] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule [Name]
ms0
      ([Name]
ys0, [Name]
ms0)    = [ImportedName] -> ([Name], [Name])
forall n m. [ImportedName' n m] -> ([n], [m])
partitionImportedNames ([ImportedName] -> ([Name], [Name]))
-> [ImportedName] -> ([Name], [Name])
forall a b. (a -> b) -> a -> b
$ List1 ImportedName -> [Item (List1 ImportedName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ImportedName
xs
      suggestion :: [Name] -> ImportedName' b b -> m Doc
suggestion [Name]
zs = m Doc -> (m Doc -> m Doc) -> Maybe (m Doc) -> m Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Doc
forall a. Null a => a
empty m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Maybe (m Doc) -> m Doc)
-> (ImportedName' b b -> Maybe (m Doc))
-> ImportedName' b b
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName]
-> (ImportedName' b b -> b) -> ImportedName' b b -> Maybe (m Doc)
forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean ((Name -> QName) -> [Name] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> QName
C.QName [Name]
zs) ImportedName' b b -> b
forall a. ImportedName' a a -> a
fromImportedName

    DuplicateUsing List1 ImportedName
xs -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicates in `using` directive:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 ImportedName -> [Item (List1 ImportedName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 ImportedName
xs)

    FixityInRenamingModule List1 Range
_rs -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Modules do not have fixity"

    LibraryWarning LibWarning
lw -> LibWarning -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty LibWarning
lw

    InfectiveImport Doc
msg -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg

    CoInfectiveImport Doc
msg -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg

    NotARewriteRule QName
x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a legal rewrite rule, since the left-hand side is"
        , case IsAmbiguous
amb of
            YesAmbiguous AmbiguousQName
xs -> [ m Doc
"ambiguous:", AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
            IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"neither a defined symbol nor a constructor"
        ]

    IllegalRewriteRule QName
q IllegalRewriteRuleReason
reason -> case IllegalRewriteRuleReason
reason of
      IllegalRewriteRuleReason
LHSNotDefinitionOrConstructor -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
      VariablesNotBoundByLHS IntSet
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the following variables are not bound by the left hand side: "
        , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((VerboseLevel -> m Doc) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (VerboseLevel -> Term) -> VerboseLevel -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Term
var) ([VerboseLevel] -> [m Doc]) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ IntSet -> [VerboseLevel]
IntSet.toList IntSet
xs)
        ]
      VariablesBoundMoreThanOnce IntSet
xs -> do
        (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
" is not a legal rewrite rule, since the following parameters are bound more than once on the left hand side: "
          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
hsep (m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
List.intersperse m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> m Doc) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (VerboseLevel -> Term) -> VerboseLevel -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Term
var) ([VerboseLevel] -> [m Doc]) -> [VerboseLevel] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ IntSet -> [VerboseLevel]
IntSet.toList IntSet
xs))
          m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
". Perhaps you can use a postulate instead of a constructor as the head symbol?"
      LHSReduces Term
v Term
v' -> [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 m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" is not a legal rewrite rule, since the left-hand side "
        , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" reduces to " 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' ]
      HeadSymbolIsProjectionLikeFunction QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the head symbol"
        , m Doc
hd , m Doc
"is a projection-like function."
        , m Doc
"You can turn off the projection-like optimization for", m Doc
hd
        , m Doc
"with the pragma {-# NOT_PROJECTION_LIKE", m Doc
hd, m Doc
"#-}"
        , m Doc
"or globally with the flag --no-projection-like"
        ]
        where hd :: m Doc
hd = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
      HeadSymbolIsTypeConstructor QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since the head symbol"
        , 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
"is a type constructor."
        ]
      HeadSymbolContainsMetas QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
"is not a legal rewrite rule, since the definition of the head symbol"
        , 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
"contains unsolved metavariables and confluence checking is enabled."
        ]
      ConstructorParametersNotGeneral ConHead
c Args
vs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ 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
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" is not a legal rewrite rule, since the constructor parameters are not fully general:"
        , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Constructor: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
        , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Parameters: " 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
prettyList ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
vs)
        ]
      ContainsUnsolvedMetaVariables Set1 MetaId
ms -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since"
        , m Doc
"it contains the unsolved meta variable(s)", NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((MetaId -> m Doc) -> NonEmpty MetaId -> 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 MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM (NonEmpty MetaId -> NonEmpty (m Doc))
-> NonEmpty MetaId -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 MetaId -> NonEmpty MetaId
forall a. NESet a -> NonEmpty a
Set1.toList Set1 MetaId
ms)
        ]
      BlockedOnProblems Set1 ProblemId
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since"
        , m Doc
"it is blocked on problem(s)", NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((ProblemId -> m Doc) -> NonEmpty ProblemId -> 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 ProblemId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemId -> m Doc
prettyTCM (NonEmpty ProblemId -> NonEmpty (m Doc))
-> NonEmpty ProblemId -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 ProblemId -> NonEmpty ProblemId
forall a. NESet a -> NonEmpty a
Set1.toList Set1 ProblemId
ps)
        ]
      RequiresDefinitions Set1 QName
qs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" is not a legal rewrite rule, since"
        , m Doc
"it requires the definition(s) of", NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((QName -> m Doc) -> NonEmpty QName -> 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 QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (NonEmpty QName -> NonEmpty (m Doc))
-> NonEmpty QName -> NonEmpty (m Doc)
forall a b. (a -> b) -> a -> b
$ Set1 QName -> NonEmpty QName
forall a. NESet a -> NonEmpty a
Set1.toList Set1 QName
qs)
        ]
      IllegalRewriteRuleReason
DoesNotTargetRewriteRelation -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ 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
" does not target rewrite relation" ]
      IllegalRewriteRuleReason
BeforeFunctionDefinition -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ m Doc
"Rewrite rule from function "
        , 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
" cannot be added before the function definition"
        ]
      BeforeMutualFunctionDefinition QName
r -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ m Doc
"Rewrite rule from function "
        , 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
" cannot be added before the definition of mutually defined"
        , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r
        ]
      IllegalRewriteRuleReason
DuplicateRewriteRule ->
        m Doc
"Rewrite rule " 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 m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" has already been added"

    ConfluenceCheckingIncompleteBecauseOfMeta QName
f -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"Confluence checking incomplete because the definition of"
      , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
      , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"contains unsolved metavariables."
      ]

    Warning
ConfluenceForCubicalNotSupported -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
      [Char]
"Confluence checking for --cubical is not yet supported, confluence checking might be incomplete"

    RewriteNonConfluent Term
lhs Term
rhs1 Term
rhs2 Doc
err -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"Local confluence check failed:"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs , m Doc
"reduces to both"
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs1 , m Doc
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs2
      , m Doc
"which are not equal because"
      , Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
err
      ]

    RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
cs -> [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
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Couldn't determine overlap between left-hand sides"
          , [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs1 , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs2 ]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because of unsolved constraints:"
          ]
        ]
      , (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> (Doc -> m Doc) -> Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return) [Doc]
cs
      ]

    RewriteAmbiguousRules Term
lhs Term
rhs1 Term
rhs2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ ( [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Global confluence check failed:" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can be rewritten to either" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs1]
          , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"or" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs2 m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> 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] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible fix: add a rewrite rule with left-hand side"
        , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to resolve the ambiguity."
        ]
      ]

    RewriteMissingRule Term
u Term
v Term
rhou -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Global confluence check failed:" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unfolds to" , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which should further unfold to"
        , [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhou] , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but it does not."
        ]
      , [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible fix: add a rule to rewrite"
        , [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v , m Doc
"to" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhou ]
        ]
      ]

    DuplicateRecordDirective RecordDirective
dir ->
      m Doc
"Ignoring duplicate record directive: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> RecordDirective -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty RecordDirective
dir

    PragmaCompileErased BackendName
bn QName
qn -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The backend"
      , [ BackendName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => BackendName -> m Doc
prettyTCM BackendName
bn
        , m Doc
"erases"
        , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn
        ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"so the COMPILE pragma will be ignored."
      ]

    Warning
PragmaCompileList -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
      [Char]
"Ignoring GHC pragma for builtin lists; they always compile to Haskell lists."

    Warning
PragmaCompileMaybe -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords
      [Char]
"Ignoring GHC pragma for builtin MAYBE; it always compiles to Haskell Maybe."

    PragmaCompileUnparsable [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Ignoring unparsable GHC pragma '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"

    PragmaCompileWrong QName
_x [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
s

    PragmaCompileWrongName QName
x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot COMPILE"
      , [ QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"since it is"
      , case IsAmbiguous
amb of
          YesAmbiguous AmbiguousQName
xs -> [ m Doc
"ambiguous:", AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
          IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"neither a defined symbol nor a constructor"
      ]

    PragmaExpectsDefinedSymbol [Char]
pragma QName
_x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Target of"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma should be a defined symbol"
      ]

    PragmaExpectsUnambiguousConstructorOrFunction [Char]
pragma QName
_x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Target of"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma should be"
      , case IsAmbiguous
amb of
          YesAmbiguous AmbiguousQName
xs -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unambiguous, but it resolves to:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
          IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function, constructor, or projection"
      ]

    PragmaExpectsUnambiguousProjectionOrFunction [Char]
pragma QName
_x IsAmbiguous
amb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Target of"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma ]
      , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma should be"
      , case IsAmbiguous
amb of
          YesAmbiguous AmbiguousQName
xs -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unambiguous, but it resolves to:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ AmbiguousQName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty AmbiguousQName
xs ]
          IsAmbiguous
NotAmbiguous -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function or projection"
      ]

    NoMain TopLevelModuleName
topLevelModule -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No main function defined in" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
prettyTCM TopLevelModuleName
topLevelModule m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> 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] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Use option --no-main to suppress this warning."
      ]

    NotInScopeW QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not in scope:"
      , do
        inscope <- Set QName -> [QName]
forall a. Set a -> [a]
Set.toList (Set QName -> [QName])
-> (ScopeInfo -> Set QName) -> ScopeInfo -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set QName
concreteNamesInScope (ScopeInfo -> [QName]) -> m ScopeInfo -> m [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
        prettyNotInScopeNames True (suggestion inscope) $ singleton x
      ]
      where
      suggestion :: [QName] -> QName -> m Doc
suggestion [QName]
inscope QName
x = VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall {m :: * -> *}.
(Null (m Doc), Applicative m) =>
[m Doc] -> m Doc
par ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ m Doc
"did you forget space around the ':'?"  | Char
':' Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char]
s ]
        , [ m Doc
"did you forget space around the '->'?" | [Char]
"->" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isInfixOf` [Char]
s ]
        , Maybe (m Doc) -> [m Doc]
forall a. Maybe a -> [a]
maybeToList (Maybe (m Doc) -> [m Doc]) -> Maybe (m Doc) -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [QName] -> (QName -> Name) -> QName -> Maybe (m Doc)
forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope QName -> Name
C.unqualify QName
x
        ]
        where
        par :: [m Doc] -> m Doc
par []  = m Doc
forall a. Null a => a
empty
        par [m Doc
d] = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
d
        par [m Doc]
ds  = 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
vcat [m Doc]
ds
        s :: [Char]
s = QName -> [Char]
forall a. Pretty a => a -> [Char]
P.prettyShow QName
x

    AsPatternShadowsConstructorOrPatternSynonym ConstructorOrPatternSynonym
patsyn -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Name bound in @-pattern ignored because it shadows a"
      , [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ConstructorOrPatternSynonym -> Doc
forall a. Pretty a => a -> Doc
P.pretty ConstructorOrPatternSynonym
patsyn ]
      ]

    PatternShadowsConstructor Name
x QName
c -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The pattern variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has the same name as the constructor" [m Doc] -> [m Doc] -> [m Doc]
forall 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
c]

    PlentyInHardCompileTimeMode QωOrigin
o -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignored use of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QωOrigin -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QωOrigin
o] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in hard compile-time mode"

    RecordFieldWarning RecordFieldWarning
w -> RecordFieldWarning -> m Doc
forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning RecordFieldWarning
w

    MissingTypeSignatureForOpaque QName
name IsOpaque
isOpaque -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ m Doc
"Missing type signature for" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
what m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"definition" 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
name m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> 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] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
            [Char]
"Types of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" definitions are never inferred since this would leak " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
            [Char]
"information that should be " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"."
        ]
      where
        what :: [Char]
what = case IsOpaque
isOpaque of
          IsOpaque
TransparentDef -> [Char]
"abstract"
          OpaqueDef OpaqueId
_    -> [Char]
"opaque"


    Warning
NotAffectedByOpaque -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Only function definitions can be marked opaque. This definition will be treated as transparent."

    UnfoldingWrongName QName
x -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Name in unfolding clause should be unambiguous defined name:" [m Doc] -> [m Doc] -> [m Doc]
forall 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
x]

    UnfoldTransparentName QName
qn -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name" [m Doc] -> [m Doc] -> [m Doc]
forall 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
qn m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"mentioned by an unfolding clause, does not belong to an opaque block. This has no effect."

    Warning
AbstractInLetBindings -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Abstract definitions are not allowed in let bindings."
    Warning
MacroInLetBindings    -> [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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Macros can not be defined in let bindings."

    Warning
UselessOpaque -> m Doc
"This `opaque` block has no effect."

    HiddenNotInArgumentPosition Expr
e -> [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
$
      [Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an implicit argument."

    InstanceNotInArgumentPosition Expr
e -> [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
$
      [Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an instance argument."

    InvalidDisplayForm QName
x [Char]
reason -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring invalid display form for"
        , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x ]
        , if [Char] -> Bool
forall a. Null a => a -> Bool
null [Char]
reason then [] else m Doc
"because" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
reason
        ]

    UnusedVariablesInDisplayForm List1 Name
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The following"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ List1 Name -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural List1 Name
xs [Char]
"variable is" [Char]
"variables are"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"bound on the left hand side but unused on the right hand side of the display form:"
        ]
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (Name -> m Doc) -> List1 Name -> 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 Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 Name
xs
      , [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ m Doc
"Replace" ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ List1 Name -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural List1 Name
xs [Char]
"it by an underscore" [Char]
"them by underscores"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to pacify this warning"
        ]
      ]

    TooManyArgumentsToSort QName
q List1 (NamedArg Expr)
args -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Too many arguments given to sort"
      , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q ]
      ]

    WithClauseProjectionFixityMismatch NamedArg Pattern
p0 ProjOrigin
o' NamedArg DeBruijnPattern
q ProjOrigin
o -> [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"With clause pattern"
        , [ NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p0 ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not an instance of its parent pattern"
        , [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> m [Doc]
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q] ]
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"since the parent pattern is"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"and the with clause pattern is"
        , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o'
        ]
      where
        prettyProjOrigin :: ProjOrigin -> a
prettyProjOrigin ProjOrigin
ProjPrefix  = a
"a prefix projection"
        prettyProjOrigin ProjOrigin
ProjPostfix = a
"a postfix projection"
        prettyProjOrigin ProjOrigin
ProjSystem  = a
forall a. HasCallStack => a
__IMPOSSIBLE__

    FaceConstraintCannotBeHidden ArgInfo
ai -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Face constraint patterns cannot be" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Hiding -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai), m Doc
"arguments"]

    FaceConstraintCannotBeNamed NamedName
x -> [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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ignoring name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
"`" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> NamedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NamedName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"`"] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"given to face constraint pattern"

    CustomBackendWarning [Char]
backend Doc
warn -> ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
backend m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":") 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
warn

{-# SPECIALIZE prettyRecordFieldWarning :: RecordFieldWarning -> TCM Doc #-}
prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning :: forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning = \case
  W.DuplicateFields List1 (Name, Range)
xrs    -> List1 Name -> m Doc
forall (m :: * -> *). MonadPretty m => List1 Name -> m Doc
prettyDuplicateFields    (List1 Name -> m Doc) -> List1 Name -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> List1 (Name, Range) -> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Range) -> Name
forall a b. (a, b) -> a
fst List1 (Name, Range)
xrs
  W.TooManyFields QName
q [Name]
ys List1 (Name, Range)
xrs -> QName -> [Name] -> List1 Name -> m Doc
forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> List1 Name -> m Doc
prettyTooManyFields QName
q [Name]
ys (List1 Name -> m Doc) -> List1 Name -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> List1 (Name, Range) -> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Range) -> Name
forall a b. (a, b) -> a
fst List1 (Name, Range)
xrs

prettyDuplicateFields :: MonadPretty m => List1 C.Name -> m Doc
prettyDuplicateFields :: forall (m :: * -> *). MonadPretty m => List1 Name -> m Doc
prettyDuplicateFields List1 Name
xs = [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [ m Doc
"Duplicate", List1 Name -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS List1 Name
xs m Doc
"field" ]
    , m Doc -> NonEmpty (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 ((Name -> m Doc) -> List1 Name -> 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 Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 Name
xs)
    , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in record"
    ]

{-# SPECIALIZE prettyTooManyFields :: QName -> [C.Name] -> List1 C.Name -> TCM Doc  #-}
prettyTooManyFields :: MonadPretty m => QName -> [C.Name] -> List1 C.Name -> m Doc
prettyTooManyFields :: forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> List1 Name -> m Doc
prettyTooManyFields QName
r [Name]
missing List1 Name
xs = [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The record type"
    , [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r]
    , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"does not have the"
    , List1 Name -> [m Doc]
forall {m :: * -> *} {a}.
(Functor m, Sized a, IsString (m Doc)) =>
a -> [m Doc]
fields List1 Name
xs
    , m Doc -> NonEmpty (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 ((Name -> m Doc) -> List1 Name -> 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 Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 Name
xs)
    , if [Name] -> Bool
forall a. Null a => a -> Bool
null [Name]
missing then [] else [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but it would have the"
      , [Name] -> [m Doc]
forall {m :: * -> *} {a}.
(Functor m, Sized a, IsString (m Doc)) =>
a -> [m Doc]
fields [Name]
missing
      , 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 ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
missing)
      ]
    ]
  where
    fields :: a -> [m Doc]
fields a
ys = [ a -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS a
ys m Doc
"field" ]

{-# SPECIALIZE prettyNotInScopeNames :: (Pretty a, HasRange a) => Bool -> (a -> TCM Doc) -> [a] -> TCM Doc #-}
-- | Report a number of names that are not in scope.
prettyNotInScopeNames
  :: (MonadPretty m, Pretty a, HasRange a)
  => Bool          -- ^ Print range?
  -> (a -> m Doc)  -- ^ Correction suggestion generator.
  -> [a]           -- ^ Names that are not in scope.
  -> m Doc
prettyNotInScopeNames :: forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
printRange a -> m Doc
suggestion [a]
xs = VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
name [a]
xs
  where
  name :: a -> m Doc
name a
x = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x
    , if Bool
printRange then 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 (a -> Range
forall a. HasRange a => a -> Range
getRange a
x) else m Doc
forall a. Null a => a
empty
    , a -> m Doc
suggestion a
x
    ]

{-# SPECIALIZE didYouMean :: (Pretty a, Pretty b) => [C.QName] -> (a -> b) -> a -> Maybe (TCM Doc) #-}
-- | Suggest some corrections to a misspelled name.
didYouMean
  :: (MonadPretty m, Pretty a, Pretty b)
  => [C.QName]     -- ^ Names in scope.
  -> (a -> b)      -- ^ Canonization function for similarity search.
  -> a             -- ^ A name which is not in scope.
  -> Maybe (m Doc) -- ^ "did you mean" hint.
didYouMean :: forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope a -> b
canon a
x
  | [[Char]] -> Bool
forall a. Null a => a -> Bool
null [[Char]]
ys   = Maybe (m Doc)
forall a. Maybe a
Nothing
  | Bool
otherwise = m Doc -> Maybe (m Doc)
forall a. a -> Maybe a
Just (m Doc -> Maybe (m Doc)) -> m Doc -> Maybe (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
      [ m Doc
"did you mean"
      , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([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
$ 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
" or" ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
                 ([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ [Char]
y -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"'" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'") [[Char]]
ys)
        m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
      ]
  where
  strip :: Pretty b => b -> String
  strip :: forall a. Pretty a => a -> [Char]
strip        = (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ([Char] -> [Char]) -> (b -> [Char]) -> b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') ([Char] -> [Char]) -> (b -> [Char]) -> b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow
  -- dropModule x = fromMaybe x $ List.stripPrefix "module " x
  maxDist :: a -> a
maxDist a
n    = a -> a -> a
forall a. Integral a => a -> a -> a
div a
n a
3
  close :: [a] -> [a] -> Bool
close [a]
a [a]
b    = [a] -> [a] -> VerboseLevel
forall a. Eq a => [a] -> [a] -> VerboseLevel
editDistance [a]
a [a]
b VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel -> VerboseLevel
forall {a}. Integral a => a -> a
maxDist ([a] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [a]
a)
  ys :: [[Char]]
ys           = (QName -> [Char]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ([QName] -> [[Char]]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
close (b -> [Char]
forall a. Pretty a => a -> [Char]
strip (b -> [Char]) -> b -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> b
canon a
x) ([Char] -> Bool) -> (QName -> [Char]) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
strip (Name -> [Char]) -> (QName -> Name) -> QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
C.unqualify) [QName]
inscope


prettyTCWarnings :: Set TCWarning -> TCM String
prettyTCWarnings :: Set TCWarning -> TCM [Char]
prettyTCWarnings = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char])
-> (Set TCWarning -> TCMT IO [[Char]])
-> Set TCWarning
-> TCM [Char]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> (Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> [Char]
forall a. Doc a -> [Char]
P.render ([Doc] -> [[Char]])
-> (Set TCWarning -> TCMT IO [Doc])
-> Set TCWarning
-> TCMT IO [[Char]]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Set TCWarning -> TCMT IO [Doc]
prettyTCWarnings'

prettyTCWarnings' :: Set TCWarning -> TCM [Doc]
prettyTCWarnings' :: Set TCWarning -> TCMT IO [Doc]
prettyTCWarnings' = (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM ([TCWarning] -> TCMT IO [Doc])
-> (Set TCWarning -> [TCWarning]) -> Set TCWarning -> TCMT IO [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TCWarning -> [TCWarning]
filterTCWarnings

-- | If there are several warnings, remove the unsolved-constraints warning
-- in case there are no interesting constraints to list.
filterTCWarnings :: Set TCWarning -> [TCWarning]
filterTCWarnings :: Set TCWarning -> [TCWarning]
filterTCWarnings Set TCWarning
wset = case Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
wset of
  -- #4065: Always keep the only warning
  [TCWarning
w] -> [TCWarning
w]
  -- Andreas, 2019-09-10, issue #4065:
  -- If there are several warnings, remove the unsolved-constraints warning
  -- in case there are no interesting constraints to list.
  [TCWarning]
ws  -> ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
`filter` [TCWarning]
ws) ((TCWarning -> Bool) -> [TCWarning])
-> (TCWarning -> Bool) -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ \ TCWarning
w -> case TCWarning -> Warning
tcWarning TCWarning
w of
    UnsolvedConstraints List1 ProblemConstraint
cs -> (ProblemConstraint -> Bool) -> List1 ProblemConstraint -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProblemConstraint -> Bool
interestingConstraint List1 ProblemConstraint
cs
    Warning
_ -> Bool
True


-- | Turns warnings, if any, into errors.
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError [TCWarning]
mws = case ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) of
   ([], [])                   -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
   (_unsolvedHoles :: [TCWarning]
_unsolvedHoles@(TCWarning
_:[TCWarning]
_), []) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
SolvedButOpenHoles
   ([TCWarning]
_ , TCWarning
w : [TCWarning]
ws)               -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> TypeError
NonFatalErrors (Set1 TCWarning -> TypeError) -> Set1 TCWarning -> TypeError
forall a b. (a -> b) -> a -> b
$ NonEmpty TCWarning -> Set1 TCWarning
forall a. Ord a => NonEmpty a -> NESet a
Set1.fromList (TCWarning
w TCWarning -> [TCWarning] -> NonEmpty TCWarning
forall a. a -> [a] -> NonEmpty a
:| [TCWarning]
ws)
   where
   -- filter out unsolved interaction points for imported module so
   -- that we get the right error message (see test case Fail/Issue1296)
   ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) = (TCWarning -> Bool) -> [TCWarning] -> ([TCWarning], [TCWarning])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Warning -> Bool
isUnsolvedIM (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
mws
   isUnsolvedIM :: Warning -> Bool
isUnsolvedIM UnsolvedInteractionMetas{} = Bool
True
   isUnsolvedIM Warning
_                          = Bool
False


-- | Depending which flags are set, one may happily ignore some
-- warnings.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarningsPreserving :: forall (m :: * -> *).
HasOptions m =>
Set WarningName -> Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarningsPreserving Set WarningName
additionalKeptWarnings Set TCWarning
ws = do
  -- For some reason some SafeFlagPragma seem to be created multiple times.
  -- This is a way to collect all of them and remove duplicates.
  let pragmas :: TCWarning -> ([TCWarning], Set [Char])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma Set [Char]
ps -> ([TCWarning
w], Set [Char]
ps); Warning
_ -> ([], Set [Char]
forall a. Null a => a
empty) }
  let sfp :: Set TCWarning
sfp = case (TCWarning -> ([TCWarning], Set [Char]))
-> Set TCWarning -> ([TCWarning], Set [Char])
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> ([TCWarning], Set [Char])
pragmas Set TCWarning
ws of
              (TCWarning CallStack
loc Range
r Warning
w Doc
doc [Char]
str Bool
b : [TCWarning]
_, Set [Char]
sfp) ->
                 TCWarning -> Set TCWarning
forall el coll. Singleton el coll => el -> coll
singleton (TCWarning -> Set TCWarning) -> TCWarning -> Set TCWarning
forall a b. (a -> b) -> a -> b
$ CallStack -> Range -> Warning -> Doc -> [Char] -> Bool -> TCWarning
TCWarning CallStack
loc Range
r (Set [Char] -> Warning
SafeFlagPragma Set [Char]
sfp) Doc
doc [Char]
str Bool
b
              ([TCWarning], Set [Char])
_ -> Set TCWarning
forall a. Null a => a
empty

  pragmaWarnings <- (WarningMode
-> Lens' WarningMode (Set WarningName) -> Set WarningName
forall o i. o -> Lens' o i -> i
^. (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
Lens' WarningMode (Set WarningName)
warningSet) (WarningMode -> Set WarningName)
-> (PragmaOptions -> WarningMode)
-> PragmaOptions
-> Set WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WarningMode
optWarningMode (PragmaOptions -> Set WarningName)
-> m PragmaOptions -> m (Set WarningName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let warnSet = Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set WarningName
pragmaWarnings Set WarningName
additionalKeptWarnings

  -- filter out the warnings the flags told us to ignore
  let cleanUp Warning
w = let wName :: WarningName
wName = Warning -> WarningName
warningName Warning
w in
        WarningName
wName WarningName -> WarningName -> Bool
forall a. Eq a => a -> a -> Bool
/= WarningName
SafeFlagPragma_
        Bool -> Bool -> Bool
&& WarningName
wName WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
warnSet

  return $ Set.union sfp $ Set.filter (cleanUp . tcWarning) ws

applyFlagsToTCWarnings :: HasOptions m => Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarnings :: forall (m :: * -> *).
HasOptions m =>
Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarnings = Set WarningName -> Set TCWarning -> m (Set TCWarning)
forall (m :: * -> *).
HasOptions m =>
Set WarningName -> Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarningsPreserving Set WarningName
forall a. Set a
Set.empty

{-# SPECIALIZE isBoundaryConstraint :: ProblemConstraint -> TCM (Maybe Range) #-}
isBoundaryConstraint :: (ReadTCState m, MonadTCM m) => ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint :: forall (m :: * -> *).
(ReadTCState m, MonadTCM m) =>
ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint ProblemConstraint
c =
  Closure Constraint
-> (Constraint -> m (Maybe Range)) -> m (Maybe Range)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) ((Constraint -> m (Maybe Range)) -> m (Maybe Range))
-> (Constraint -> m (Maybe Range)) -> m (Maybe Range)
forall a b. (a -> b) -> a -> b
$ \case
    ValueCmp Comparison
_ CompareAs
_ (MetaV MetaId
mid Elims
xs) Term
y | Just Args
xs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
xs ->
      ((MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range)
-> Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range
forall {a} {b} {c} {d}. HasRange a => (a, b, c, d) -> Range
g (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
 -> Maybe Range)
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid Args
xs)
    ValueCmp Comparison
_ CompareAs
_ Term
y (MetaV MetaId
mid Elims
xs) | Just Args
xs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
xs ->
      ((MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range)
-> Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
-> Maybe Range
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaVariable, IntMap Bool, SubstCand, Substitution) -> Range
forall {a} {b} {c} {d}. HasRange a => (a, b, c, d) -> Range
g (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)
 -> Maybe Range)
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> m (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid Args
xs)
    Constraint
_ -> Maybe Range -> m (Maybe Range)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Range
forall a. Maybe a
Nothing
  where
    g :: (a, b, c, d) -> Range
g (a
a, b
_, c
_, d
_) = a -> Range
forall a. HasRange a => a -> Range
getRange a
a

{-# SPECIALIZE getAllUnsolvedWarnings :: TCM [TCWarning] #-}
getAllUnsolvedWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]
getAllUnsolvedWarnings :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings = do
  unsolvedInteractions <- m [Range]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas

  allCons <- getAllConstraints
  unsolvedConstraints  <- filterM (fmap isNothing . isBoundaryConstraint) allCons
  interactionBoundary  <- catMaybes <$> traverse isBoundaryConstraint allCons

  unsolvedMetas        <- getUnsolvedMetas

  mapM warning_ $ catMaybes
    [ UnsolvedInteractionMetas  . Set1.fromList <$> List1.nonEmpty unsolvedInteractions
    , UnsolvedMetaVariables     . Set1.fromList <$> List1.nonEmpty unsolvedMetas
    , UnsolvedConstraints                       <$> List1.nonEmpty unsolvedConstraints
    , InteractionMetaBoundaries . Set1.fromList <$> List1.nonEmpty interactionBoundary
    ]

-- | Collect all warnings that have accumulated in the state.

{-# SPECIALIZE getAllWarnings :: WhichWarnings -> TCM (Set TCWarning) #-}
getAllWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m (Set TCWarning)
getAllWarnings :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings = Set WarningName -> WhichWarnings -> m (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving Set WarningName
forall a. Set a
Set.empty

{-# SPECIALIZE getAllWarningsPreserving :: Set WarningName -> WhichWarnings -> TCM (Set TCWarning) #-}
getAllWarningsPreserving ::
  (ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving Set WarningName
keptWarnings WhichWarnings
ww = do
  unsolved            <- [TCWarning] -> Set TCWarning
forall a. Ord a => [a] -> Set a
Set.fromList ([TCWarning] -> Set TCWarning)
-> m [TCWarning] -> m (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [TCWarning]
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings
  collectedTCWarnings <- useTC stTCWarnings

  -- E.g. the InversionDepthReached warning is only shown when we have unsolved constraints.
  let showWarn
        | Set TCWarning -> Bool
forall a. Null a => a -> Bool
null Set TCWarning
unsolved = \ Warning
w -> Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww Bool -> Bool -> Bool
&& Bool -> Bool
not (Warning -> Bool
onlyShowIfUnsolved Warning
w)
        | Bool
otherwise     = \ Warning
w -> Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww

  Set.filter (showWarn . tcWarning) <$> do
    applyFlagsToTCWarningsPreserving keptWarnings $
      unsolved `Set.union` collectedTCWarnings

getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning)
getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning)
getAllWarningsOfTCErr = \case
  TypeError CallStack
_ TCState
tcst Closure TypeError
cls -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cls of
    NonFatalErrors{} -> Set TCWarning -> TCM (Set TCWarning)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set TCWarning
forall a. Null a => a
empty
    TypeError
_ -> TCM (Set TCWarning) -> TCM (Set TCWarning)
forall a. TCM a -> TCM a
localTCState (TCM (Set TCWarning) -> TCM (Set TCWarning))
-> TCM (Set TCWarning) -> TCM (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ do
      TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
      -- We filter out the unsolved(Metas/Constraints) to stay
      -- true to the previous error messages.
      (TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) (Set TCWarning -> Set TCWarning)
-> TCM (Set TCWarning) -> TCM (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCM (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
  TCErr
_ -> Set TCWarning -> TCM (Set TCWarning)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set TCWarning
forall a. Null a => a
empty