[Agda] Agda can't find an obvious instance.

[effectfully]

In this sense instance search always leads to unpredictable behaviour
and brittle code, because it always relies on a context. Agda 2.4.3
happily infers the type of `x':

----

open import Data.Nat

record Default (A : Set) : Set where
  field default : A

open Default {{...}}

instance
  DefaultNat : Default ℕ
  DefaultNat = record { default = 0 }

x : _
x = default

----

This is quite a big restriction. E.g.

record Setoid {α} (A : Set α) β : Set (α ⊔ suc β) where
  infix 4 _≈_

  field
    _≈_           : A -> A -> Set β
    isEquivalence : IsEquivalence _≈_

it's no point to write "open Setoid {{...}}" — instance search can't
find instances of `Setoid', because of this tiny `β'.

Also, in my second example (with the `R' record) the instance can be
determined by the first index, so the second index probably shouldn't
affect instance search at all.