1 2module Agda.TypeChecking.Pretty.Warning where 3 4import Prelude hiding ( null ) 5 6import Control.Monad ( guard ) 7 8-- Control.Monad.Fail import is redundant since GHC 8.8.1 9import Control.Monad.Fail ( MonadFail ) 10 11import Data.Char ( toLower ) 12import Data.Function 13import Data.Maybe 14 15import qualified Data.Set as Set 16import Data.Set (Set) 17 18import qualified Data.List as List 19import qualified Data.Text as T 20 21import Agda.TypeChecking.Monad.Base 22import {-# SOURCE #-} Agda.TypeChecking.Errors 23import Agda.TypeChecking.Monad.MetaVars 24import Agda.TypeChecking.Monad.Options 25import Agda.TypeChecking.Monad.Debug 26import Agda.TypeChecking.Monad.State ( getScope ) 27import Agda.TypeChecking.Monad ( localTCState ) 28import Agda.TypeChecking.Positivity () --instance only 29import Agda.TypeChecking.Pretty 30import Agda.TypeChecking.Pretty.Call 31import {-# SOURCE #-} Agda.TypeChecking.Pretty.Constraint (prettyInterestingConstraints, interestingConstraint) 32import Agda.TypeChecking.Warnings (MonadWarning, isUnsolvedWarning, onlyShowIfUnsolved, classifyWarning, WhichWarnings(..), warning_) 33import Agda.TypeChecking.Monad.Constraints (getAllConstraints) 34 35import Agda.Syntax.Common ( ImportedName'(..), fromImportedName, partitionImportedNames ) 36import Agda.Syntax.Position 37import qualified Agda.Syntax.Concrete as C 38import Agda.Syntax.Scope.Base ( concreteNamesInScope, NameOrModule(..) ) 39import Agda.Syntax.Internal 40import Agda.Syntax.Translation.InternalToAbstract 41 42import Agda.Interaction.Options 43import Agda.Interaction.Options.Warnings 44 45import Agda.Utils.Lens 46import Agda.Utils.List ( editDistance ) 47import qualified Agda.Utils.List1 as List1 48import Agda.Utils.Null 49import Agda.Utils.Pretty ( Pretty, prettyShow ) 50import qualified Agda.Utils.Pretty as P 51 52instance PrettyTCM TCWarning where 53 prettyTCM w@(TCWarning loc _ _ _ _) = do 54 reportSLn "warning" 2 $ "Warning raised at " ++ prettyShow loc 55 pure $ tcWarningPrintedWarning w 56 57prettyWarning :: MonadPretty m => Warning -> m Doc 58prettyWarning = \case 59 60 UnsolvedMetaVariables ms -> 61 fsep ( pwords "Unsolved metas at the following locations:" ) 62 $$ nest 2 (vcat $ map prettyTCM ms) 63 64 UnsolvedInteractionMetas is -> 65 fsep ( pwords "Unsolved interaction metas at the following locations:" ) 66 $$ nest 2 (vcat $ map prettyTCM is) 67 68 UnsolvedConstraints cs -> do 69 pcs <- prettyInterestingConstraints cs 70 if null pcs 71 then fsep $ pwords "Unsolved constraints" -- #4065: keep minimal warning text 72 else vcat 73 [ fsep $ pwords "Failed to solve the following constraints:" 74 , nest 2 $ return $ P.vcat $ List.nub pcs 75 ] 76 77 TerminationIssue because -> do 78 dropTopLevel <- topLevelModuleDropper 79 fwords "Termination checking failed for the following functions:" 80 $$ nest 2 (fsep $ punctuate comma $ 81 map (pretty . dropTopLevel) $ 82 concatMap termErrFunctions because) 83 $$ fwords "Problematic calls:" 84 $$ nest 2 (fmap (P.vcat . List.nub) $ 85 mapM prettyTCM $ List.sortBy (compare `on` callInfoRange) $ 86 concatMap termErrCalls because) 87 88 UnreachableClauses f pss -> fsep $ 89 pwords "Unreachable" ++ pwords (plural (length pss) "clause") 90 where 91 plural 1 thing = thing 92 plural n thing = thing ++ "s" 93 94 CoverageIssue f pss -> fsep ( 95 pwords "Incomplete pattern matching for" ++ [prettyTCM f <> "."] ++ 96 pwords "Missing cases:") $$ nest 2 (vcat $ map display pss) 97 where 98 display (tel, ps) = prettyTCM $ NamedClause f True $ 99 empty { clauseTel = tel, namedClausePats = ps } 100 101 CoverageNoExactSplit f cs -> vcat $ 102 fsep (pwords "Exact splitting is enabled, but the following" ++ pwords (P.singPlural cs "clause" "clauses") ++ 103 pwords "could not be preserved as definitional equalities in the translation to a case tree:" 104 ) : 105 map (nest 2 . prettyTCM . NamedClause f True) cs 106 107 NotStrictlyPositive d ocs -> fsep $ 108 [prettyTCM d] ++ pwords "is not strictly positive, because it occurs" 109 ++ [prettyTCM ocs] 110 111 CantGeneralizeOverSorts ms -> vcat 112 [ text "Cannot generalize over unsolved sort metas:" 113 , nest 2 $ vcat [ prettyTCM x <+> text "at" <+> (pretty =<< getMetaRange x) | x <- ms ] 114 , fsep $ pwords "Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any" 115 ] 116 117 AbsurdPatternRequiresNoRHS ps -> fwords $ 118 "The right-hand side must be omitted if there " ++ 119 "is an absurd pattern, () or {}, in the left-hand side." 120 121 OldBuiltin old new -> fwords $ 122 "Builtin " ++ old ++ " no longer exists. " ++ 123 "It is now bound by BUILTIN " ++ new 124 125 EmptyRewritePragma -> fsep . pwords $ "Empty REWRITE pragma" 126 127 EmptyWhere -> fsep . pwords $ "Empty `where' block (ignored)" 128 129 IllformedAsClause s -> fsep . pwords $ 130 "`as' must be followed by an identifier" ++ s 131 132 ClashesViaRenaming nm xs -> fsep $ concat $ 133 [ [ case nm of NameNotModule -> "Name"; ModuleNotName -> "Module" ] 134 , pwords "clashes introduced by `renaming':" 135 , map prettyTCM xs 136 ] 137 138 UselessPatternDeclarationForRecord s -> fwords $ unwords 139 [ "`pattern' attribute ignored for", s, "record" ] 140 141 UselessPublic -> fwords $ "Keyword `public' is ignored here" 142 143 UselessHiding xs -> fsep $ concat 144 [ pwords "Ignoring names in `hiding' directive:" 145 , punctuate "," $ map pretty xs 146 ] 147 148 UselessInline q -> fsep $ 149 pwords "It is pointless for INLINE'd function" ++ [prettyTCM q] ++ 150 pwords "to have a separate Haskell definition" 151 152 WrongInstanceDeclaration -> fwords "Terms marked as eligible for instance search should end with a name, so `instance' is ignored here." 153 154 InstanceWithExplicitArg q -> fsep $ 155 pwords "Instance declarations with explicit arguments are never considered by instance search," ++ 156 pwords "so making" ++ [prettyTCM q] ++ pwords "into an instance has no effect." 157 158 InstanceNoOutputTypeName b -> fsep $ 159 pwords "Instance arguments whose type does not end in a named or variable type are never considered by instance search," ++ 160 pwords "so having an instance argument" ++ [return b] ++ pwords "has no effect." 161 162 InstanceArgWithExplicitArg b -> fsep $ 163 pwords "Instance arguments with explicit arguments are never considered by instance search," ++ 164 pwords "so having an instance argument" ++ [return b] ++ pwords "has no effect." 165 166 InversionDepthReached f -> do 167 maxDepth <- maxInversionDepth 168 fsep $ pwords "Refusing to invert pattern matching of" ++ [prettyTCM f] ++ 169 pwords ("because the maximum depth (" ++ show maxDepth ++ ") has been reached.") ++ 170 pwords "Most likely this means you have an unsatisfiable constraint, but it could" ++ 171 pwords "also mean that you need to increase the maximum depth using the flag" ++ 172 pwords "--inversion-max-depth=N" 173 174 NoGuardednessFlag q -> 175 fsep $ [ prettyTCM q ] ++ pwords "is declared coinductive, but option" ++ 176 pwords "--guardedness is not enabled. Coinductive functions on" ++ 177 pwords "this type will likely be rejected by the termination" ++ 178 pwords "checker unless this flag is enabled." 179 180 GenericWarning d -> return d 181 182 GenericNonFatalError d -> return d 183 184 GenericUseless _r d -> return d 185 186 SafeFlagPostulate e -> fsep $ 187 pwords "Cannot postulate" ++ [pretty e] ++ pwords "with safe flag" 188 189 SafeFlagPragma xs -> 190 let plural | length xs == 1 = "" 191 | otherwise = "s" 192 in fsep $ [fwords ("Cannot set OPTIONS pragma" ++ plural)] 193 ++ map text xs ++ [fwords "with safe flag."] 194 195 SafeFlagNonTerminating -> fsep $ 196 pwords "Cannot use NON_TERMINATING pragma with safe flag." 197 198 SafeFlagTerminating -> fsep $ 199 pwords "Cannot use TERMINATING pragma with safe flag." 200 201 SafeFlagWithoutKFlagPrimEraseEquality -> fsep (pwords "Cannot use primEraseEquality with safe and without-K flags.") 202 203 WithoutKFlagPrimEraseEquality -> fsep (pwords "Using primEraseEquality with the without-K flag is inconsistent.") 204 205 SafeFlagNoPositivityCheck -> fsep $ 206 pwords "Cannot use NO_POSITIVITY_CHECK pragma with safe flag." 207 208 SafeFlagPolarity -> fsep $ 209 pwords "Cannot use POLARITY pragma with safe flag." 210 211 SafeFlagNoUniverseCheck -> fsep $ 212 pwords "Cannot use NO_UNIVERSE_CHECK pragma with safe flag." 213 214 SafeFlagEta -> fsep $ 215 pwords "Cannot use ETA pragma with safe flag." 216 217 SafeFlagInjective -> fsep $ 218 pwords "Cannot use INJECTIVE pragma with safe flag." 219 220 SafeFlagNoCoverageCheck -> fsep $ 221 pwords "Cannot use NON_COVERING pragma with safe flag." 222 223 ParseWarning pw -> pretty pw 224 225 DeprecationWarning old new version -> fsep $ 226 [text old] ++ pwords "has been deprecated. Use" ++ [text new] ++ pwords 227 "instead. This will be an error in Agda" ++ [text version <> "."] 228 229 NicifierIssue w -> sayWhere (getRange w) $ pretty w 230 231 UserWarning str -> text (T.unpack str) 232 233 ModuleDoesntExport m names modules xs -> vcat 234 [ fsep $ pwords "The module" ++ [pretty m] ++ pwords "doesn't export the following:" 235 , prettyNotInScopeNames False (suggestion names) ys 236 , prettyNotInScopeNames False (suggestion modules) ms 237 ] 238 where 239 ys, ms :: [C.ImportedName] 240 ys = map ImportedName ys0 241 ms = map ImportedModule ms0 242 (ys0, ms0) = partitionImportedNames xs 243 suggestion zs = maybe empty parens . didYouMean (map C.QName zs) fromImportedName 244 245 DuplicateUsing xs -> fsep $ pwords "Duplicates in `using` directive:" ++ map pretty (List1.toList xs) 246 247 FixityInRenamingModule _rs -> fsep $ pwords "Modules do not have fixity" 248 249 LibraryWarning lw -> pretty lw 250 251 InfectiveImport o m -> fsep $ 252 pwords "Importing module" ++ [pretty m] ++ pwords "using the" ++ 253 [pretty o] ++ pwords "flag from a module which does not." 254 255 CoInfectiveImport o m -> fsep $ 256 pwords "Importing module" ++ [pretty m] ++ pwords "not using the" ++ 257 [pretty o] ++ pwords "flag from a module which does." 258 259 RewriteNonConfluent lhs rhs1 rhs2 err -> fsep 260 [ "Local confluence check failed:" 261 , prettyTCM lhs , "reduces to both" 262 , prettyTCM rhs1 , "and" , prettyTCM rhs2 263 , "which are not equal because" 264 , return err 265 ] 266 267 RewriteMaybeNonConfluent lhs1 lhs2 cs -> vcat $ concat 268 [ [ fsep $ concat 269 [ pwords "Couldn't determine overlap between left-hand sides" 270 , [ prettyTCM lhs1 , text "and" , prettyTCM lhs2 ] 271 , pwords "because of unsolved constraints:" 272 ] 273 ] 274 , map (nest 2 . return) cs 275 ] 276 277 RewriteAmbiguousRules lhs rhs1 rhs2 -> vcat 278 [ ( fsep $ concat 279 [ pwords "Global confluence check failed:" , [prettyTCM lhs] 280 , pwords "can be rewritten to either" , [prettyTCM rhs1] 281 , pwords "or" , [prettyTCM rhs2 <> "."] 282 ]) 283 , fsep $ concat 284 [ pwords "Possible fix: add a rewrite rule with left-hand side" 285 , [prettyTCM lhs] , pwords "to resolve the ambiguity." 286 ] 287 ] 288 289 RewriteMissingRule u v rhou -> vcat 290 [ fsep $ concat 291 [ pwords "Global confluence check failed:" , [prettyTCM u] 292 , pwords "unfolds to" , [prettyTCM v] , pwords "which should further unfold to" 293 , [prettyTCM rhou] , pwords "but it does not." 294 ] 295 , fsep $ concat 296 [ pwords "Possible fix: add a rule to rewrite" 297 , [ prettyTCM v , "to" , prettyTCM rhou ] 298 ] 299 ] 300 301 PragmaCompileErased bn qn -> fsep $ concat 302 [ pwords "The backend" 303 , [ text bn 304 , "erases" 305 , prettyTCM qn 306 ] 307 , pwords "so the COMPILE pragma will be ignored." 308 ] 309 310 NotInScopeW xs -> vcat 311 [ fsep $ pwords "Not in scope:" 312 , do 313 inscope <- Set.toList . concreteNamesInScope <$> getScope 314 prettyNotInScopeNames True (suggestion inscope) xs 315 ] 316 where 317 suggestion inscope x = nest 2 $ par $ concat 318 [ [ "did you forget space around the ':'?" | ':' `elem` s ] 319 , [ "did you forget space around the '->'?" | "->" `List.isInfixOf` s ] 320 , maybeToList $ didYouMean inscope C.unqualify x 321 ] 322 where 323 par [] = empty 324 par [d] = parens d 325 par ds = parens $ vcat ds 326 s = P.prettyShow x 327 328 AsPatternShadowsConstructorOrPatternSynonym patsyn -> fsep $ concat 329 [ pwords "Name bound in @-pattern ignored because it shadows" 330 , if patsyn then pwords "pattern synonym" else [ "constructor" ] 331 ] 332 333 RecordFieldWarning w -> prettyRecordFieldWarning w 334 335prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc 336prettyRecordFieldWarning = \case 337 DuplicateFieldsWarning xrs -> prettyDuplicateFields $ map fst xrs 338 TooManyFieldsWarning q ys xrs -> prettyTooManyFields q ys $ map fst xrs 339 340prettyDuplicateFields :: MonadPretty m => [C.Name] -> m Doc 341prettyDuplicateFields xs = fsep $ concat 342 [ pwords "Duplicate" 343 , fields xs 344 , punctuate comma (map pretty xs) 345 , pwords "in record" 346 ] 347 where 348 fields ys = P.singPlural ys [text "field"] [text "fields"] 349 350prettyTooManyFields :: MonadPretty m => QName -> [C.Name] -> [C.Name] -> m Doc 351prettyTooManyFields r missing xs = fsep $ concat 352 [ pwords "The record type" 353 , [prettyTCM r] 354 , pwords "does not have the" 355 , fields xs 356 , punctuate comma (map pretty xs) 357 , if null missing then [] else concat 358 [ pwords "but it would have the" 359 , fields missing 360 , punctuate comma (map pretty missing) 361 ] 362 ] 363 where 364 fields ys = P.singPlural ys [text "field"] [text "fields"] 365 366-- | Report a number of names that are not in scope. 367prettyNotInScopeNames 368 :: (MonadPretty m, Pretty a, HasRange a) 369 => Bool -- ^ Print range? 370 -> (a -> m Doc) -- ^ Correction suggestion generator. 371 -> [a] -- ^ Names that are not in scope. 372 -> m Doc 373prettyNotInScopeNames printRange suggestion xs = nest 2 $ vcat $ map name xs 374 where 375 name x = fsep 376 [ pretty x 377 , if printRange then "at" <+> prettyTCM (getRange x) else empty 378 , suggestion x 379 ] 380 381-- | Suggest some corrections to a misspelled name. 382didYouMean 383 :: (MonadPretty m, Pretty a, Pretty b) 384 => [C.QName] -- ^ Names in scope. 385 -> (a -> b) -- ^ Canonization function for similarity search. 386 -> a -- ^ A name which is not in scope. 387 -> Maybe (m Doc) -- ^ "did you mean" hint. 388didYouMean inscope canon x 389 | null ys = Nothing 390 | otherwise = Just $ sep 391 [ "did you mean" 392 , nest 2 (vcat $ punctuate " or" $ 393 map (\ y -> text $ "'" ++ y ++ "'") ys) 394 <> "?" 395 ] 396 where 397 strip :: Pretty b => b -> String 398 strip = map toLower . filter (/= '_') . prettyShow 399 -- dropModule x = fromMaybe x $ List.stripPrefix "module " x 400 maxDist n = div n 3 401 close a b = editDistance a b <= maxDist (length a) 402 ys = map prettyShow $ filter (close (strip $ canon x) . strip . C.unqualify) inscope 403 404 405prettyTCWarnings :: [TCWarning] -> TCM String 406prettyTCWarnings = fmap (unlines . List.intersperse "") . prettyTCWarnings' 407 408prettyTCWarnings' :: [TCWarning] -> TCM [String] 409prettyTCWarnings' = mapM (fmap P.render . prettyTCM) . filterTCWarnings 410 411-- | If there are several warnings, remove the unsolved-constraints warning 412-- in case there are no interesting constraints to list. 413filterTCWarnings :: [TCWarning] -> [TCWarning] 414filterTCWarnings = \case 415 -- #4065: Always keep the only warning 416 [w] -> [w] 417 -- Andreas, 2019-09-10, issue #4065: 418 -- If there are several warnings, remove the unsolved-constraints warning 419 -- in case there are no interesting constraints to list. 420 ws -> (`filter` ws) $ \ w -> case tcWarning w of 421 UnsolvedConstraints cs -> any interestingConstraint cs 422 _ -> True 423 424 425-- | Turns warnings, if any, into errors. 426tcWarningsToError :: [TCWarning] -> TCM () 427tcWarningsToError mws = case (unsolvedHoles, otherWarnings) of 428 ([], []) -> return () 429 (_unsolvedHoles@(_:_), []) -> typeError SolvedButOpenHoles 430 (_, ws@(_:_)) -> typeError $ NonFatalErrors ws 431 where 432 -- filter out unsolved interaction points for imported module so 433 -- that we get the right error message (see test case Fail/Issue1296) 434 (unsolvedHoles, otherWarnings) = List.partition (isUnsolvedIM . tcWarning) mws 435 isUnsolvedIM UnsolvedInteractionMetas{} = True 436 isUnsolvedIM _ = False 437 438 439-- | Depending which flags are set, one may happily ignore some 440-- warnings. 441 442applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning] 443applyFlagsToTCWarningsPreserving additionalKeptWarnings ws = do 444 -- For some reason some SafeFlagPragma seem to be created multiple times. 445 -- This is a way to collect all of them and remove duplicates. 446 let pragmas w = case tcWarning w of { SafeFlagPragma ps -> ([w], ps); _ -> ([], []) } 447 let sfp = case fmap List.nub (foldMap pragmas ws) of 448 (TCWarning loc r w p b:_, sfp) -> 449 [TCWarning loc r (SafeFlagPragma sfp) p b] 450 _ -> [] 451 452 pragmaWarnings <- (^. warningSet) . optWarningMode <$> pragmaOptions 453 let warnSet = Set.union pragmaWarnings additionalKeptWarnings 454 455 -- filter out the warnings the flags told us to ignore 456 let cleanUp w = let wName = warningName w in 457 wName /= SafeFlagPragma_ 458 && wName `Set.member` warnSet 459 && case w of 460 UnsolvedMetaVariables ums -> not $ null ums 461 UnsolvedInteractionMetas uis -> not $ null uis 462 UnsolvedConstraints ucs -> not $ null ucs 463 _ -> True 464 465 return $ sfp ++ filter (cleanUp . tcWarning) ws 466 467applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning] 468applyFlagsToTCWarnings = applyFlagsToTCWarningsPreserving Set.empty 469 470getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning] 471getAllUnsolvedWarnings = do 472 unsolvedInteractions <- getUnsolvedInteractionMetas 473 unsolvedConstraints <- getAllConstraints 474 unsolvedMetas <- getUnsolvedMetas 475 476 let checkNonEmpty c rs = c rs <$ guard (not $ null rs) 477 478 mapM warning_ $ catMaybes 479 [ checkNonEmpty UnsolvedInteractionMetas unsolvedInteractions 480 , checkNonEmpty UnsolvedMetaVariables unsolvedMetas 481 , checkNonEmpty UnsolvedConstraints unsolvedConstraints ] 482 483-- | Collect all warnings that have accumulated in the state. 484 485getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning] 486getAllWarnings = getAllWarningsPreserving Set.empty 487 488getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning] 489getAllWarningsPreserving keptWarnings ww = do 490 unsolved <- getAllUnsolvedWarnings 491 collectedTCWarnings <- useTC stTCWarnings 492 493 let showWarn w = classifyWarning w <= ww && 494 not (null unsolved && onlyShowIfUnsolved w) 495 496 fmap (filter (showWarn . tcWarning)) 497 $ applyFlagsToTCWarningsPreserving keptWarnings 498 $ reverse $ unsolved ++ collectedTCWarnings 499 500getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning] 501getAllWarningsOfTCErr err = case err of 502 TypeError _ tcst cls -> case clValue cls of 503 NonFatalErrors{} -> return [] 504 _ -> localTCState $ do 505 putTC tcst 506 ws <- getAllWarnings AllWarnings 507 -- We filter out the unsolved(Metas/Constraints) to stay 508 -- true to the previous error messages. 509 return $ filter (not . isUnsolvedWarning . tcWarning) ws 510 _ -> return [] 511