<html>
  <head>
    <meta content="text/html; charset=utf-8" http-equiv="Content-Type">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>...which is now <a
href="https://stackoverflow.com/questions/43195079/how-does-adding-an-instance-parameter-help-instance-search">here</a>.<br>
    </p>
    <br>
    <div class="moz-cite-prefix">On 04/03/2017 12:33 AM, Martin Stone
      Davis wrote:<br>
    </div>
    <blockquote
      cite="mid:e4bf38ea-5b8e-71c5-bd75-978a8e969d7d@gmail.com"
      type="cite">I realised just now that this question is probably
      more appropriately posted on stackoverflow, so I'll post it there
      (after I check to see if someone has already answered a similar
      question).
      <br>
      <br>
      <br>
      On 04/01/2017 11:12 PM, Martin Stone Davis wrote:
      <br>
      <blockquote type="cite">{- 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. -}
        <br>
        <br>
        {-# OPTIONS --show-implicit #-}
        <br>
        <br>
        record IsSymmetric1 {A : Set} (F : A → A → A) (Q : A → A → Set)
        : Set where
        <br>
          field
        <br>
            symmetry1 : ∀ {x y} → Q (F x y) (F y x)
        <br>
        <br>
        open IsSymmetric1 ⦃ … ⦄
        <br>
        <br>
        record IsRelation {A : Set} (Q : A → A → Set) : Set where
        <br>
          no-eta-equality
        <br>
        <br>
        record IsSymmetric2 {A : Set} (F : A → A → A) (Q : A → A → Set)
        ⦃ isRelation : IsRelation Q ⦄ : Set where
        <br>
          field
        <br>
            symmetry2 : ∀ {x y} → Q (F x y) (F y x)
        <br>
        <br>
        open IsSymmetric2 ⦃ … ⦄
        <br>
        <br>
        postulate
        <br>
          B : Set
        <br>
          G : B → B → B
        <br>
          R : B → B → Set
        <br>
          instance I-IsSymmetric1 : IsSymmetric1 {B} G R
        <br>
          instance I-IsRelation : IsRelation R
        <br>
          instance I-IsSymmetric2 : IsSymmetric2 {B} G R
        <br>
        <br>
        test1 : ∀ {x y} → R (G x y) (G y x)
        <br>
        test1 = symmetry1 -- yellow unless {F = G} or {Q = R} is
        specified
        <br>
        {-
        <br>
        _A_39 : Set  [ at ….agda:29,9-18 ]
        <br>
        _F_40 : _A_39 {.x} {.y} → _A_39 {.x} {.y} → _A_39 {.x} {.y}  [
        at ….agda:29,9-18 ]
        <br>
        _Q_41 : _A_39 {.x} {.y} → _A_39 {.x} {.y} → Set  [ at
        ….agda:29,9-18 ]
        <br>
        _r_42 : IsSymmetric1 {_A_39 {.x} {.y}} (_F_40 {.x} {.y}) (_Q_41
        {.x} {.y})  [ at ….agda:29,9-18 ]
        <br>
        _x_43 : _A_39 {.x} {.y}  [ at ….agda:29,9-18 ]
        <br>
        _y_44 : _A_39 {.x} {.y}  [ at ….agda:29,9-18 ]
        <br>
        _45 : R (G .x .y) (G .y .x)  [ at ….agda:29,9-18 ]
        <br>
        _46 : R (G .x .y) (G .y .x)  [ at ….agda:29,9-18 ]
        <br>
        <br>
        ———— Errors ————————————————————————————————————————————————
        <br>
        Failed to solve the following constraints:
        <br>
          Resolve instance argument
        <br>
            _42 :
        <br>
              {.x .y : B} →
        <br>
              IsSymmetric1 {_A_39 {.x} {.y}} (_F_40 {.x} {.y}) (_Q_41
        {.x} {.y})
        <br>
          Candidates I-IsSymmetric1 : IsSymmetric1 {B} G R
        <br>
          [55] _Q_41 {.x} {.y}
        <br>
               (_F_40 {.x} {.y} (_x_43 {.x} {.y}) (_y_44 {.x} {.y}))
        <br>
               (_F_40 {.x} {.y} (_y_44 {.x} {.y}) (_x_43 {.x} {.y}))
        <br>
               =< R (G .x .y) (G .y .x)
        <br>
                 : Set
        <br>
          _45 :=
        <br>
            λ {.x} {.y} →
        <br>
              IsSymmetric1.symmetry1 (_r_42 {.x} {.y}) {_x_43 {.x} {.y}}
        <br>
              {_y_44 {.x} {.y}}
        <br>
            [blocked on problem 55]
        <br>
        -}
        <br>
        <br>
        test2 : ∀ {x y} → R (G x y) (G y x)
        <br>
        test2 = symmetry2
        <br>
        <br>
      </blockquote>
      <br>
    </blockquote>
    <br>
  </body>
</html>