Agda : Ambiguous name _==_. It could refer to any one of

Question

What to do if I want to work with packages that provide colliding names, e.g.

  module Halp where
  open import Data.String 
  open import Data.Char 
  open import Data.Bool

  foo : String -> String -> String
  foo a b  with a == b
  ... | true = "foo"
  ... | false = "bar"

leads to

 Ambiguous name _==_. It could refer to any one of
  Data.String._==_ bound at ...\Data\String.agda:71,1-5
  Data.Char._==_   bound at ...\Data\Char.agda:40,1-5

is there an option to make agda figure out what function I mean by arguments if there is ambiguity?

For now I found a workaround of doing _==s_ = Data.String._==_.

Is there other way?

Answer 1

You can make this work by using instance arguments, the Agda alternative to type classes. Unfortunately, the Agda library hasn't been written with instance arguments in mind (yet), so you have to define the Eq class and the instances for Char and String yourself:

open import Data.Bool

open import Data.Char hiding (_==_)
open import Data.String hiding (_==_)

-- The Eq type class
record Eq (A : Set) : Set₁ where
  field
    _==_ : A → A → Bool

-- Instance argument magic
open Eq {{...}}

-- Eq instance for Char
EqChar : Eq Char
EqChar = record { _==_ = Data.Char._==_ }

-- Eq instance for Bool
EqString : Eq String
EqString = record { _==_ = Data.String._==_ }

Now you can use _==_ for both Char and Bool:

test : Bool
test = ('a' == 'a') ∧ ("foo" == "foo") 

To learn more about instance arguments, you can read about them on the Agda wiki (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments) or in the paper that introduced them (http://people.cs.kuleuven.be/~dominique.devriese/agda-instance-arguments/icfp001-Devriese.pdf).

Answer 2

Sadly, no, there is no way to make Agda pick one of those based on the types of the arguments. Agda can resolve ambiguous names only for constructors.

However, there are better ways of specifying which one to use than using _==s_.

• You can specify what functions you want to import into the global namespace:

  open import Data.Char
    hiding (_==_)
  open import Data.String
  
  -- or the other way around
  open import Data.Char
    using (Char) -- and other stuff you might need
  open import Data.String
    using (String; _==_) -- etc.
  

• You can open modules locally inside a function:

  import Data.Char
  import Data.String
  
  test : Type
  test = expr -- use _==_ here
    where
    open Data.String
    -- unqualified names are only available inside expr
  

• You can open modules locally inside another module:

  module UsesStringEq where
    open Data.String
      using (_==_)
  
    test : Type
    test = expr -- use _==_ here
  
  open UsesStringEq public
  -- make sure that other modules can use unqualified names
  -- from UsesStringEq
  

• You can use fully qualified names:

  test : String → String → String
  test a b = if a Data.String.== b then "OK" else "Bad"
  

Answer 3

For now I found a workaround of doing _==s_ = Data.String._==_.

You can also rename bindings when you open the module:

open import Data.String renaming (_==_ to _==s_)
open import Data.Char renaming (_==_ to _==c_)