Using multiple EqReasoning instantiations conveniently

Question 1

Normally, the only way Agda can pick something for you is when it is uniquely determined by the context. In the case of EqReasoning, there isn't usually enough information to pin down the Setoid, even worse actually: you could have two different Setoids over the same Carrier and _≈_ (consider for example two definitionally unequal proofs of transitivity in the isEquivalence field).

However, Agda does allow special form of implicit arguments, which can be filled as long as there is only one value of the desired type. These are known as instance arguments (think instance as in Haskell type class instances).

To demonstrate roughly how this works:

postulate
  A : Set
  a : A

Now, instance arguments are wrapped in double curly braces {{}}:

elem : {{x : A}} → A
elem {{x}} = x

If we decide to later use elem somewhere, Agda will check for any values of type A in scope and if there's only one of them, it'll fill that one in for {{x : A}}. If we added:

postulate
  b : A

Agda will now complain that:

Resolve instance argument _x_7 : A. Candidates: [a : A, b : A]

Because Agda already allows you to perform computations on type level, instance arguments are deliberately limited in what they can do, namely Agda won't perform recursive search to fill them in. Consider for example:

eq : ... → IsEquivalence _≈_ → IsEquivalence (Eq _≈_)

where Eq is Data.Maybe.Eq mentioned in your question. When you then require Agda to fill in an instance argument of a type IsEquivalence (Eq _≈_), it won't try to find something of type IsEquivalence _≈_ and apply eq to it.

With that out of the way, let's take a look at what could work. However, bear in mind that all this stands on unification and as such you might need to push it in the right direction here and there (and if the types you are dealing with become complex, unification might require you to give it so many directions that it won't be worth it in the end).

Personally, I find instance arguments a bit fragile and I usually avoid them (and from a quick check, it would seem that so does the standard library), but your experience might vary.

Anyways, here we go. I constructed a (totally nonsensical) example to demonstrate how to do it. Some boilerplate first:

open import Data.Maybe
open import Data.Nat
open import Relation.Binary

import Relation.Binary.EqReasoning as EqR

To make this example self-contained, I wrote some kind of Setoid with natural numbers as its carrier:

data _≡ℕ_ : ℕ → ℕ → Set where
  z≡z :                    0     ≡ℕ 0
  s≡s : ∀ {m n} → m ≡ℕ n → suc m ≡ℕ suc n

ℕ-setoid : Setoid _ _
ℕ-setoid = record
  { _≈_     = _≡ℕ_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≡ℕ_
  refl {zero}  = z≡z
  refl {suc _} = s≡s refl

  sym : Symmetric _≡ℕ_
  sym z≡z     = z≡z
  sym (s≡s p) = s≡s (sym p)

  trans : Transitive _≡ℕ_
  trans z≡z          q  = q
  trans (s≡s p) (s≡s q) = s≡s (trans p q)

Now, the EqReasoning module is parametrized over a Setoid, so usually you do something like this:

open EqR ℕ-setoid

However, we'd like to have the Setoid parameter to be implicit (instance) rather than explicit, so we define and open a dummy module:

open module Dummy {c ℓ} {{s : Setoid c ℓ}} = EqR s

And we can write this simple proof:

idʳ : ∀ n → n ≡ℕ (n + 0)
idʳ 0 = z≡z
idʳ (suc n) = begin
  suc n        ≈⟨ s≡s (idʳ n) ⟩
  suc (n + 0)  ∎

Notice that we never had to specify ℕ-setoid, the instance argument picked it up because it was the only type-correct value.

Now, let's spice it up a bit. We'll add Data.Maybe.setoid into the mix. Again, because instance arguments do not perform a recursive search, we'll have to define the setoid ourselves:

Maybeℕ-setoid = setoid ℕ-setoid
_≡M_ = Setoid._≈_ Maybeℕ-setoid

I'm going to postulate few stupid things just to demonstrate that Agda indeed picks correct setoids:

postulate
  comm : ∀ m n → (m + n) ≡ℕ (n + m)
  eq0  : ∀ n → n ≡ℕ 0
  eq∅  : just 0 ≡M nothing

lem : ∀ n → just (n + 0) ≡M nothing
lem n = begin
  just (n + 0)  ≈⟨ just
    (begin
      n + 0  ≈⟨ comm n 0 ⟩
      n      ≈⟨ eq0 n ⟩
      0      ∎
    )⟩
  just 0        ≈⟨ eq∅ ⟩
  nothing       ∎

Question 2

I figured an alternative to the proposed solution using instance arguments that slightly bends the requirements, but fits my purpose. The major burden in the question was having to explicitly open EqReasoning multiple times and especially having to invent new names for the contained symbols. A slight improvement would be to pass the correct Setoid once per relation proof. In other words passing it to begin_ or _∎ somehow. Then we could make the Setoid implicit for all the other functions!

import Relation.Binary.EqReasoning as EqR
import Relation.Binary using (Setoid)
module ExplicitEqR where
 infix 1 begin⟨_⟩_
 infixr 2 _≈⟨_⟩_ _≡⟨_⟩_
 infix 2 _∎
 begin⟨_⟩_ : ∀ {c l} (X : Setoid c l) → {x y : Setoid.Carrier X} → EqR._IsRelatedTo_ X x y → Setoid._≈_ X x y
 begin⟨_⟩_ X p = EqR.begin_ X p
 _∎ : ∀ {c l} {X : Setoid c l} → (x : Setoid.Carrier X) → EqR._IsRelatedTo_ X x x
 _∎ {X = X} = EqR._∎ X
 _≈⟨_⟩_ : ∀ {c l} {X : Setoid c l} → (x : Setoid.Carrier X) → {y z : Setoid.Carrier X} → Setoid._≈_ X x y → EqR._IsRelatedTo_ X y z → EqR._IsRelatedTo_ X x z
 _≈⟨_⟩_ {X = X} = EqR._≈⟨_⟩_ X
 _≡⟨_⟩_ : ∀ {c l} {X : Setoid c l} → (x : Setoid.Carrier X) → {y z : Setoid.Carrier X} → x ≡ y → EqR._IsRelatedTo_ X y z → EqR._IsRelatedTo_ X x z
 _≡⟨_⟩_ {X = X} = EqR._≡⟨_⟩_ X

Reusing the nice example from Vitus answer, we can write it:

lem : ∀ n → just (n + 0) ≡M nothing
lem n = begin⟨ Data.Maybe.setoid ℕ-setoid ⟩
  just (n + 0)  ≈⟨ just
    (begin⟨ ℕ-setoid ⟩
      n + 0  ≈⟨ comm n 0 ⟩
      n      ≈⟨ eq0 n ⟩
      0      ∎
    )⟩
  just 0        ≈⟨ eq∅ ⟩
  nothing       ∎
  where open ExplicitEqR

One still has to mention the Setoids in use, to avoid the use of instance arguments as presented by Vitus. However the technique makes it significantly more convenient.