CODEWITHSUNDEEP
agda
Darkle
Darkle

Reputation: 43

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

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?

Upvotes: 4

Views: 483

Answers (3)

Toxaris
Toxaris

Reputation: 7266

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_)

Upvotes: 0

Jesper
Jesper

Reputation: 2945

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).

Upvotes: 4

Vitus
Vitus

Reputation: 11922

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"

Upvotes: 1

Related Questions