[Agda] help explaining instance resolution

[Martin Stone Davis]

{- Can someone explain why test2 succeeds but test1 fails (with unsolved 
metas & constraints)? How does the addition of the ⦃ isRelation ⦄ 
parameter to IsSymmetric2 help? I figure it must somehow have to do with 
some metas getting solved, therefore allowing instance search to 
succeed, but beyond that I'm quite foggy. -}

{-# OPTIONS --show-implicit #-}

record IsSymmetric1 {A : Set} (F : A → A → A) (Q : A → A → Set) : Set where
   field
     symmetry1 : ∀ {x y} → Q (F x y) (F y x)

open IsSymmetric1 ⦃ … ⦄

record IsRelation {A : Set} (Q : A → A → Set) : Set where
   no-eta-equality

record IsSymmetric2 {A : Set} (F : A → A → A) (Q : A → A → Set) ⦃ 
isRelation : IsRelation Q ⦄ : Set where
   field
     symmetry2 : ∀ {x y} → Q (F x y) (F y x)

open IsSymmetric2 ⦃ … ⦄

postulate
   B : Set
   G : B → B → B
   R : B → B → Set
   instance I-IsSymmetric1 : IsSymmetric1 {B} G R
   instance I-IsRelation : IsRelation R
   instance I-IsSymmetric2 : IsSymmetric2 {B} G R

test1 : ∀ {x y} → R (G x y) (G y x)
test1 = symmetry1 -- yellow unless {F = G} or {Q = R} is specified
{-
_A_39 : Set  [ at ….agda:29,9-18 ]
_F_40 : _A_39 {.x} {.y} → _A_39 {.x} {.y} → _A_39 {.x} {.y}  [ at 
….agda:29,9-18 ]
_Q_41 : _A_39 {.x} {.y} → _A_39 {.x} {.y} → Set  [ at ….agda:29,9-18 ]
_r_42 : IsSymmetric1 {_A_39 {.x} {.y}} (_F_40 {.x} {.y}) (_Q_41 {.x} 
{.y})  [ at ….agda:29,9-18 ]
_x_43 : _A_39 {.x} {.y}  [ at ….agda:29,9-18 ]
_y_44 : _A_39 {.x} {.y}  [ at ….agda:29,9-18 ]
_45 : R (G .x .y) (G .y .x)  [ at ….agda:29,9-18 ]
_46 : R (G .x .y) (G .y .x)  [ at ….agda:29,9-18 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
   Resolve instance argument
     _42 :
       {.x .y : B} →
       IsSymmetric1 {_A_39 {.x} {.y}} (_F_40 {.x} {.y}) (_Q_41 {.x} {.y})
   Candidates I-IsSymmetric1 : IsSymmetric1 {B} G R
   [55] _Q_41 {.x} {.y}
        (_F_40 {.x} {.y} (_x_43 {.x} {.y}) (_y_44 {.x} {.y}))
        (_F_40 {.x} {.y} (_y_44 {.x} {.y}) (_x_43 {.x} {.y}))
        =< R (G .x .y) (G .y .x)
          : Set
   _45 :=
     λ {.x} {.y} →
       IsSymmetric1.symmetry1 (_r_42 {.x} {.y}) {_x_43 {.x} {.y}}
       {_y_44 {.x} {.y}}
     [blocked on problem 55]
-}

test2 : ∀ {x y} → R (G x y) (G y x)
test2 = symmetry2