module Agda.TypeChecking.Pretty.Warning where

import Prelude hiding ( null )

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

-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail ( MonadFail )

import Data.Char ( toLower )
import Data.Function (on)
import Data.Maybe

import qualified Data.Set as Set
import Data.Set (Set)

import qualified Data.List as List
import qualified Data.Text as T

import Agda.TypeChecking.Monad.Base
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 )
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Scope.Base ( concreteNamesInScope, NameOrModule(..) )
import Agda.Syntax.Internal
import Agda.Syntax.Translation.InternalToAbstract

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

import Agda.Utils.Lens
import Agda.Utils.List ( editDistance )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty ( Pretty, prettyShow, singPlural )
import qualified Agda.Syntax.Common.Pretty as P

instance PrettyTCM TCWarning where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM w :: TCWarning
w@(TCWarning CallStack
loc Range
_ Warning
_ Doc
_ Bool
_) = do
    String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"warning" VerboseLevel
2 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Warning raised at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CallStack -> String
forall a. Pretty a => a -> String
prettyShow CallStack
loc
    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
$ TCWarning -> Doc
tcWarningPrintedWarning TCWarning
w

-- | Prefix for a warning text showing name of the warning.
--   E.g. @warning: -W[no]<warning_name>@
prettyWarningName :: MonadPretty m => WarningName -> m Doc
prettyWarningName :: forall (m :: * -> *). MonadPretty m => WarningName -> m Doc
prettyWarningName WarningName
w = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat
  [ m Doc
"warning: -W[no]"
  , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ WarningName -> String
warningName2String WarningName
w
  ]

prettyWarning :: MonadPretty m => Warning -> m Doc
prettyWarning :: forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning = \case

    UnsolvedMetaVariables [Range]
