<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>