[Agda] multiple instance resolution and negation

[Marcus Christian Lehmann]

Dear Agda community,

Is there a possibility to make instances like

   i1 : {{ a : A }} → ⊥
   i2 : {{ b : B }} → ⊥
   i3 : {{ c : C }} → ⊥

unambiguous in an instance resolution?

CONTEXT:

I am investigating on the usefulness of instance arguments for partial 
functions such as the positive square root function.

In this particular example, the square root function takes as an 
additional argument a proof that the argument is nonnegative:

   sqrt : (x : X) → {{p : (0ˣ ≤ x)}} → X

When _≤_ is defined in terms of _<_ and ⊥ as

   _≤_ : X → X → Set ℓ'
   a ≤ b = (b < a) → ⊥

then Agda complains that

   "Instance arguments with explicit arguments are never considered by"
   "instance search, so having an instance argument ⦃ p : 0ˣ ≤ x ⦄ has"
   "no effect."
   "when checking that the expression ⦃ p : 0ˣ ≤ x ⦄ → X is a type"

I came up with a different definition

   _≤ᵢ_ : X → X → Set ℓ'
   a ≤ᵢ b = {{p : b < a}} → ⊥

that works on

   sqrt : (x : X) → {{p : (0ˣ ≤ᵢ x)}} → X

when used like so:

   inst-¬ : ∀{ℓ} {A : Set ℓ} → (A → ⊥) → {{a : A}} → ⊥
   inst-¬ f {{a}} = f a

   test1 : (x : X) → (0ˣ ≤ x) → X
   test1 x 0≤x = let instance _ = inst-¬ 0≤x
                 in sqrt x -- works!

but when multiple instances are in scope

   test2 : (x y z : X) → (0ˣ ≤ x) → (0ˣ ≤ y) → (0ˣ ≤ z) → X
   test2 x y z 0≤x 0≤y 0≤z =
     let instance 0≤xᵢ : 0ˣ ≤ᵢ x
                  0≤xᵢ = inst-¬ 0≤x
                  0≤yᵢ : 0ˣ ≤ᵢ y
                  0≤yᵢ = inst-¬ 0≤y
                  0≤zᵢ : 0ˣ ≤ᵢ z
                  0≤zᵢ = inst-¬ 0≤z
     -- Goal: X
     -- Have: ⦃ p : 0ˣ ≤ᵢ x ⦄ → X
     in sqrt y -- error!

then Agda complains:

   _p_51 : 0ˣ ≤ᵢ y
   errorFailed to solve the following constraints:
     Resolve instance argument
       _p_51
         : {ℓ = ℓ₁ : Agda.Primitive.Level} {ℓ' = ℓ'' : Agda.Primitive.Level}
           (X₁ : Set ℓ₁) (0ˣ₁ : X₁) (_<₁_ : X₁ → X₁ → Set ℓ'') (x₁ y₁ z₁ 
: X₁)
           (0≤x₁ : 0ˣ₁ ≤ x₁) (0≤y₁ : 0ˣ₁ ≤ y₁) (0≤z₁ : 0ˣ₁ ≤ z₁) →
           0ˣ₁ ≤ᵢ y₁
     Candidates
       λ ⦃ a ⦄ → z a : ⦃ p : 0ˣ _<_ X ⦄ → ⊥
       λ ⦃ a ⦄ → 0≤x a : ⦃ p : 0ˣ x X ⦄ → ⊥
       λ ⦃ a ⦄ → 0≤y a : ⦃ p : 0ˣ y X ⦄ → ⊥

apart from the quirky candidate display (which does not make sense to me);

shouldn't it be possible for Agda to distinguish these three candidates 
and pick the right one?

kind regards,
Christian


PS: This issue arises. I guess, because Agda can look into the 
definition of _≤_ since everything works out, when hiding the definition 
as in

   _≤'_ : X → X → Set ℓ'
   abstracta ≤' b = (b < a) → ⊥

e.g.

   test3 : (x y z : X) → (0ˣ ≤' x) → (0ˣ ≤' y) → (0ˣ ≤' z) → X
   test3 x y z 0≤x 0≤y 0≤z =
     let instance _ = 0≤x ; _ = 0≤y ; _ = 0≤z
     in sqrt' y -- works!

I would also be happy with a different approach.

PPS: the closest item on this mailing list was an email of Apostolis 
Xekoukoulotakis from 03.11.17, 11:52 but it does not address this issue