[Agda] help explaining instance resolution
Martin Stone Davis
martin.stone.davis at gmail.com
Tue Apr 4 00:04:47 CEST 2017
...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
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170403/f1083057/attachment-0001.html>
More information about the Agda
mailing list