[Agda] instance arguments and negation.

[Apostolis Xekoukoulotakis]

I made a negation that takes an instance argument. This unfortunately stops
unification from taking place.

In hole 0 , the type is ⊥.
in hole 1 , the type is ¬ B .a

Is there a way to force agda to have (¬ᵢ B .a) in hole 0 so that
unification deduces a?

```
data ⊥ : Set where

infix 3 ¬ᵢ_

¬ᵢ_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ᵢ P = {{p : P}} → ⊥


infix 3 ¬_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = (p : P) → ⊥


data A : Set where
  a1 : A
  a2 : A


data B : A → Set where
  b1 : B a1
  b2 : B a2


gun : ∀{a} → ¬ᵢ B a
gun = {!!}

fun : ∀{a} → ¬ᵢ B a
fun = gun


gun2 : ∀{a} → ¬ B a
gun2 = {!!}

fun2 : ∀{a} → ¬ B a
fun2 = gun2

```
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171103/1082d5cc/attachment.html>