ms  ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 ([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
$ (Range -> m Doc) -> [Range] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM [Range]
ms)

    UnsolvedInteractionMetas [Range]
is ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 ([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
$ (Range -> m Doc) -> [Range] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM [Range]
is)

    InteractionMetaBoundaries [Range]
is ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 ([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
$ (Range -> m Doc) -> [Range] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (Set Range -> [Range]
forall a. Set a -> [a]
Set.toList ([Range] -> Set Range
forall a. Ord a => [a] -> Set a
Set.fromList [Range]
is)))

    UnsolvedConstraints Constraints
cs -> do
      [Doc]
pcs <- Constraints -> m [Doc]
forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
prettyInterestingConstraints Constraints
cs
      if [Doc] -> Bool
forall a. Null a => a -> Bool
null [Doc]
pcs
        then [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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unsolved constraints"  -- #4065: keep minimal warning text
        else [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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Failed to solve the following constraints:"
          , 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
$ Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
forall a. Eq a => [a] -> [a]
List.nub [Doc]
pcs
          ]

    TerminationIssue [TerminationError]
because -> do
      QName -> QName
dropTopLevel <- m (QName -> QName)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Termination checking failed for the following functions:"
        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 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
             (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> m Doc) -> (QName -> QName) -> QName -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName
dropTopLevel) ([QName] -> [m Doc]) -> [QName] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
               (TerminationError -> [QName]) -> [TerminationError] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
termErrFunctions [TerminationError]
because)
        m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Problematic calls:"
        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 (([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
forall a. Eq a => [a] -> [a]
List.nub) (m [Doc] -> m Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
              (CallInfo -> m Doc) -> [CallInfo] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CallInfo -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CallInfo -> m Doc
prettyTCM ([CallInfo] -> m [Doc]) -> [CallInfo] -> m [Doc]
forall a b. (a -> b) -> a -> b
$ (CallInfo -> Range) -> [CallInfo] -> [CallInfo]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn CallInfo -> Range
forall a. HasRange a => a -> Range
getRange ([CallInfo] -> [CallInfo]) -> [CallInfo] -> [CallInfo]
forall a b. (a -> b) -> a -> b
$
              (TerminationError -> [CallInfo])
-> [TerminationError] -> [CallInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [CallInfo]
termErrCalls [TerminationError]
because)

    UnreachableClauses QName
f [Range]
pss -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unreachable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (VerboseLevel -> String -> String
forall {a}. (Num a, Eq a) => a -> String -> String
plural ([Range] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Range]
pss) String
"clause")
        where
          plural :: a -> String -> String
plural a
1 String
thing = String
thing
          plural a
n String
thing = String
thing String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"

    CoverageIssue QName
f [(Telescope, [NamedArg DeBruijnPattern])]
pss -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Incomplete pattern matching for" [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
f 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]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Missing cases:") 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 ([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
$ ((Telescope, [NamedArg DeBruijnPattern]) -> m Doc)
-> [(Telescope, [NamedArg DeBruijnPattern])] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display [(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 [Clause]
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 (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Exact splitting is enabled, but the following" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords ([Clause] -> String -> String -> String
forall a c. Sized a => a -> c -> c -> c
P.singPlural [Clause]
cs String
"clause" String
"clauses") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
            String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"could not be preserved as definitional equalities in the translation to a case tree:"
           ) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
      (Clause -> m Doc) -> [Clause] -> [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) -> (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]
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
$
          String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Exact splitting is enabled, but the following clause" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
          String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]

    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 (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 [MetaId]
ms -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cannot generalize over unsolved sort metas:"
            , 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 [ MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Range -> m Doc) -> m Range -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x) | MetaId
x <- [MetaId]
ms ]
            , [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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

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

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

    Warning
EmptyRewritePragma -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> (String -> [m Doc]) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"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) -> (String -> [m Doc]) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Empty `where' block (ignored)"

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

    ClashesViaRenaming NameOrModule
nm [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" ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
xs
      ]

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

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

    UselessHiding [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
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Ignoring names in `hiding' directive:"
      , m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (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 [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"to have a separate Haskell definition"

    Warning
WrongInstanceDeclaration -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$
      String
"Instances should be of type {Γ} → C, where C evaluates to a postulated name or the name of " String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance declarations with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance arguments with explicit arguments are never considered by instance search," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"has no effect."

    InversionDepthReached QName
f -> do
      VerboseLevel
maxDepth <- m VerboseLevel
forall (m :: * -> *). HasOptions m => m VerboseLevel
maxInversionDepth
      [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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Refusing to invert pattern matching of" [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
f] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String
"because the maximum depth (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> String
forall a. Show a => a -> String
show VerboseLevel
maxDepth String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") has been reached.") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Most likely this means you have an unsatisfiable constraint, but it could" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"also mean that you need to increase the maximum depth using the flag" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"--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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is declared coinductive, but option" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"--guardedness is not enabled. Coinductive functions on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"this type will likely be rejected by the termination" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"checker unless this flag is enabled."

    GenericWarning Doc
d -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    GenericNonFatalError Doc
d -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    GenericUseless 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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"with safe flag"

    SafeFlagPragma [String]
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
      [ [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ [String]
-> (String -> String) -> (String -> String) -> String -> String
forall a c. Sized a => a -> c -> c -> c
singPlural (String -> [String]
words (String -> [String]) -> [String] -> [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [String]
xs) String -> String
forall a. a -> a
id (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s") String
"Cannot set OPTIONS pragma" ]
      , (String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
xs
      , [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"with safe flag." ]
      ]

    Warning
SafeFlagNonTerminating -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NON_TERMINATING pragma with safe flag."

    Warning
SafeFlagTerminating -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use TERMINATING pragma with safe flag."

    Warning
SafeFlagWithoutKFlagPrimEraseEquality -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Using primEraseEquality with the without-K flag is inconsistent.")

    Warning
SafeFlagNoPositivityCheck -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NO_POSITIVITY_CHECK pragma with safe flag."

    Warning
SafeFlagPolarity -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use POLARITY pragma with safe flag."

    Warning
SafeFlagNoUniverseCheck -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NO_UNIVERSE_CHECK pragma with safe flag."

    Warning
SafeFlagEta -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use ETA pragma with safe flag."

    Warning
SafeFlagInjective -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use INJECTIVE pragma with safe flag."

    Warning
SafeFlagNoCoverageCheck -> [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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NON_COVERING pragma with safe flag."

    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

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

    ModuleDoesntExport QName
m [Name]
names [Name]
modules [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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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

    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
          [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"and" , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs2 ]
          , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
          [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
          , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
          , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
        [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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] , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
        [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
        , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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] , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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] , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
        [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 ]
        ]
      ]

    PragmaCompileErased String
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
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The backend"
      , [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
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
        ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"so the COMPILE pragma will be ignored."
      ]

    NotInScopeW [QName]
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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Not in scope:"
      , do
        [QName]
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
        Bool -> (QName -> m Doc) -> [QName] -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
True ([QName] -> QName -> m Doc
forall {m :: * -> *}.
(Null (m Doc), IsString (m Doc), MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 Semigroup (m Doc)) =>
[QName] -> QName -> m Doc
suggestion [QName]
inscope) [QName]
xs
      ]
      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 -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
s ]
        , [ m Doc
"did you forget space around the '->'?" | String
"->" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isInfixOf` String
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 :: String
s = QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
x

    AsPatternShadowsConstructorOrPatternSynonym Bool
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
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Name bound in @-pattern ignored because it shadows"
      , if Bool
patsyn then String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"pattern synonym" else [ m Doc
"constructor" ]
      ]

    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
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in hard compile-time mode"

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

    Warning
NotAffectedByOpaque -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Only functions and primitives can be marked opaque. This declaration will be treated as transparent."

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

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

prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning :: forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning = \case
  DuplicateFieldsWarning [(Name, Range)]
xrs    -> [Name] -> m Doc
forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields ([Name] -> m Doc) -> [Name] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> [(Name, Range)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Range) -> Name
forall a b. (a, b) -> a
fst [(Name, Range)]
xrs
  TooManyFieldsWarning QName
q [Name]
ys [(Name, Range)]
xrs -> QName -> [Name] -> [Name] -> m Doc
forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
q [Name]
ys ([Name] -> m Doc) -> [Name] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Range) -> Name) -> [(Name, Range)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Range) -> Name
forall a b. (a, b) -> a
fst [(Name, Range)]
xrs

prettyDuplicateFields :: MonadPretty m => [C.Name] -> m Doc
prettyDuplicateFields :: forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields [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
    [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Duplicate"
    , [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
xs
    , 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]
xs)
    , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in record"
    ]
  where
  fields :: a -> [m Doc]
fields a
ys = a -> [m Doc] -> [m Doc] -> [m Doc]
forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"field"] [String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"fields"]

