1
事故で、私は成功するためにインスタンス検索を得ることができましたが、私はその理由を理解していません。以下のコードでインスタンスパラメータを追加すると、インスタンス検索がどのように助けられますか？
、なぜtest2は成功しないが、test1は（未解決のメタ情報&制約で）失敗しますか？ IsSymmetric2への⦃ isRelation ⦄パラメータの追加はどのように役立ちますか？どういうわけか、いくつかのメタが解決されなければならないので、インスタンス検索を成功させる必要があると思っていますが、それを超えるとかなり霧がかかります。
誰かがここで働くメカニックに光を当てることができますか？
私の質問（「弱さ」セクション）に触れた回答はhereですが、回避策の仕組みの仕組みについての説明はありません。私は現在の質問に対する答えが、その回避策をよりよく理解するのに役立つだろうと推測しています。
{-# 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
test2 : ∀ {x y} → R (G x y) (G y x)
test2 = symmetry2
エラーとtest1ための型チェッカーによって報告された未解決のメタ情報は、次のとおり
_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]