Agda禁用K时无法对x≡x模式匹配，用J可行？原因何在？

尝试在Agda中启用without-K模式，用J规则证明K公理时遇到了一个问题：Agda拒绝将任何类型为Id A x x的项与refl进行模式匹配（提示类似“无法统一x₁ ≟ x₁”）。

比如下面的代码，尝试对p做case拆分时会被Agda拒绝：

data 𝟙 : Type where
  * : 𝟙

test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 𝟙
test {l} {A} x p = ?

但改用J规则实现的版本却能正常运行：

data 𝟙 : Type where
  * : 𝟙

test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 𝟙
test {l} {A} x p = J {A = A} {x = x} (λ y path -> 𝟙) {y = x} p *

这里有两个疑问：

• 使用J规则是否本质上等同于把p当作refl进行分支匹配？
• 如果是，为什么Agda在第一个示例中拒绝拆分p？

参考所用J规则的类型：

J : {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
    {y : A} (p : x ≡ y) → B x refl → B y p

问题解析 #

1. without-K模式的核心限制 #

启用without-K后，Agda会禁用K公理，只保留J规则作为等式的唯一归纳原理。K公理的核心是：所有类型为x ≡ x的路径都是refl——这意味着你可以直接对任意自反路径做refl模式匹配，断言它就是自反构造子。而without-K的目的就是排除这个强假设，只允许使用更弱的J规则。

2. 为什么直接模式匹配被拒绝 #

第一个示例中，尝试对p : x ≡ x做refl模式匹配（比如写成test x refl = *），本质上是在应用K公理：你假设了所有x≡x的路径都是refl。但without-K模式下Agda不允许这种假设，因此会报错“无法统一x₁ ≟ x₁”——这其实是Agda在提示你：不能默认把任意x≡x的路径等同于refl。

3. J规则的本质与合法性 #

J规则并不是直接把p当作refl匹配，而是通过等式归纳来推导结果：

• J的类型要求你提供一个依赖类型B，它依赖于目标点y和从x到y的路径；
• 你只需要提供基例B x refl（也就是当路径是refl时的结果），J会自动将这个基例扩展到所有从x到任意y的路径p上，包括y=x的情况。

当y=x时，J的作用是：通过归纳，把B x refl的结果传递给所有B x p（其中p:x≡x）。这是without-K模式下合法的操作，因为J本身不蕴含K公理——它没有断言p就是refl，只是通过归纳原理确保所有路径都能继承基例的结果。

简单来说：直接模式匹配refl是在假设所有自反路径都是refl（K公理），而J规则是在归纳推导所有路径的结果，这两者在without-K模式下有本质区别。

内容的提问来源于stack exchange，提问作者HPSmash77