[Agda] Weird instance propagation between parameterised modules

[Orestis Melkonian]

Done: https://github.com/agda/agda/issues/5093

--OM

On 12/8/20 1:12 PM, Ulf Norell wrote:
> 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 
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201208/a140bcf7/attachment.html>