Wie hilft das Hinzufügen eines Instanzparameters, Instanzen zu suchen?

Question

Durch Zufall konnte ich die Instanzsuche erfolgreich durchführen, aber ich verstehe nicht warum.

In dem nachfolgenden Code, warum ist test2 erfolgreich, aber test1 fehlgeschlagen (mit ungelösten Metas & Einschränkungen)? Wie hilft die Ergänzung des ⦃ isRelation ⦄ Parameters zu IsSymmetric2? Ich denke, dass es irgendwie damit zu tun haben muss, dass einige Metas gelöst werden, so dass die Instanzsuche Erfolg haben kann, aber darüber hinaus bin ich ziemlich neblig.

Kann jemand hier die Mechanik bei der Arbeit beleuchten?

Es gibt eine Antwort , die meine Frage berührt (die "Schwäche" -Abschnitt), aber es gibt keine Erklärung dafür, wie die Problemumgehung funktioniert. Ich schätze, dass eine Antwort auf die aktuelle Frage mir helfen wird, diese Problemumgehung besser zu verstehen.

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

die Fehler und ungelöst durch den typechecker berichtet metas für test1 sind:

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

Answer 1

Die problematische Metavariable _Q_41 ist, das heißt die Q Argument symmetry1. Aus der Einschränkung [55] sollte klar sein, dass es für _Q_41 keine eindeutige Lösung gibt (beispielsweise sind sowohl R als auch flip R potenzielle Lösungen).

Wenn Sie die Bedingung IsRelation Q hinzufügen, wird diese in IsRelation {_A39 {.x} {.y}} (_Q_41 {.x} {.y}) in test2 umgewandelt. In der Regel sucht die Instanzsuche eine solche Einschränkung nicht, da das Hauptargument eine Metavariable ist. In diesem Fall ist jedoch die Metavariable eingeschränkt (siehe [1]), sodass die Instanzsuche fortgesetzt wird. Die einzige verfügbare Instanz ist IsRelation R, und die Auswahl dieser Lösung erzwingt _Q_41 als R.

Wenn Sie eine Instanz IsRelation (flip R) hinzufügen, würde das Beispiel nicht mehr durchlaufen, da Instanz Suche konnte nicht zwischen den beiden IsRelation Instanzen wählen, ohne mehr über _Q_41 zu wissen.

[1] http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution