<div dir="ltr"><div>This looks like a bug. Can you file an issue?</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Dec 8, 2020 at 11:56 AM Orestis Melkonian <<a href="mailto:melkon.or@gmail.com">melkon.or@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi y'all,<br>
<br>
I came across a rather peculiar issue when simultaneously using instance <br>
arguments, parameterised modules and generalized variables. I tried to <br>
find a minimal-enough example to demonstrate this, tested on Agda-2.6.1.<br>
<br>
Let's assume we have an Eq typeclass in a separate file:<br>
```Eq.agda<br>
module Eq where<br>
<br>
open import Agda.Builtin.Bool<br>
<br>
record Eq (A : Set) : Set where<br>
   field<br>
     _==_ : A → A → Bool<br>
open Eq {{...}} public<br>
```<br>
<br>
Then a module parameterised over some type A having (decidable) equality:<br>
<br>
```M1.agda<br>
open import Eq<br>
<br>
module M1 (A : Set) {{_ : Eq A}} where<br>
<br>
postulate<br>
   B : Set<br>
variable<br>
   n : B<br>
postulate<br>
   P : B → Set<br>
<br>
postulate<br>
   p₁ : P n<br>
```<br>
<br>
All fine so far, but what if I want to split that file, e.g. to work on <br>
p₁ there:<br>
```M2.agda<br>
open import Eq<br>
<br>
module M2 (A : Set) {{_ : Eq A}} where<br>
<br>
open import M1 A<br>
<br>
postulate p₂ : P n<br>
```<br>
But now there is an error:<br>
```<br>
No instance of type Eq A was found in scope.<br>
when checking that n is a valid argument to a function of type<br>
⦃ _ = x : Eq A ⦄ → M1.B A → Set<br>
```<br>
<br>
Amusingly, this is solved if we pass `it` as the instance argument!<br>
```M2.agda<br>
open import Eq<br>
module M2 (A : Set) {{_ : Eq A}} where<br>
<br>
open import M1 A {{it}}<br>
<br>
postulate p₂ : P n<br>
```<br>
<br>
I am wondering if I am missing something, or this is actually a bug..<br>
Moreover, shouldn't all occurrences of `{{it}}` be meaningless?<br>
<br>
Cheers,<br>
--OM<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>