<div dir="ltr"><div><div>I made a negation that takes an instance argument. This unfortunately stops unification from taking place.<br><br></div>In hole 0 , the type is  ⊥.<br></div>in hole 1 , the type is ¬ B .a<div><div><div><br></div><div>Is there a way to force agda to have (¬ᵢ B .a) in hole 0 so that unification deduces a?<br></div><div><br>```<br>data ⊥ : Set where<br><br>infix 3 ¬ᵢ_<br><br>¬ᵢ_ : ∀ {ℓ} → Set ℓ → Set ℓ<br>¬ᵢ P = {{p : P}} → ⊥<br><br><br>infix 3 ¬_<br><br>¬_ : ∀ {ℓ} → Set ℓ → Set ℓ<br>¬ P = (p : P) → ⊥<br><br><br>data A : Set where<br>  a1 : A<br>  a2 : A<br><br><br>data B : A → Set where<br>  b1 : B a1<br>  b2 : B a2<br><br><br>gun : ∀{a} → ¬ᵢ B a<br>gun = {!!}<br><br>fun : ∀{a} → ¬ᵢ B a<br>fun = gun<br><br><br>gun2 : ∀{a} → ¬ B a<br>gun2 = {!!}<br><br>fun2 : ∀{a} → ¬ B a<br>fun2 = gun2<br><br>```<br></div></div></div></div>