Error message for duplicate module definition points to external module instead of internal module

[GoogleCodeExporter]

That's a strange one. Consider

  open import Common.Size as L
  import Common.Size as M

  private open module L = M

This reports correctly

  Duplicate definition of module L.

Now change L to N (coming after M in the alphabet).

  open import Common.Size as N
  import Common.Size as M

  private open module N = M

Suddenly, innocent M is blamed:

  Duplicate definition of module M.

Agda is a bitch. Always putting blame on the lower modules.

Original issue reported on code.google.com by andreas....@gmail.com on 18 Oct 2012 at 10:40

[GoogleCodeExporter]

Funny how this error message is created: Just the abstract name 'Common.Size' is reported to the error printer, who tries to recover the concrete name using inverseScopeLookup. This function takes the 'best' match

   best $ filter unambiguousModule $ findModule m

    best xs = case sortBy (compare `on` len) xs of
      []    -> Nothing
      x : _ -> Just x

where 'best' ignores whether there are several best matches.

I do not understand why the offending concrete name is not simply passed to the error reporter. Well, I'll try to change this and find out what happens...

Original comment by andreas....@gmail.com on 18 Oct 2012 at 11:21

[GoogleCodeExporter]

Nothing happened. I fixed the bug.

Original comment by andreas....@gmail.com on 18 Oct 2012 at 11:40

• Changed state: Fixed

[GoogleCodeExporter]

The error message is still not nice:

  import Common.Size as A
  module M where

  private open module A = M

-- Duplicate definition of module A. Previous definition of module A
-- at /Users/abel/cover/alfa/Agda2-clean/test/Common/Size.agda:7,15-19
-- when scope checking the declaration
--   open module A = M

Should not the duplicate definition be in the import statement? But the 'best' match, used by the printer from Concrete to Abstract, is the original definition of the module Common.Size that is aliased to A.

Original comment by andreas....@gmail.com on 19 Oct 2012 at 12:18

• Changed title: Error message for duplicate module definition points to external module instead of internal module
• Changed state: Accepted

[andreasabel]

This is related to #2619.

[andreasabel]

Mmh, can fix it by setting the definition site of the imported module Common.Size to the range of the first A. However, then clicking on Common.Size does no longer jump to this module.

diff --git a/src/full/Agda/Syntax/Abstract/Name.hs b/src/full/Agda/Syntax/Abstract/Name.hs
index 6e735c0..8b68693 100644
--- a/src/full/Agda/Syntax/Abstract/Name.hs
+++ b/src/full/Agda/Syntax/Abstract/Name.hs
@@ -366,6 +366,23 @@ instance KillRange QName where
 instance KillRange AmbiguousQName where
   killRange (AmbQ xs) = AmbQ $ killRange xs
 
+-- ** Set @nameBindingSite@
+
+class SetBindingSite a where
+  setBindingSite :: Range -> a -> a
+
+instance SetBindingSite Name where
+  setBindingSite r x = x { nameBindingSite = r }
+
+-- | Is is sufficient to set the binding site of the last @Name@?
+instance SetBindingSite ModuleName where
+  setBindingSite r (MName xs) = MName $ updateLast (setBindingSite r) xs
+
+-- | Is is sufficient to set the binding site of the @Name@?
+instance SetBindingSite QName where
+  setBindingSite r (QName m n) = QName m $ setBindingSite r n
+
+
 ------------------------------------------------------------------------
 -- * Sized instances
 ------------------------------------------------------------------------
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index f5dc329..1d0e1c6 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -1490,9 +1490,15 @@ instance ToAbstract NiceDeclaration A.Declaration where
         printScope "import" 10 "before import:"
         (m, i) <- scopeCheckImport m
         printScope "import" 10 $ "scope checked import: " ++ show i
+
+        -- Andreas, 2017-07-28, issue #719
+        -- In case we have imported the module with an @as@-clause,
+        -- set the binding site to that @as@-name for better error reporting.
+        let m' = caseMaybe as m $ \ (AsName y _) -> setBindingSite (getRange y) m
+
         -- We don't want the top scope of the imported module (things happening
         -- before the module declaration)
-        return (m, Map.delete noModuleName i)
+        return (m', Map.delete noModuleName i)
 
       -- Merge the imported scopes with the current scopes
       modifyScopes $ \ ms -> Map.unionWith mergeScope (Map.delete m ms) i

It seems that some infrastructure is needed here. Currently, the first A is only a concrete name linking to the abstract name of Common.Size. We basically have two concrete names pointing to the same abstract name, and only abstract names carry nameBindingSites. Thus, with the current infrastructure, this seems unsolvable. We need something like module aliases on the Syntax.Abstract level. (That could also alleviate the module copying problem, see #1646.)

[andreasabel]

Here is another idea for a fix (see original example). Upon the new definition of concrete L we are checking whether L is defined already, and yes, it points to abstract Common.Size. Using inverseScopeLookup we find that abstract Common.Size is referenced by concrete Common.Size, M, and L. Filtering for L we should get a concrete L whose range we can use for the error location. If not, we take the binding site of abstract Common.Size.

[andreasabel]

Ok the last proposal actually worked for the error message.

    ShadowedModule x ms@(m0 : _) -> do
      -- Clash! Concrete module name x already points to the abstract names ms.
      (r, m) <- do
        -- Andreas, 2017-07-28, issue #719.
        -- First, we try to find whether one of the abstract names @ms@ points back to @x@
        scope <- getScope
        -- Get all pairs (y,m) such that y points to some m ∈ ms.
        let xms0 = ms >>= \ m -> map (,m) $ inverseScopeLookupModule m scope
        reportSLn "scope.clash.error" 30 $ "candidates = " ++ prettyShow xms0

        -- Try to find x (which will have a different Range, if it has one (#2649)).
        let xms = filter ((\ y -> not (null $ getRange y) && y == C.QName x) . fst) xms0
        reportSLn "scope.class.error" 30 $ "filtered candidates = " ++ prettyShow xms

        -- If we found a copy of x with non-empty range, great!
        ifJust (headMaybe xms) (\ (x', m) -> return (getRange x', m)) $ {-else-} do

        -- If that failed, we pick the first m from ms which has a nameBindingSite.
        let rms = ms >>= \ m -> map (,m) $
              filter (noRange /=) $ map nameBindingSite $ reverse $ mnameToList m
              -- Andreas, 2017-07-25, issue #2649
              -- Take the first nameBindingSite we can get hold of.
        reportSLn "scope.class.error" 30 $ "rangeful clashing modules = " ++ prettyShow rms

        -- If even this fails, we pick the first m and give no range.
        return $ fromMaybe (noRange, m0) $ headMaybe rms

      fsep $
        pwords "Duplicate definition of module" ++ [prettyTCM x <> text "."] ++
        pwords "Previous definition of" ++ [help m] ++ pwords "module" ++ [prettyTCM x] ++
        pwords "at" ++ [prettyTCM r]
      where
        help m = caseMaybeM (isDatatypeModule m) empty $ \case
          IsData   -> text "(datatype)"
          IsRecord -> text "(record)"

However, if we want to jump the defining import of a module/identifier (rather than into the imported module), as wished in #2619, the same trick does not work. We might need binding sites in concrete names or some magic in Highlighting.Generate.