[Agda] overloading operations

[Sergei Meshveliani]

On Wed, 2018-11-14 at 14:08 +0100, Guillaume Allais wrote:

> [..]
> `instance` is a bit like instance in Haskell: everything declared in the
> block is made available for instance resolution. The difference in Agda
> is of course that you can also declare record values *outside* of instance
> blocks. They are then *not* used by the automatic instance resolution.
> But the user can have access to them like any other value.
> [..]


For example, I declare 

 record Setoid {c} ℓ (Carrier : Set c) :  Set (suc (c ⊔ ℓ))  where
     infix 4 _≈_
     field
       _≈_           : Rel Carrier ℓ
       isEquivalence : IsEquivalence _≈_

(after the suggestion by Guillaume Brunerie).
Overloading for the above Setoid operations works like this:

   open Setoid {{...}}

   module _ {α α= β β=} (C : Set α) (C' : Set β)
                        {{S : Setoid α= C}} {{S' : Setoid β= C'}}
     where
     IsCongruent :  (C → C') → Set _
     IsCongruent f =
                   {x y : C} → x ≈ y → (f x) ≈ (f y)
 
The word `instance' is not applied.
On the other hand, the two instances for _≈_ are actually resolved.

For this particular declaration for Setoid, what possibility is lost by
skipping instance declarations?

Thanks,

------
Sergei