prettyTooManyFields :: MonadPretty m => QName -> [C.Name] -> [C.Name] -> m Doc
prettyTooManyFields :: forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
r [Name]
missing [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
    [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
    , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"does not have the"
    , [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
xs
    , 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]
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
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"but it would have the"
      , [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => 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] -> [m Doc]
forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"field"] [String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"fields"]

-- | 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
    ]

-- | 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
  | [String] -> Bool
forall a. Null a => a -> Bool
null [String]
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
$
                 (String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
y -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") [String]
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 -> String
strip        = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> (b -> String) -> b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') (String -> String) -> (b -> String) -> b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> String
forall a. Pretty a => a -> String
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 :: [String]
ys           = (QName -> String) -> [QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QName -> String
forall a. Pretty a => a -> String
prettyShow ([QName] -> [String]) -> [QName] -> [String]
forall a b. (a -> b) -> a -> b
$ (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
close (b -> String
forall a. Pretty a => a -> String
strip (b -> String) -> b -> String
forall a b. (a -> b) -> a -> b
$ a -> b
canon a
x) (String -> Bool) -> (QName -> String) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Pretty a => a -> String
strip (Name -> String) -> (QName -> Name) -> QName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
C.unqualify) [QName]
inscope


prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings = ([Doc] -> String) -> TCMT IO [Doc] -> TCM String
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([String] -> String
unlines ([String] -> String) -> ([Doc] -> [String]) -> [Doc] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
List.intersperse String
"" ([String] -> [String]) -> ([Doc] -> [String]) -> [Doc] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
forall a. Doc a -> String
P.render) (TCMT IO [Doc] -> TCM String)
-> ([TCWarning] -> TCMT IO [Doc]) -> [TCWarning] -> TCM String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> TCMT IO [Doc]
prettyTCWarnings'

renderTCWarnings' :: [TCWarning] -> TCM [String]
renderTCWarnings' :: [TCWarning] -> TCM [String]
renderTCWarnings' = ([Doc] -> [String]) -> TCMT IO [Doc] -> TCM [String]
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
forall a. Doc a -> String
P.render) (TCMT IO [Doc] -> TCM [String])
-> ([TCWarning] -> TCMT IO [Doc]) -> [TCWarning] -> TCM [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> TCMT IO [Doc]
prettyTCWarnings'

prettyTCWarnings' :: [TCWarning] -> TCM [Doc]
prettyTCWarnings' :: [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])
-> ([TCWarning] -> [TCWarning]) -> [TCWarning] -> TCMT IO [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> [TCWarning]
filterTCWarnings

-- | If there are several warnings, remove the unsolved-constraints warning
-- in case there are no interesting constraints to list.
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings = \case
  -- #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 Constraints
cs -> (ProblemConstraint -> Bool) -> Constraints -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProblemConstraint -> Bool
interestingConstraint Constraints
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]
_, ws :: [TCWarning]
ws@(TCWarning
_:[TCWarning]
_))              -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [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 -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving :: forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving Set WarningName
additionalKeptWarnings [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], [String])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma [String]
ps -> ([TCWarning
w], [String]
ps); Warning
_ -> ([], []) }
  let sfp :: [TCWarning]
