[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

```

[Andreas Abel]

This is not specific to instance arguments, you get the same problem
with hidden arguments:

infix 3 ¬ₕ_

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

gun3 : ∀{a} → ¬ₕ B a
gun3 = {!!}

fun3 : ∀{a} → ¬ₕ B a
fun3 = gun3 -- yellow

-- fun3 is short for:

fun3' : ∀{a} → ¬ₕ B a
fun3' {a} {p} = gun3 {_} {_} -- yellow yellow

The underlying reason for the unsolved metas is that hidden arguments
are inserted eagerly. Workaround: eta-expand manually.

fun3'' : ∀{a} → ¬ₕ B a
fun3'' {a} {p} = gun3 {_} {p} -- no yellow

Best,
Andreas

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