AGDA：无法求解以下约束：p x＆lt; = _x_53（在_x_53上被阻止）

Question

当我阅读

data _≡_ {X : Set} : X -> X -> Set where
  refl : {x : X} -> x ≡ x
infix 4 _≡_

-- Lemma 2.1.2
_·_ :  {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
refl · refl = refl

-- Lemma 2.3.1
transp : {A : Set} {P : A -> Set} {x y : A} -> x ≡ y -> P x -> P y
transp refl f = f

lemma2'3'9 : {A : Set}{P : A -> Set}{x y z : A}{p : x ≡ y}{q : y ≡ z}{u : P x} -> 
             (transp q (transp p u)) ≡ (transp (p · q) u)
lemma2'3'9 {p = refl} {q = refl} = ?

使用ADGA EMACS模式进行类型检查给我以下错误：

?0 : transp refl (transp refl u) ≡ transp (refl · refl) u
_X_53 : Set  [ at /home/user/prog/agda/sample.agda:12,38-39 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  P x =< _X_53 (blocked on _X_53)

问题

1. 什么是'_x_53'，为什么它大于或等于（p x） ？
2. 如何摆脱此错误？

注意 我在Coq中写了一个引理2.3.9的工作示例，所以我假设在AGDA中可能有可能。

Inductive eq {X:Type} (x: X) : X -> Type :=
  | refl : eq x x.
Notation "x = y" := (eq x y)
                       (at level 70, no associativity)
                     : type_scope.

Definition eqInd{A} (C: forall x y: A, x = y -> Type) (c: forall x: A, C x x (refl x)) (x y: A): forall p: x = y, C x y p :=
  fun xy: x = y => match xy with
            | refl _ => c x
            end.

Definition dot'{A}{x y: A}: x = y -> forall z: A, y = z -> x = z :=
  let D := fun x y: A => fun p: x = y => forall z: A, forall q: y = z, x = z in
  let d: forall x, D x x (refl x) := let E: forall x z: A, forall q: x = z, Type := fun x z: A => fun q: x = z => x = z in
                                let e := fun x => refl x
                                in  fun x z => fun q => eqInd E e x z q
  in fun p: x = y => eqInd D d x y p.

(* Lemma 2.1.2 *)
Definition dot{A}{x y z: A}: x = y -> y = z -> x = z :=
  fun p: x = y => dot' p z.

Definition id {A} := fun a: A => a.

(* Lemma 2.3.1 *)
Definition transp{A} {P: A -> Type} {x y: A}: x = y -> P x -> P y :=
  fun p =>
  let D := fun x y: A => fun p: x = y => P x -> P y in
  let d: forall x, D x x (refl x) := fun x => id
  in  eqInd D d x y p.

Lemma L_2_3_9{A}{P: A -> Type}{x y z: A}{p: x = y}{q: y = z}{u: P x}:
  transp q (transp p u) = transp (dot p q) u.
Proof.
  unfold transp, dot, dot'.
  rewrite <- q.
  rewrite <- p.
  reflexivity.
  Qed.

Answer 1

_x_53是一个元变量，即一个术语的未知部分。为了弄清楚该术语的这个未知部分，AGDA试图解决元变量。她这样做是通过查看上下文出现的上下文，从这种上下文中得出约束，并确定满足约束的元变量的可能候选解决方案。

除其他外，AGDA使用元变量实施隐式参数。每个隐式参数都被元变量替换，然后AGDA试图在包含其余参数的上下文中解决。例如，这就是隐式参数的值可以从其余参数中得出的方式。

有时，Agda无法弄清楚一个隐性的论点，即使人们认为她应该能够。 IE，AGDA无法解析隐式参数的元变量。这是她需要一点帮助的时候，即我们必须明确指定一个或多个隐性论点。这就是@Gallais在评论中所建议的。

=＆lt;比较两种类型。 a =＆lt; B表示可以将某些类型A放置在需要类型B的地方。因此，如果您的函数可以采用b，则可以给它一个a，并且它将输入检查。我认为这主要用于AGDA大小的类型。我认为，就您而言，这可以读为类型平等。

但是回到错误消息。 AGDA无法找到_X_53的解决方案。需要满足的约束是p x =＆lt; _x_53。如果在您的情况下，=＆lt;是类型等式，那么为什么AGDA不简单地将_X_53设置为p x？

根据我非常有限的理解，原因是高阶统一，这有点像技术术语 - 具有反复无常和挑剔的野兽。 _x_53不是这里的完整真相。元变量可以是函数，因此具有参数。根据AGDA调试日志，实际的统一问题是统一_X_53 AP X X和p x。如果我记得正确的话，那么前者中的两个x是一个问题。不过，用一粒盐去吃。我不是一个类型的理论家。

长话短说，有时AGDA无法弄清楚一个隐性的论点，因为统一失败了，而且很难理解为什么。

Finally, something related: The following article talks a bit about best practices for using implicit arguments:

更新

我想两个x是一个问题，因为它们使AGDA无法找到统一问题的独特解决方案。请注意，这两个，λABCd。 p c和λABCd。 p d将适用于_x_53，因为两者都会使_x_53 ap x x x降低到p x。