1module Agda.Syntax.Concrete.Definitions.Errors where 2 3import Control.DeepSeq 4 5import Data.Data 6 7import GHC.Generics (Generic) 8 9import Agda.Syntax.Position 10import Agda.Syntax.Concrete 11import Agda.Syntax.Concrete.Name 12import Agda.Syntax.Concrete.Definitions.Types 13 14import Agda.Interaction.Options.Warnings 15 16import Agda.Utils.CallStack ( CallStack ) 17import Agda.Utils.List1 (List1, pattern (:|)) 18import Agda.Utils.List2 (List2, pattern List2) 19import qualified Agda.Utils.List1 as List1 20import Agda.Utils.Pretty 21 22------------------------------------------------------------------------ 23-- Errors 24 25-- | Exception with internal source code callstack 26data DeclarationException = DeclarationException 27 { deLocation :: CallStack 28 , deException :: DeclarationException' 29 } 30 31-- | The exception type. 32data DeclarationException' 33 = MultipleEllipses Pattern 34 | InvalidName Name 35 | DuplicateDefinition Name 36 | DuplicateAnonDeclaration Range 37 | MissingWithClauses Name LHS 38 | WrongDefinition Name DataRecOrFun DataRecOrFun 39 | DeclarationPanic String 40 | WrongContentBlock KindOfBlock Range 41 | AmbiguousFunClauses LHS (List1 Name) 42 -- ^ In a mutual block, a clause could belong to any of the ≥2 type signatures ('Name'). 43 | AmbiguousConstructor Range Name [Name] 44 -- ^ In an interleaved mutual block, a constructor could belong to any of the data signatures ('Name') 45 | InvalidMeasureMutual Range 46 -- ^ In a mutual block, all or none need a MEASURE pragma. 47 -- Range is of mutual block. 48 | UnquoteDefRequiresSignature (List1 Name) 49 | BadMacroDef NiceDeclaration 50 deriving (Data, Show) 51 52------------------------------------------------------------------------ 53-- Warnings 54 55data DeclarationWarning = DeclarationWarning 56 { dwLocation :: CallStack 57 , dwWarning :: DeclarationWarning' 58 } deriving (Show, Generic) 59 60-- | Non-fatal errors encountered in the Nicifier. 61data DeclarationWarning' 62 -- Please keep in alphabetical order. 63 = EmptyAbstract Range -- ^ Empty @abstract@ block. 64 | EmptyConstructor Range -- ^ Empty @constructor@ block. 65 | EmptyField Range -- ^ Empty @field@ block. 66 | EmptyGeneralize Range -- ^ Empty @variable@ block. 67 | EmptyInstance Range -- ^ Empty @instance@ block 68 | EmptyMacro Range -- ^ Empty @macro@ block. 69 | EmptyMutual Range -- ^ Empty @mutual@ block. 70 | EmptyPostulate Range -- ^ Empty @postulate@ block. 71 | EmptyPrivate Range -- ^ Empty @private@ block. 72 | EmptyPrimitive Range -- ^ Empty @primitive@ block. 73 | InvalidCatchallPragma Range 74 -- ^ A {-\# CATCHALL \#-} pragma 75 -- that does not precede a function clause. 76 | InvalidConstructor Range 77 -- ^ Invalid definition in a constructor block 78 | InvalidConstructorBlock Range 79 -- ^ Invalid constructor block (not inside an interleaved mutual block) 80 | InvalidCoverageCheckPragma Range 81 -- ^ A {-\# NON_COVERING \#-} pragma that does not apply to any function. 82 | InvalidNoPositivityCheckPragma Range 83 -- ^ A {-\# NO_POSITIVITY_CHECK \#-} pragma 84 -- that does not apply to any data or record type. 85 | InvalidNoUniverseCheckPragma Range 86 -- ^ A {-\# NO_UNIVERSE_CHECK \#-} pragma 87 -- that does not apply to a data or record type. 88 | InvalidRecordDirective Range 89 -- ^ A record directive outside of a record / below existing fields. 90 | InvalidTerminationCheckPragma Range 91 -- ^ A {-\# TERMINATING \#-} and {-\# NON_TERMINATING \#-} pragma 92 -- that does not apply to any function. 93 | MissingDefinitions [(Name, Range)] 94 -- ^ Declarations (e.g. type signatures) without a definition. 95 | NotAllowedInMutual Range String 96 | OpenPublicPrivate Range 97 -- ^ @private@ has no effect on @open public@. (But the user might think so.) 98 | OpenPublicAbstract Range 99 -- ^ @abstract@ has no effect on @open public@. (But the user might think so.) 100 | PolarityPragmasButNotPostulates [Name] 101 | PragmaNoTerminationCheck Range 102 -- ^ Pragma @{-\# NO_TERMINATION_CHECK \#-}@ has been replaced 103 -- by @{-\# TERMINATING \#-}@ and @{-\# NON_TERMINATING \#-}@. 104 | PragmaCompiled Range 105 -- ^ @COMPILE@ pragmas are not allowed in safe mode 106 | ShadowingInTelescope (List1 (Name, List2 Range)) 107 | UnknownFixityInMixfixDecl [Name] 108 | UnknownNamesInFixityDecl [Name] 109 | UnknownNamesInPolarityPragmas [Name] 110 | UselessAbstract Range 111 -- ^ @abstract@ block with nothing that can (newly) be made abstract. 112 | UselessInstance Range 113 -- ^ @instance@ block with nothing that can (newly) become an instance. 114 | UselessPrivate Range 115 -- ^ @private@ block with nothing that can (newly) be made private. 116 deriving (Data, Show, Generic) 117 118declarationWarningName :: DeclarationWarning -> WarningName 119declarationWarningName = declarationWarningName' . dwWarning 120 121declarationWarningName' :: DeclarationWarning' -> WarningName 122declarationWarningName' = \case 123 -- Please keep in alphabetical order. 124 EmptyAbstract{} -> EmptyAbstract_ 125 EmptyConstructor{} -> EmptyConstructor_ 126 EmptyField{} -> EmptyField_ 127 EmptyGeneralize{} -> EmptyGeneralize_ 128 EmptyInstance{} -> EmptyInstance_ 129 EmptyMacro{} -> EmptyMacro_ 130 EmptyMutual{} -> EmptyMutual_ 131 EmptyPrivate{} -> EmptyPrivate_ 132 EmptyPostulate{} -> EmptyPostulate_ 133 EmptyPrimitive{} -> EmptyPrimitive_ 134 InvalidCatchallPragma{} -> InvalidCatchallPragma_ 135 InvalidConstructor{} -> InvalidConstructor_ 136 InvalidConstructorBlock{} -> InvalidConstructorBlock_ 137 InvalidNoPositivityCheckPragma{} -> InvalidNoPositivityCheckPragma_ 138 InvalidNoUniverseCheckPragma{} -> InvalidNoUniverseCheckPragma_ 139 InvalidRecordDirective{} -> InvalidRecordDirective_ 140 InvalidTerminationCheckPragma{} -> InvalidTerminationCheckPragma_ 141 InvalidCoverageCheckPragma{} -> InvalidCoverageCheckPragma_ 142 MissingDefinitions{} -> MissingDefinitions_ 143 NotAllowedInMutual{} -> NotAllowedInMutual_ 144 OpenPublicPrivate{} -> OpenPublicPrivate_ 145 OpenPublicAbstract{} -> OpenPublicAbstract_ 146 PolarityPragmasButNotPostulates{} -> PolarityPragmasButNotPostulates_ 147 PragmaNoTerminationCheck{} -> PragmaNoTerminationCheck_ 148 PragmaCompiled{} -> PragmaCompiled_ 149 ShadowingInTelescope{} -> ShadowingInTelescope_ 150 UnknownFixityInMixfixDecl{} -> UnknownFixityInMixfixDecl_ 151 UnknownNamesInFixityDecl{} -> UnknownNamesInFixityDecl_ 152 UnknownNamesInPolarityPragmas{} -> UnknownNamesInPolarityPragmas_ 153 UselessAbstract{} -> UselessAbstract_ 154 UselessInstance{} -> UselessInstance_ 155 UselessPrivate{} -> UselessPrivate_ 156 157-- | Nicifier warnings turned into errors in @--safe@ mode. 158unsafeDeclarationWarning :: DeclarationWarning -> Bool 159unsafeDeclarationWarning = unsafeDeclarationWarning' . dwWarning 160 161unsafeDeclarationWarning' :: DeclarationWarning' -> Bool 162unsafeDeclarationWarning' = \case 163 -- Please keep in alphabetical order. 164 EmptyAbstract{} -> False 165 EmptyConstructor{} -> False 166 EmptyField{} -> False 167 EmptyGeneralize{} -> False 168 EmptyInstance{} -> False 169 EmptyMacro{} -> False 170 EmptyMutual{} -> False 171 EmptyPrivate{} -> False 172 EmptyPostulate{} -> False 173 EmptyPrimitive{} -> False 174 InvalidCatchallPragma{} -> False 175 InvalidConstructor{} -> False 176 InvalidConstructorBlock{} -> False 177 InvalidNoPositivityCheckPragma{} -> False 178 InvalidNoUniverseCheckPragma{} -> False 179 InvalidRecordDirective{} -> False 180 InvalidTerminationCheckPragma{} -> False 181 InvalidCoverageCheckPragma{} -> False 182 MissingDefinitions{} -> True -- not safe 183 NotAllowedInMutual{} -> False -- really safe? 184 OpenPublicPrivate{} -> False 185 OpenPublicAbstract{} -> False 186 PolarityPragmasButNotPostulates{} -> False 187 PragmaNoTerminationCheck{} -> True -- not safe 188 PragmaCompiled{} -> True -- not safe 189 ShadowingInTelescope{} -> False 190 UnknownFixityInMixfixDecl{} -> False 191 UnknownNamesInFixityDecl{} -> False 192 UnknownNamesInPolarityPragmas{} -> False 193 UselessAbstract{} -> False 194 UselessInstance{} -> False 195 UselessPrivate{} -> False 196 197------------------------------------------------------------------------ 198-- Instances 199 200instance HasRange DeclarationException where 201 getRange (DeclarationException _ err) = getRange err 202 203instance HasRange DeclarationException' where 204 getRange (MultipleEllipses d) = getRange d 205 getRange (InvalidName x) = getRange x 206 getRange (DuplicateDefinition x) = getRange x 207 getRange (DuplicateAnonDeclaration r) = r 208 getRange (MissingWithClauses x lhs) = getRange lhs 209 getRange (WrongDefinition x k k') = getRange x 210 getRange (AmbiguousFunClauses lhs xs) = getRange lhs 211 getRange (AmbiguousConstructor r _ _) = r 212 getRange (DeclarationPanic _) = noRange 213 getRange (WrongContentBlock _ r) = r 214 getRange (InvalidMeasureMutual r) = r 215 getRange (UnquoteDefRequiresSignature x) = getRange x 216 getRange (BadMacroDef d) = getRange d 217 218instance HasRange DeclarationWarning where 219 getRange (DeclarationWarning _ w) = getRange w 220 221instance HasRange DeclarationWarning' where 222 getRange (UnknownNamesInFixityDecl xs) = getRange xs 223 getRange (UnknownFixityInMixfixDecl xs) = getRange xs 224 getRange (UnknownNamesInPolarityPragmas xs) = getRange xs 225 getRange (PolarityPragmasButNotPostulates xs) = getRange xs 226 getRange (MissingDefinitions xs) = getRange xs 227 getRange (UselessPrivate r) = r 228 getRange (NotAllowedInMutual r x) = r 229 getRange (UselessAbstract r) = r 230 getRange (UselessInstance r) = r 231 getRange (EmptyConstructor r) = r 232 getRange (EmptyMutual r) = r 233 getRange (EmptyAbstract r) = r 234 getRange (EmptyPrivate r) = r 235 getRange (EmptyInstance r) = r 236 getRange (EmptyMacro r) = r 237 getRange (EmptyPostulate r) = r 238 getRange (EmptyGeneralize r) = r 239 getRange (EmptyPrimitive r) = r 240 getRange (EmptyField r) = r 241 getRange (InvalidTerminationCheckPragma r) = r 242 getRange (InvalidCoverageCheckPragma r) = r 243 getRange (InvalidNoPositivityCheckPragma r) = r 244 getRange (InvalidCatchallPragma r) = r 245 getRange (InvalidConstructor r) = r 246 getRange (InvalidConstructorBlock r) = r 247 getRange (InvalidNoUniverseCheckPragma r) = r 248 getRange (InvalidRecordDirective r) = r 249 getRange (PragmaNoTerminationCheck r) = r 250 getRange (PragmaCompiled r) = r 251 getRange (OpenPublicAbstract r) = r 252 getRange (OpenPublicPrivate r) = r 253 getRange (ShadowingInTelescope ns) = getRange ns 254 255-- These error messages can (should) be terminated by a dot ".", 256-- there is no error context printed after them. 257instance Pretty DeclarationException' where 258 pretty (MultipleEllipses p) = fsep $ 259 pwords "Multiple ellipses in left-hand side" ++ [pretty p] 260 pretty (InvalidName x) = fsep $ 261 pwords "Invalid name:" ++ [pretty x] 262 pretty (DuplicateDefinition x) = fsep $ 263 pwords "Duplicate definition of" ++ [pretty x] 264 pretty (DuplicateAnonDeclaration _) = fsep $ 265 pwords "Duplicate declaration of _" 266 pretty (MissingWithClauses x lhs) = fsep $ 267 pwords "Missing with-clauses for function" ++ [pretty x] 268 269 pretty (WrongDefinition x k k') = fsep $ pretty x : 270 pwords ("has been declared as a " ++ prettyShow k ++ 271 ", but is being defined as a " ++ prettyShow k') 272 pretty (AmbiguousFunClauses lhs xs) = sep 273 [ fsep $ 274 pwords "More than one matching type signature for left hand side " ++ [pretty lhs] ++ 275 pwords "it could belong to any of:" 276 , vcat $ fmap (pretty . PrintRange) xs 277 ] 278 pretty (AmbiguousConstructor _ n ns) = sep 279 [ fsep (pwords "Could not find a matching data signature for constructor " ++ [pretty n]) 280 , vcat (case ns of 281 [] -> [fsep $ pwords "There was no candidate."] 282 _ -> fsep (pwords "It could be any of:") : fmap (pretty . PrintRange) ns 283 ) 284 ] 285 pretty (WrongContentBlock b _) = fsep . pwords $ 286 case b of 287 PostulateBlock -> "A postulate block can only contain type signatures, possibly under keyword instance" 288 DataBlock -> "A data definition can only contain type signatures, possibly under keyword instance" 289 _ -> "Unexpected declaration" 290 pretty (InvalidMeasureMutual _) = fsep $ 291 pwords "In a mutual block, either all functions must have the same (or no) termination checking pragma." 292 pretty (UnquoteDefRequiresSignature xs) = fsep $ 293 pwords "Missing type signatures for unquoteDef" ++ map pretty (List1.toList xs) 294 pretty (BadMacroDef nd) = fsep $ 295 text (declName nd) : pwords "are not allowed in macro blocks" 296 pretty (DeclarationPanic s) = text s 297 298instance Pretty DeclarationWarning where 299 pretty (DeclarationWarning _ w) = pretty w 300 301instance Pretty DeclarationWarning' where 302 pretty (UnknownNamesInFixityDecl xs) = fsep $ 303 pwords "The following names are not declared in the same scope as their syntax or fixity declaration (i.e., either not in scope at all, imported from another module, or declared in a super module):" 304 ++ punctuate comma (map pretty xs) 305 pretty (UnknownFixityInMixfixDecl xs) = fsep $ 306 pwords "The following mixfix names do not have an associated fixity declaration:" 307 ++ punctuate comma (map pretty xs) 308 pretty (UnknownNamesInPolarityPragmas xs) = fsep $ 309 pwords "The following names are not declared in the same scope as their polarity pragmas (they could for instance be out of scope, imported from another module, or declared in a super module):" 310 ++ punctuate comma (map pretty xs) 311 pretty (MissingDefinitions xs) = fsep $ 312 pwords "The following names are declared but not accompanied by a definition:" 313 ++ punctuate comma (map (pretty . fst) xs) 314 pretty (NotAllowedInMutual r nd) = fsep $ 315 text nd : pwords "in mutual blocks are not supported. Suggestion: get rid of the mutual block by manually ordering declarations" 316 pretty (PolarityPragmasButNotPostulates xs) = fsep $ 317 pwords "Polarity pragmas have been given for the following identifiers which are not postulates:" 318 ++ punctuate comma (map pretty xs) 319 pretty (UselessPrivate _) = fsep $ 320 pwords "Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations." 321 pretty (UselessAbstract _) = fsep $ 322 pwords "Using abstract here has no effect. Abstract applies to only definitions like data definitions, record type definitions and function clauses." 323 pretty (UselessInstance _) = fsep $ 324 pwords "Using instance here has no effect. Instance applies only to declarations that introduce new identifiers into the module, like type signatures and axioms." 325 pretty (EmptyMutual _) = fsep $ pwords "Empty mutual block." 326 pretty EmptyConstructor{} = fsep $ pwords "Empty constructor block." 327 pretty (EmptyAbstract _) = fsep $ pwords "Empty abstract block." 328 pretty (EmptyPrivate _) = fsep $ pwords "Empty private block." 329 pretty (EmptyInstance _) = fsep $ pwords "Empty instance block." 330 pretty (EmptyMacro _) = fsep $ pwords "Empty macro block." 331 pretty (EmptyPostulate _) = fsep $ pwords "Empty postulate block." 332 pretty (EmptyGeneralize _) = fsep $ pwords "Empty variable block." 333 pretty (EmptyPrimitive _) = fsep $ pwords "Empty primitive block." 334 pretty (EmptyField _) = fsep $ pwords "Empty field block." 335 pretty InvalidRecordDirective{} = fsep $ 336 pwords "Record directives can only be used inside record definitions and before field declarations." 337 pretty (InvalidTerminationCheckPragma _) = fsep $ 338 pwords "Termination checking pragmas can only precede a function definition or a mutual block (that contains a function definition)." 339 pretty InvalidConstructor{} = fsep $ 340 pwords "`constructor' blocks may only contain type signatures for constructors." 341 pretty InvalidConstructorBlock{} = fsep $ 342 pwords "No `constructor' blocks outside of `interleaved mutual' blocks." 343 pretty (InvalidCoverageCheckPragma _) = fsep $ 344 pwords "Coverage checking pragmas can only precede a function definition or a mutual block (that contains a function definition)." 345 pretty (InvalidNoPositivityCheckPragma _) = fsep $ 346 pwords "NO_POSITIVITY_CHECKING pragmas can only precede a data/record definition or a mutual block (that contains a data/record definition)." 347 pretty (InvalidCatchallPragma _) = fsep $ 348 pwords "The CATCHALL pragma can only precede a function clause." 349 pretty (InvalidNoUniverseCheckPragma _) = fsep $ 350 pwords "NO_UNIVERSE_CHECKING pragmas can only precede a data/record definition." 351 pretty (PragmaNoTerminationCheck _) = fsep $ 352 pwords "Pragma {-# NO_TERMINATION_CHECK #-} has been removed. To skip the termination check, label your definitions either as {-# TERMINATING #-} or {-# NON_TERMINATING #-}." 353 pretty (PragmaCompiled _) = fsep $ 354 pwords "COMPILE pragma not allowed in safe mode." 355 pretty (OpenPublicAbstract _) = fsep $ 356 pwords "public does not have any effect in an abstract block." 357 pretty (OpenPublicPrivate _) = fsep $ 358 pwords "public does not have any effect in a private block." 359 pretty (ShadowingInTelescope nrs) = fsep $ 360 pwords "Shadowing in telescope, repeated variable names:" 361 ++ punctuate comma (fmap (pretty . fst) nrs) 362 363instance NFData DeclarationWarning 364instance NFData DeclarationWarning' 365