<div dir="ltr"><div>Answered <a href="https://stackoverflow.com/questions/43195079/how-does-adding-an-instance-parameter-help-instance-search/43203610#43203610">here</a>.<br></div><div><br></div><div>/ Ulf</div><div><br></div><div class="gmail_extra"><div class="gmail_quote">On Tue, Apr 4, 2017 at 12:04 AM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF">
    <p>...which is now <a href="https://stackoverflow.com/questions/43195079/how-does-adding-an-instance-parameter-help-instance-search" target="_blank">here</a>.<br>
    </p><div><div class="h5">
    <br>
    <div class="m_-4263860627179533314moz-cite-prefix">On 04/03/2017 12:33 AM, Martin Stone
      Davis wrote:<br>
    </div>
    <blockquote 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 ——————————————————————————————<wbr>——————————————————
        <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>
  </div></div></div>

<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div></div>