[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