[ fix #3199 ] Distinguish imported & local user warnings

The problem with putting (recursively) imported user warnings in the
interface is that they refer to identifiers defined in modules which
are not themselves directly imported. And Agda doesn't know how to
translate these module names to paths during serialization!

We now only put the user warnings defined locally in the interface.

src/full/Agda/Interaction/Imports.hs

@@ -147,9 +147,9 @@ addImportedThings ::
 addImportedThings isig ibuiltin patsyns display userwarn warnings = do
   stImports              %= \ imp -> unionSignatures [imp, isig]
   stImportedBuiltins     %= \ imp -> Map.union imp ibuiltin
+  stImportedUserWarnings %= \ imp -> Map.union imp userwarn
   stPatternSynImports    %= \ imp -> Map.union imp patsyns
   stImportedDisplayForms %= \ imp -> HMap.unionWith (++) imp display
-  stUserWarnings         %= \ imp -> Map.union imp userwarn
   stTCWarnings           %= \ imp -> List.union imp warnings
   addImportedInstances isig
 
@@ -505,7 +505,7 @@ typeCheck x file isMain = do
       isig     <- use stImports
       ibuiltin <- use stImportedBuiltins
       display  <- use stImportsDisplayForms
-      userwarn <- use stUserWarnings
+      userwarn <- use stImportedUserWarnings
       ipatsyns <- getPatternSynImports
       ho       <- getInteractionOutputCallback
       -- Every interface is treated in isolation. Note: Some changes to
@@ -948,7 +948,7 @@ buildInterface file topLevel pragmas = do
     display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms
     -- TODO: Kill some ranges?
     (display, sig) <- eliminateDeadCode display =<< getSignature
-    userwarns <- use stUserWarnings
+    userwarns <- use stLocalUserWarnings
     syntaxInfo <- use stSyntaxInfo
     -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
     -- serialization to avoid error locations pointing to external files

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -535,7 +535,7 @@ instance ToAbstract OldQName A.Expr where
         -- In case we find a defined name, we start by checking whether there's
         -- a warning attached to it
         reportSDoc "scope.warning" 50 $ text $ "Checking usage of " ++ prettyShow d
-        mstr <- Map.lookup (anameName d) <$> use stUserWarnings
+        mstr <- Map.lookup (anameName d) <$> getUserWarnings
         forM_ mstr (warning . UserWarning)
         -- then we take note of generalized names used
         when (anameKind d == GeneralizeName) $ do
@@ -2005,7 +2005,7 @@ instance ToAbstract C.Pragma [A.Pragma] where
 
   toAbstract (C.WarningOnUsage _ oqn str) = do
     qn <- toAbstract $ OldName oqn
-    stUserWarnings %= Map.insert qn str
+    stLocalUserWarnings %= Map.insert qn str
     pure []
 
   -- Termination checking pragmes are handled by the nicifier

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -171,7 +171,10 @@ data PreScopeState = PreScopeState
     -- ^ @{-# FOREIGN #-}@ code that should be included in the compiled output.
     -- Does not include code for imported modules.
   , stPreFreshInteractionId :: !InteractionId
-  , stPreUserWarnings       :: !(Map A.QName String)
+  , stPreImportedUserWarnings :: !(Map A.QName String)
+    -- ^ Imported @UserWarning@s, not to be stored in the @Interface@
+  , stPreLocalUserWarnings    :: !(Map A.QName String)
+    -- ^ Locally defined @UserWarning@s, to be stored in the @Interface@
   }
 
 type DisambiguatedNames = IntMap A.QName
@@ -316,7 +319,8 @@ initPreScopeState = PreScopeState
   , stPreImportedInstanceDefs = Map.empty
   , stPreForeignCode          = Map.empty
   , stPreFreshInteractionId   = 0
-  , stPreUserWarnings         = Map.empty
+  , stPreImportedUserWarnings = Map.empty
+  , stPreLocalUserWarnings    = Map.empty
   }
 
 initPostScopeState :: PostScopeState
@@ -422,10 +426,21 @@ stFreshInteractionId f s =
   f (stPreFreshInteractionId (stPreScopeState s)) <&>
   \x -> s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}}
 
-stUserWarnings :: Lens' (Map A.QName String) TCState
-stUserWarnings f s =
-  f (stPreUserWarnings (stPreScopeState s)) <&>
-  \ x -> s {stPreScopeState = (stPreScopeState s) {stPreUserWarnings = x}}
+stImportedUserWarnings :: Lens' (Map A.QName String) TCState
+stImportedUserWarnings f s =
+  f (stPreImportedUserWarnings (stPreScopeState s)) <&>
+  \ x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedUserWarnings = x}}
+
+stLocalUserWarnings :: Lens' (Map A.QName String) TCState
+stLocalUserWarnings f s =
+  f (stPreLocalUserWarnings (stPreScopeState s)) <&>
+  \ x -> s {stPreScopeState = (stPreScopeState s) {stPreLocalUserWarnings = x}}
+
+getUserWarnings :: MonadState TCState m => m (Map A.QName String)
+getUserWarnings = do
+  iuw <- use stImportedUserWarnings
+  luw <- use stLocalUserWarnings
+  return $ iuw `Map.union` luw
 
 stBackends :: Lens' [Backend] TCState
 stBackends f s =