如何处理相互冲突的模块定义？

Question

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ℚ

如果我像0ℚ ≤ lookup (σ id) i × lookup (σ id) i ≤ 1ℚ那样编写上面的代码，我就会得到以下类型的错误。

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

有什么优雅的方法可以使Agda推断出它自己使用的正确的函数吗？在这里，它应该能够做正确的事情，因为类型是已知的。

Answer 1

Agda允许模棱两可的构造函数和模棱两可的投射，但任何其他名称在使用的位置都必须是明确的。

为了避免歧义，可以使用open import Data.Nat renaming (_≤_ to _≤Nat_)语法重命名符号。或者，您可以使用open import Data.Nat as Nat和x Nat.≤ y。

不同的库设计可以使用实例参数来提供临时重载(例如，Agda序曲)。