当检查模式 p(y) 是否具有 Z 类型时，x != y 类型为 Y

Question

我收到x != y of type Y when checking that the pattern p(y) has type Z 形式的奇怪错误。我不知道为什么或如何得到这个，并想解决这个问题。下面是一个问题实例；谢谢。

---

假设我有一套，

postulate A : Set

以及一种将其元素解释为集合的方法，

postulate F : A → Set

然后使用该集合的对，

record B : Set where field s t : A

我可以在其上构建一个参数化类型：

data C : A → Set where MkC : (b : B) → F (B.s b) → C (B.t b)

现在我想，例如，形成一个函数

ABCF : ∀ a → (f : A → A) → C a → C (f a)
ABCF t f e = {!!}

我会通过C-c C-c 对第三个参数进行模式匹配来做到这一点 这样做让我很开心

ABCF .(B.t b) f (MkC b x) = {!!}

然后另一个C-c C-c，在b，产生

ABCF t f (MkC record { s = s ; t = .t } x) = ?

但是这个大小写紧跟着一个错误：

B.t b != t of type A
when checking that the pattern MkC record { s = s ; t = .t } x has
type C t

用t' 替换.t 也不能解决这个问题。

任何帮助指出此错误背后的原因以及如何修复它都将不胜感激！

---

编辑

正如下面的回答，上述问题可能是由于错误引起的，但相反的情况呢？

FCBA : ∀ {a} (f : A → A) → C (f a) → C a
FCBA {a} f (MkC record { s = s ; t = .(f a) } x) = ?

我们将如何解决这个问题？哪个带有错误

B.t b != f a of type A
when checking that the pattern MkC record { s = s ; t = .(f a) } x
has type C (f a)

Answer 1

看起来像一个错误。如果您将无法访问的模式与常规模式交换，一切正常：

ABCF : ∀ a → (f : A → A) → C a → C (f a)
ABCF .t f (MkC record { s = s ; t = t } x) = {!!}

但是a 无论如何都应该是隐含的，因为它总是可以从C a 推断出来。那么就没有问题了：

ABCF : ∀ {a} → (f : A → A) → C a → C (f a)
ABCF f (MkC record { s = s ; t = t } x) = {!!}

---

如果因为类型太具体而无法直接进行模式匹配，可以泛化：

open import Relation.Binary.PropositionalEquality

FCBA : ∀ {a} (f : A → A) → C (f a) → C a
FCBA {a} f c with f a | inspect f a | c
... | .b | [ r ] | MkC record { s = s ; t = b } x = {!!}

这里我们将f a推广到b并记住f a ≡ b（在这种情况下，这样的记忆可能没有用，但如果你不想忘记b实际上是f a，则需要它）。这允许在 c 上进行模式匹配，并像以前一样交换不可访问的模式和常规模式。

但这不是一个技巧——它是一个丑陋的 hack。您可能应该在 Agda 邮件列表中询问为什么需要这种交换以及这是否是预期的行为。