Check module equality before issuing "Ambiguous name" error #6035

anuyts · 2022-08-18T13:55:49Z

When I use a defined name A that corresponds to multiple definitions, Agda issues an "Ambiguous name" error. However, if the definitions are actually the same piece of code but accessed through different open or open import statements and the module of A is moreover instantiated each time with the same arguments, then there is no ambiguity and A should simply be used.

Either of the following solutions could work:

before reporting ambiguity, check whether all definitions are actually in the same place in the code and their parent modules are instantiated with the same arguments; if yes, there is no ambiguity;
before reporting ambiguity, check whether all definitions are judgementally equal; if yes, there is no ambiguity; (I guess this would allow name overloading as a way to have named instances…)

Consider the following small example:

module OverlappingOpens where

postulate _≡_ : {A : Set} → A → A → Set

module Fine where
  module There (A0 : Set) where
    A : Set
    A = A0

  module Thither (A0 : Set) (X : Set) where
    open There A0
    postulate thither : X → A

  module Thence (A0 : Set) (X : Set) where
    open There A0
    postulate thence : A → X

  module Iso (A0 : Set) (X : Set) where
    open There A0
    open Thither A0 X
    open Thence A0 X
    postulate here : (x : X) → thence (thither x) ≡ x
    postulate there : (a : A) → thither (thence a) ≡ a

module Bad where
  module There (A0 : Set) where
    A : Set
    A = A0

  module Thither (A0 : Set) (X : Set) where
    open There A0 public
    postulate thither : X → A

  module Thence (A0 : Set) (X : Set) where
    open There A0 public
    postulate thence : A → X

  module Iso (A0 : Set) (X : Set) where
    open Thither A0 X
    open Thence A0 X
    postulate here : (x : X) → thence (thither x) ≡ x
    postulate there : (a : A) → thither (thence a) ≡ a

In Fine, there is no issue, but in Bad, ambiguity is reported for A. If I replace A with an underscore, the file typechecks, showing that both As (the domain of thence and the codomain of thither) really coincide.

As a real life example, in my draft pull request about (relative) adjunctions, the modules LeftRelativeRightAdhoc and LeftAdhocRightRelative both open Adhoc. The module Birelative opens both LeftRelativeRightAdhoc and LeftAdhocRightRelative, which would lead to consistent openings of Adhoc. However, I had to make LeftRelativeRightAdhoc and LeftAdhocRightRelative open Adhoc non-publicly to avoid ambiguity errors in Birelative. This is already less than ideal.
But I inferred that under the current circumstances, open ... public and open import ... public are in general an annoying thing to do, so I had Birelative export none of the aforementioned modules. Then in NaturalBijection I had to open all four (actually their non-relative counterparts) where I would just have wanted to write open Plain F G public and have that module open the other three. This means that as a library developer, I have little control over the interface of my modules, which makes it hard to make edits with good backwards compatibility.

The text was updated successfully, but these errors were encountered:

gallais · 2022-08-18T16:19:00Z

This may be convenient in the short term but don't you run the risk of building a massive scope
with many duplicated definitions thus slowing down compilation?

plt-amy · 2022-08-18T16:38:20Z

Relevant: #4331

.. by which I mean that in a structured signature setup, it'd be possible to cheaply implement this, I think?

andreasabel · 2022-10-08T19:17:12Z

Me too. Just ran into the situation of the OP. Very annoying to see an error like:

Issue6035.agda:41,28-29
Ambiguous name A. It could refer to any one of
  Issue6035.Bad.Iso.A bound at
    Issue6035.agda:26,5-6
  Issue6035.Bad.Iso.A bound at
    Issue6035.agda:26,5-6
(hint: Use C-c C-w (in Emacs) if you want to know why)
when scope checking A

(This is the error triggered by the OP.)
Agda's report is non-sensical, claiming that the name is ambiguous, and then proving a breath later that its denotation (the abstract name behind it) is non-ambiguous.
The detailed explanation is:

A is in scope as
  * a defined name Issue6035.Bad.Iso._.A brought into scope by
    - the application of Thither at Issue6035.agda:38,10-17
    - the application of There at Issue6035.agda:30,10-15
    - its definition at Issue6035.agda:26,5-6
  * a defined name Issue6035.Bad.Iso._.A brought into scope by
    - the application of Thence at Issue6035.agda:39,10-16
    - the application of There at Issue6035.agda:34,10-15
    - its definition at Issue6035.agda:26,5-6

Ok, there are different paths ending in the same target, but why should this be an error? @gallais argues that it might be a useful information that the module setup has redundancies, but it would suffice to print a warning instead.
In my case it was even just a variable that is "ambiguous". I could not care less.

plt-amy · 2022-10-08T19:33:49Z

Do you think we could improve this situation slightly by adding the C-c C-w information to the error report when the names look the same?

andreasabel · 2022-10-09T07:35:21Z

Ah, yes, I just also thought we could always directly expand the "hint" given at the end of the error. This information is available where we raise the error, yet we throw it away instead of passing it to the error message.

andreasabel · 2022-10-09T08:11:25Z

Investigating the problem, I found that the two names rendered in the error message have different NameIds, so, for the scope checker they are really different. This becomes apparent if we name all the intermediate modules created by open M args statements. Here it is, with a further shrinking of the OP:

module Issue6035 where

module M0 (A0 : Set) where
  A : Set
  A = A0

module M1 (A1 : Set) where
  open module M01 = M0 A1 public