sfp = case ([String] -> [String])
-> ([TCWarning], [String]) -> ([TCWarning], [String])
forall a b. (a -> b) -> ([TCWarning], a) -> ([TCWarning], b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [String] -> [String]
forall a. Eq a => [a] -> [a]
List.nub ((TCWarning -> ([TCWarning], [String]))
-> [TCWarning] -> ([TCWarning], [String])
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> ([TCWarning], [String])
pragmas [TCWarning]
ws) of
              (TCWarning CallStack
loc Range
r Warning
w Doc
p Bool
b:[TCWarning]
_, [String]
sfp) ->
                 [CallStack -> Range -> Warning -> Doc -> Bool -> TCWarning
TCWarning CallStack
loc Range
r ([String] -> Warning
SafeFlagPragma [String]
sfp) Doc
p Bool
b]
              ([TCWarning], [String])
_                        -> []

  Set WarningName
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
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 -> Bool
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
        Bool -> Bool -> Bool
&& case Warning
w of
          UnsolvedMetaVariables [Range]
ums    -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Range] -> Bool
forall a. Null a => a -> Bool
null [Range]
ums
          UnsolvedInteractionMetas [Range]
uis -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Range] -> Bool
forall a. Null a => a -> Bool
null [Range]
uis
          UnsolvedConstraints Constraints
ucs      -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Constraints -> Bool
forall a. Null a => a -> Bool
null Constraints
ucs
          Warning
_                            -> Bool
True

  [TCWarning] -> m [TCWarning]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCWarning] -> m [TCWarning]) -> [TCWarning] -> m [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning]
sfp [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
cleanUp (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
ws

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

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 [Arg Term]
xs <- Elims -> Maybe [Arg Term]
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
-> [Arg Term]
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid [Arg Term]
xs)
    ValueCmp Comparison
_ CompareAs
_ Term
y (MetaV MetaId
mid Elims
xs) | Just [Arg Term]
xs <- Elims -> Maybe [Arg Term]
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
-> [Arg Term]
-> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
mid [Arg Term]
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

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

  Constraints
allCons <- m Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
  Constraints
unsolvedConstraints  <- (ProblemConstraint -> m Bool) -> Constraints -> m Constraints
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Maybe Range -> Bool) -> m (Maybe Range) -> m Bool
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe Range -> Bool
forall a. Maybe a -> Bool
isNothing (m (Maybe Range) -> m Bool)
-> (ProblemConstraint -> m (Maybe Range))
-> ProblemConstraint
-> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> m (Maybe Range)
forall (m :: * -> *).
(ReadTCState m, MonadTCM m) =>
ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint) Constraints
allCons
  [Range]
