Agda：无法解决以下约束：P x <= _X_53(在_X_53上被阻止)

Question

我在读这本书的时候正在写Agda代码。我被引理2.3.9卡住了:

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'，为什么它大于或等于(px)?
2. 我怎样才能摆脱这个错误?

注意我在Coq中编写了一个Lemma 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无法理解一个隐含的论点，尽管人们会认为她应该能够理解。即，Agda无法解析隐式参数的元变量。这是她需要一点帮助的时候，也就是说，我们必须明确指定一个或多个隐式参数。这就是@gallais表明在评论。

=<比较两种类型。A =< B意味着A类型的东西可以放在需要B类型的东西的地方。所以，如果你有一个接受B的函数，你可以给它一个A，它会进行类型检查。我认为这主要用于Agda的大小类型。在你的情况下，我认为，这可以被理解为类型相等。

回到错误信息。Agda未能找到_X_53的解决方案。需要满足的约束是P x =< _X_53。如果在您的情况下，=<是类型相等，那么为什么Agda不简单地将_X_53设置为P x呢?

根据我非常有限的理解，原因是高阶统一，用一个非常专业的术语来说，这是一个反复无常和挑剔的野兽。_X_53并不是完全正确的。元变量可以是函数，因此有参数。根据Agda调试日志,实际的统一问题统一_X_53 A P x xP x。如果我记得正确的话，那么前两个x是一个问题。不过，对此持保留态度。我不是类型理论家。

长话短说，有时候Agda不能找出一个隐含的参数，因为统一失败了，很难确切地理解为什么。

最后，一些相关的东西:下面的文章讨论了一些使用隐式参数的最佳实践:

我猜这两个x是一个问题，因为它们使Agda无法找到统一问题的唯一解决方案。请注意，λ a b c d. P c和λ a b c d. P d都适用于_X_53，因为它们都会使_X_53 A P x x减少到P x。