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

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。

不同的库设计可以利用instance arguments提供临时重载（例如Agda prelude）。