<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Done: <a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/5093">https://github.com/agda/agda/issues/5093</a><br>
<br>
--OM<br>
</p>
<div class="moz-cite-prefix">On 12/8/20 1:12 PM, Ulf Norell wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAJjNqYFJUnimxoNrJQuufqqXXwNtrLTpr84JW+MyA8kaBnq69Q@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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"
moz-do-not-send="true">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"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
</body>
</html>