<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>