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.IntSet (IntSet)
import qualified Data.IntSet as IntSet
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 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 ( IsOpaque(OpaqueDef, TransparentDef), getHiding, 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.FileName ( filePath )
import Agda.Utils.Functor  ( (<.>) )
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
    [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
    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

{-# SPECIALIZE prettyWarningName :: WarningName -> TCM Doc #-}
-- | 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]"
  , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ WarningName -> [Char]
warningName2String WarningName
w
  ]

{-# SPECIALIZE prettyWarning :: Warning -> TCM Doc #-}
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 ( [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 ([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 ( [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 ([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 ( [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 ([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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
      [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"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
$$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"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
$
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unreachable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords (VerboseLevel -> [Char] -> [Char]
forall {a}. (Num a, Eq a) => a -> [Char] -> [Char]
plural ([Range] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Range]
pss) [Char]
"clause")
        where
          plural :: a -> [Char] -> [Char]
plural a
1 [Char]
thing = [Char]
thing
          plural a
n [Char]
thing = [Char]
thing [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"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 (
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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]
++
      [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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 ([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]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Clause] -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
P.singPlural [Clause]
cs [Char]
"clause" [Char]
"clauses") [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 -> [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
$
          [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 -> TCErr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err

    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 [MetaId]
ms -> [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
text [Char]
"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
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

    AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
ps -> [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)"

    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 [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]
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 [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 -> [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
$
      [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
      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
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"because the maximum depth (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> [Char]
forall a. Show a => a -> [Char]
show VerboseLevel
maxDepth [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") has been reached.") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Most likely this means you have an unsatisfiable constraint, but it could" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"also mean that you need to increase the maximum depth using the flag" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"--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 [[Char]]
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
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]
"Cannot set 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
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"with safe flag." ]
      ]

    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 Text
str -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Text -> [Char]
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
$ [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]
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

    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' ]
      HeadSymbolIsProjection 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 projection"
        ]
      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, Semigroup (m Doc), 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 Set 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)", [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((MetaId -> m Doc) -> [MetaId] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM ([MetaId] -> [m Doc]) -> [MetaId] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
ms)
        ]
      BlockedOnProblems Set 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)", [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((ProblemId -> m Doc) -> [ProblemId] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemId -> m Doc
prettyTCM ([ProblemId] -> [m Doc]) -> [ProblemId] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
ps)
        ]
      RequiresDefinitions Set 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", [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM ([QName] -> [m Doc]) -> [QName] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set 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 [Char]
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"
      , [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
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."

    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]
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]
"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 -> [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 LHSOrPatSyn
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"
      , case LHSOrPatSyn
patsyn of
          LHSOrPatSyn
IsPatSyn -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pattern synonym"
          LHSOrPatSyn
IsLHS    -> [ m Doc
"constructor" ]
      ]

    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."

    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
UselessOpaque -> m Doc
"This `opaque` block has no effect."

    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 [(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
  W.TooManyFields 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
    [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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)
    , [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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 [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"field"] [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"fields"]

{-# SPECIALIZE prettyTooManyFields :: QName -> [C.Name] -> [C.Name] -> TCM Doc  #-}
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
    [ [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"
    , [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
      [ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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 [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"field"] [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"fields"]

{-# 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 :: [TCWarning] -> TCM String
prettyTCWarnings :: [TCWarning] -> TCM [Char]
prettyTCWarnings = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char])
-> ([TCWarning] -> TCMT IO [[Char]]) -> [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]])
-> ([TCWarning] -> TCMT IO [Doc])
-> [TCWarning]
-> TCMT IO [[Char]]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m 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], [[Char]])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma [[Char]]
ps -> ([TCWarning
w], [[Char]]
ps); Warning
_ -> ([], []) }
  let sfp :: [TCWarning]
sfp = case ([[Char]] -> [[Char]])
-> ([TCWarning], [[Char]]) -> ([TCWarning], [[Char]])
forall a b. (a -> b) -> ([TCWarning], a) -> ([TCWarning], b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
List.nub ((TCWarning -> ([TCWarning], [[Char]]))
-> [TCWarning] -> ([TCWarning], [[Char]])
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], [[Char]])
pragmas [TCWarning]
ws) of
              (TCWarning CallStack
loc Range
r Warning
w Doc
p Bool
b:[TCWarning]
_, [[Char]]
sfp) ->
                 [CallStack -> Range -> Warning -> Doc -> Bool -> TCWarning
TCWarning CallStack
loc Range
r ([[Char]] -> Warning
SafeFlagPragma [[Char]]
sfp) Doc
p Bool
b]
              ([TCWarning], [[Char]])
_                        -> []

  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

{-# 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 :: (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.

{-# SPECIALIZE getAllWarnings :: WhichWarnings -> TCM [TCWarning] #-}
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

{-# SPECIALIZE getAllWarningsPreserving :: Set WarningName -> WhichWarnings -> TCM [TCWarning] #-}
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 []