OptionWarnings are emitted twice

[andreasabel]

OptionWarnings are emitted twice, e.g.: https://github.com/agda/agda/blob/05138510ac152b6fbb6130467502095073ba07cb/test/Succeed/LossyUnification.warn#L1-L6

Suspected reason: We are calling setOptionsFromPragma several times during processing a file. https://github.com/agda/agda/blob/05138510ac152b6fbb6130467502095073ba07cb/src/full/Agda/TypeChecking/Monad/Options.hs#L208-L212

Found while working on:

• 7219

[UlfNorell]

Not sure how it applies to this issue, but in #6640 I had to jump through some hoops to not get the conflicting options warning multiple times:

• Only warn when the pragma options have changed (otherwise you get the same warning for each new OPTIONS pragma in a file) https://github.com/agda/agda/blob/b982f8240a0bbdecb6181a08518f0acf9ea45421/src/full/Agda/TypeChecking/Monad/Options.hs#L69-L71
• Split setOptionsFromPragma into a checking and a non-checking version https://github.com/agda/agda/blob/b982f8240a0bbdecb6181a08518f0acf9ea45421/src/full/Agda/TypeChecking/Monad/Options.hs#L226-L232
• and propagate it to setOptionsFromSourcePragma in Interaction.Imports https://github.com/agda/agda/blob/b982f8240a0bbdecb6181a08518f0acf9ea45421/src/full/Agda/Interaction/Imports.hs#L171-L179
• and only run the check in typeCheckMain and in createInterface for non-main modules (otherwise you get the warning twice for the main module) https://github.com/agda/agda/blob/b982f8240a0bbdecb6181a08518f0acf9ea45421/src/full/Agda/Interaction/Imports.hs#L420-L425 https://github.com/agda/agda/blob/b982f8240a0bbdecb6181a08518f0acf9ea45421/src/full/Agda/Interaction/Imports.hs#L1000-L1004

[andreasabel]

My question here is whether we should dig out the reason why the warning is raised twice, or whether we reorganise the warning store so that duplicate warnings are just stored once. E.g. the warning store could be a map from positions to sets of warnings. (Currently it is a plain list.)