[Agda] instance arguments and negation.

[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

On 03.11.2017 11:52, Apostolis Xekoukoulotakis wrote:
> 
> 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  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/