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