Comment l'ajout d'un paramètre d'instance aide-t-il la recherche d'instance?

Question

Par hasard, j'ai réussi à obtenir une recherche d'instance pour réussir mais je ne comprends pas pourquoi.

Dans le code ci-dessous, pourquoi test2 réussit mais test1 échoue (avec des métas non résolues & contraintes)? Comment l'ajout du paramètre ⦃ isRelation ⦄ à IsSymmetric2 aide-t-il? Je me dis que cela doit d'une manière ou d'une autre être lié à la résolution de certains métas, permettant ainsi à la recherche d'instance de réussir, mais au-delà, je suis tout à fait brumeux.

Quelqu'un peut-il faire la lumière sur la mécanique à l'œuvre ici?

Il y a une réponse here qui touche à ma question (la section "Faiblesse") mais il n'y a pas d'explication sur la mécanique du fonctionnement de cette solution de contournement. Je devine qu'une réponse à la présente question m'aidera à mieux comprendre cette solution de contournement.

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

Les erreurs et des métas non résolus présentés par le typechecker pour test1 sont:

_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

Le metavariable problématique est _Q_41, à savoir l'argument Q à symmetry1. Il devrait être clair à partir de la contrainte [55] qu'il n'existe pas de solution unique pour _Q_41 (par exemple, les deux R et flip R sont des solutions potentielles).

Lorsque vous ajoutez la contrainte IsRelation Q cela se transforme en IsRelation {_A39 {.x} {.y}} (_Q_41 {.x} {.y}) en test2. Généralement la recherche d'instance ne touche pas une contrainte comme celle-ci puisque l'argument principal est une métavariable, mais dans ce cas la méta-variable est contrainte (voir [1]), donc la recherche d'instance continue. La seule instance disponible est IsRelation R et le choix de cette solution force _Q_41 à être R.

Si vous deviez ajouter une instance IsRelation (flip R) l'exemple ne passerait plus, car la recherche d'instance ne pouvait pas choisir entre les deux instances IsRelation sans en savoir plus sur _Q_41.

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