[Agda] Weird instance propagation between parameterised modules

[Ulf Norell]

This looks like a bug. Can you file an issue?

/ Ulf

On Tue, Dec 8, 2020 at 11:56 AM Orestis Melkonian <melkon.or at gmail.com>
wrote:

> Hi y'all,
>
> I came across a rather peculiar issue when simultaneously using instance
> arguments, parameterised modules and generalized variables. I tried to
> find a minimal-enough example to demonstrate this, tested on Agda-2.6.1.
>
> Let's assume we have an Eq typeclass in a separate file:
> ```Eq.agda
> module Eq where
>
> open import Agda.Builtin.Bool
>
> record Eq (A : Set) : Set where
>    field
>      _==_ : A → A → Bool
> open Eq {{...}} public
> ```
>
> Then a module parameterised over some type A having (decidable) equality:
>
> ```M1.agda
> open import Eq
>
> module M1 (A : Set) {{_ : Eq A}} where
>
> postulate
>    B : Set
> variable
>    n : B
> postulate
>    P : B → Set
>
> postulate
>    p₁ : P n
> ```
>
> All fine so far, but what if I want to split that file, e.g. to work on
> p₁ there:
> ```M2.agda
> open import Eq
>
> module M2 (A : Set) {{_ : Eq A}} where
>
> open import M1 A
>
> postulate p₂ : P n
> ```
> But now there is an error:
> ```
> No instance of type Eq A was found in scope.
> when checking that n is a valid argument to a function of type
> ⦃ _ = x : Eq A ⦄ → M1.B A → Set
> ```
>
> Amusingly, this is solved if we pass `it` as the instance argument!
> ```M2.agda
> open import Eq
> module M2 (A : Set) {{_ : Eq A}} where
>
> open import M1 A {{it}}
>
> postulate p₂ : P n
> ```
>
> I am wondering if I am missing something, or this is actually a bug..
> Moreover, shouldn't all occurrences of `{{it}}` be meaningless?
>
> Cheers,
> --OM
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201208/d0b71dfb/attachment.html>