module M2 (A2 : Set) where
  open module M02 = M0 A2 public

module M3 (A3 : Set) where
  open module M1' = M1 A3
  open module M2' = M2 A3
  B = A

With the intermediate names, the error also becomes more plausible:

Ambiguous name A. It could refer to any one of
  M1'.A 
  M2'.A

Since Agda's treatment of module is nominal rather than structural, there isn't much to do here except for making the error a bit clearer --- unless we redesign and reimplement the handling of module applications.

Also move explainWhyInScope to TypeChecking.Errors

andreasabel · 2022-10-10T06:44:53Z

Do you think we could improve this situation slightly by adding the C-c C-w information to the error report when the names look the same?

I implemented this in:

Re #6035: make WhyInScope explanation part of AmbiguousName error #6174

nad · 2022-10-10T08:25:33Z

Should this be done also for AmbiguousModule?

agda/src/full/Agda/TypeChecking/Errors.hs

Lines 815 to 827 in bf1a531

    
           AmbiguousName x reason -> vcat 
        
             [ fsep $ pwords "Ambiguous name" ++ [pretty x <> "."] ++ 
        
                      pwords "It could refer to any one of" 
        
             , nest 2 $ vcat $ fmap nameWithBinding $ ambiguousNamesInReason reason 
        
             , explainWhyInScope $ whyInScopeDataFromAmbiguousNameReason x reason 
        
             ] 
        
           AmbiguousModule x ys -> vcat 
        
             [ fsep $ pwords "Ambiguous module name" ++ [pretty x <> "."] ++ 
        
                      pwords "It could refer to any one of" 
        
             , nest 2 $ vcat $ fmap help ys 
        
             , fwords "(hint: Use C-c C-w (in Emacs) if you want to know why)" 
        
             ]

anuyts mentioned this issue Aug 18, 2022

Beefing up adjunctions. agda/cubical#873

Draft

andreasabel added ambiguous-names Issues to do with reporting of name ambiguity scope Issues relating to scope checking labels Aug 18, 2022

jespercockx added the type: enhancement Issues and pull requests about possible improvements label Aug 23, 2022

jespercockx added this to the icebox milestone Aug 23, 2022

andreasabel modified the milestones: icebox, later Oct 8, 2022

andreasabel self-assigned this Oct 9, 2022

andreasabel added a commit that referenced this issue Oct 9, 2022

Re #6035: debug printing; use 'setCurrentRange'

eeedc2a

andreasabel added a commit that referenced this issue Oct 9, 2022

Re #6035: document WhyInScope, use C.QName instead of String

faa7810

andreasabel mentioned this issue Oct 9, 2022

Re #6035: make WhyInScope explanation part of AmbiguousName error #6174

Merged

andreasabel added a commit that referenced this issue Oct 9, 2022

Refactor #6035: AmbiguousNameReason: more info for AmbiguousName error

4328cb9

andreasabel added a commit that referenced this issue Oct 9, 2022

Refactor #6035: AmbiguousNameReason: more info for AmbiguousName error

41f3af1

andreasabel added a commit that referenced this issue Oct 9, 2022

Refactor for #6035: bundle Info_WhyInScope fields as WhyInScopeData

469b722

Also move explainWhyInScope to TypeChecking.Errors

andreasabel added a commit that referenced this issue Oct 9, 2022

Re #6035: add WhyInScope info to AmbiguousName error message

c36ac7d

andreasabel added a commit that referenced this issue Oct 10, 2022

Re #6035: debug printing; use 'setCurrentRange'

05656f2

andreasabel added a commit that referenced this issue Oct 10, 2022

Re #6035: document WhyInScope, use C.QName instead of String

de23266

andreasabel added a commit that referenced this issue Oct 10, 2022

Refactor #6035: AmbiguousNameReason: more info for AmbiguousName error

38bb808

andreasabel added a commit that referenced this issue Oct 10, 2022

Refactor for #6035: bundle Info_WhyInScope fields as WhyInScopeData

3243f17

Also move explainWhyInScope to TypeChecking.Errors

andreasabel added a commit that referenced this issue Oct 10, 2022

Re #6035: add WhyInScope info to AmbiguousName error message

bf1a531

andreasabel removed their assignment Oct 10, 2022

andreasabel modified the milestones: later, icebox Oct 10, 2022

andreasabel added the parameters Module parameters label Oct 10, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Check module equality before issuing "Ambiguous name" error #6035

Check module equality before issuing "Ambiguous name" error #6035

anuyts commented Aug 18, 2022

gallais commented Aug 18, 2022

plt-amy commented Aug 18, 2022 •

edited

Loading

andreasabel commented Oct 8, 2022

plt-amy commented Oct 8, 2022

andreasabel commented Oct 9, 2022

andreasabel commented Oct 9, 2022

andreasabel commented Oct 10, 2022

nad commented Oct 10, 2022

Check module equality before issuing "Ambiguous name" error #6035

Check module equality before issuing "Ambiguous name" error #6035

Comments

anuyts commented Aug 18, 2022

gallais commented Aug 18, 2022

plt-amy commented Aug 18, 2022 • edited Loading

andreasabel commented Oct 8, 2022

plt-amy commented Oct 8, 2022

andreasabel commented Oct 9, 2022

andreasabel commented Oct 9, 2022

andreasabel commented Oct 10, 2022

nad commented Oct 10, 2022

plt-amy commented Aug 18, 2022 •

edited

Loading