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