[Agda] Weird instance propagation between parameterised modules
Orestis Melkonian
melkon.or at gmail.com
Tue Dec 8 11:56:42 CET 2020
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
More information about the Agda
mailing list