interactionBoundary  <- [Maybe Range] -> [Range]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Range] -> [Range]) -> m [Maybe Range] -> m [Range]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProblemConstraint -> m (Maybe Range))
-> Constraints -> m [Maybe Range]
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 ProblemConstraint -> m (Maybe Range)
forall (m :: * -> *).
(ReadTCState m, MonadTCM m) =>
ProblemConstraint -> m (Maybe Range)
isBoundaryConstraint Constraints
allCons

  [Range]
unsolvedMetas        <- m [Range]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedMetas

  let checkNonEmpty :: (a -> a) -> a -> f a
checkNonEmpty a -> a
c a
rs = a -> a
c a
rs a -> f () -> f a
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Bool
forall a. Null a => a -> Bool
null a
rs)

  (Warning -> m TCWarning) -> [Warning] -> m [TCWarning]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Warning -> m TCWarning
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m TCWarning
warning_ ([Warning] -> m [TCWarning]) -> [Warning] -> m [TCWarning]
forall a b. (a -> b) -> a -> b
$ [Maybe Warning] -> [Warning]
forall a. [Maybe a] -> [a]
catMaybes
                [ ([Range] -> Warning) -> [Range] -> Maybe Warning
forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedInteractionMetas  [Range]
unsolvedInteractions
                , ([Range] -> Warning) -> [Range] -> Maybe Warning
forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedMetaVariables     [Range]
unsolvedMetas
                , (Constraints -> Warning) -> Constraints -> Maybe Warning
forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty Constraints -> Warning
UnsolvedConstraints       Constraints
unsolvedConstraints
                , ([Range] -> Warning) -> [Range] -> Maybe Warning
forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
InteractionMetaBoundaries [Range]
interactionBoundary
                ]

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

getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m [TCWarning]
getAllWarnings :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings = Set WarningName -> WhichWarnings -> m [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
forall a. Set a
Set.empty

getAllWarningsPreserving
  :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m)
  => Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
keptWarnings WhichWarnings
ww = do
  [TCWarning]
unsolved            <- m [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings
  [TCWarning]
collectedTCWarnings <- Lens' TCState [TCWarning] -> m [TCWarning]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' TCState [TCWarning]
stTCWarnings

  let showWarn :: Warning -> Bool
showWarn 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 ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
unsolved Bool -> Bool -> Bool
&& Warning -> Bool
onlyShowIfUnsolved Warning
w)

  ([TCWarning] -> [TCWarning]) -> m [TCWarning] -> m [TCWarning]
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
showWarn (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning))
    (m [TCWarning] -> m [TCWarning]) -> m [TCWarning] -> m [TCWarning]
forall a b. (a -> b) -> a -> b
$ Set WarningName -> [TCWarning] -> m [TCWarning]
forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving Set WarningName
keptWarnings
    ([TCWarning] -> m [TCWarning]) -> [TCWarning] -> m [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> [TCWarning]
forall a. [a] -> [a]
reverse ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning]
unsolved [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ [TCWarning]
collectedTCWarnings

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err = case TCErr
err of
  TypeError CallStack
_ TCState
tcst Closure TypeError
cls -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cls of
    NonFatalErrors{} -> [TCWarning] -> TCM [TCWarning]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    TypeError
_ -> TCM [TCWarning] -> TCM [TCWarning]
forall a. TCM a -> TCM a
localTCState (TCM [TCWarning] -> TCM [TCWarning])
-> TCM [TCWarning] -> TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ do
      TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
      [TCWarning]
ws <- WhichWarnings -> TCM [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
      -- We filter out the unsolved(Metas/Constraints) to stay
      -- true to the previous error messages.
      [TCWarning] -> TCM [TCWarning]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCWarning] -> TCM [TCWarning]) -> [TCWarning] -> TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
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) [TCWarning]
ws
  TCErr
_ -> [TCWarning] -> TCM [TCWarning]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []