如何添加实例参数来帮助实例搜索？

Question

不小心,我设法让实例搜索成功,但我不明白为什么.

在下面的代码中,为什么test2成功但test1失败(有未解决的元数据和约束)？如何添加? isRelation ?参数来IsSymmetric2帮助？我认为它必须以某种方式与一些metas得到解决,因此允许实例搜索成功,但除此之外,我很有雾.

有人能否说明这里的工作机制？

有一个答案在这里触及我的问题(以下简称"弱点"一节)上,但没有解释出现的解决方法是如何工作的力学.我猜这个问题的答案将帮助我更好地理解这种解决方法.

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

typechecker报告的错误和未解决的元数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]

Answer 1

有问题的元变量是_Q_41,即Q参数symmetry1.它应该是从约束清楚[55],有没有为唯一的解决方案_Q_41(例如两者R并flip R有可能的解决方案).

当你添加IsRelation Q约束时,它变成IsRelation {_A39 {.x} {.y}} (_Q_41 {.x} {.y})了test2.通常实例搜索不会触及类似的约束,因为主要参数是元变量,但在这种情况下,元变量受到约束(参见[1]),因此实例搜索继续进行.唯一可用的实例IsRelation R,并选择该解决方案的力量 _Q_41是R.

如果您要添加实例,IsRelation (flip R)则示例将不再通过,因为实例搜索无法在IsRelation不了解更多信息的情况下在两个实例之间进行选择_Q_41.

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