Search code examples
agda

How to deal with conflicting module definitions?

open import Data.Vec
open import Data.Nat
open import Data.Fin
open import Data.Integer
open import Data.Rational
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

Infoset = ℕ
Size = ℕ
Player = ℤ

data GameTree (infoset-size : Infoset → Size) : Set where
  Terminal : (reward : ℚ) → GameTree infoset-size
  Response : (id : Infoset) → (subnodes : Vec (GameTree infoset-size) (infoset-size id)) → GameTree infoset-size

record Policy (infoset-size : Infoset → Size) : Set where
  field
    σ : ∀ (id : Infoset) → Vec ℚ (infoset-size id)
    wf-elem : ∀ (id : Infoset) (i : Fin (infoset-size id)) → 0ℚ Data.Rational.≤ lookup (σ id) i × lookup (σ id) i Data.Rational.≤ 1ℚ

Had I written the above like 0ℚ ≤ lookup (σ id) i × lookup (σ id) i ≤ 1ℚ I would have gotten the following type error.

Ambiguous name _≤_. It could refer to any one of
  Data.Nat._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Nat\Base.agda:33,6-9
  Data.Fin._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Fin\Base.agda:218,1-4
  Data.Integer._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Integer\Base.agda:44,6-9
  Data.Rational._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Rational\Base.agda:71,6-9

Is there some elegant way to induce to make Agda infer the right functions to use on its own? Here it should be capable of doing the right thing given that the types are known.

Solution

  • Agda allows ambiguous constructors and ambiguous projections, but any other names have to be unambigous at the position where they are used.

    To avoid ambiguity, you can rename a symbol using the open import Data.Nat renaming (_≤_ to _≤Nat_) syntax. Alternatively, you can use open import Data.Nat as Nat and use x Nat.≤ y.

    A different library design could make use of instance arguments to provide ad-hoc overloading (for example the Agda prelude).