[Agda] help explaining instance resolution

[Ulf Norell]

Answered here
<https://stackoverflow.com/questions/43195079/how-does-adding-an-instance-parameter-help-instance-search/43203610#43203610>
.

/ Ulf

On Tue, Apr 4, 2017 at 12:04 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> ...which is now here
> <https://stackoverflow.com/questions/43195079/how-does-adding-an-instance-parameter-help-instance-search>
> .
>
> On 04/03/2017 12:33 AM, Martin Stone Davis wrote:
>
> 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).
>
>
> On 04/01/2017 11:12 PM, Martin Stone Davis wrote:
>
> {- 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170404/22b7bf34/attachment.html>