如何告知Agda类型检查器两种类型确实相等？

最小示例代码 #

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x
{-# BUILTIN EQUALITY _≡_  #-}

data Type₁ : Set where
    id : Type₁
    non-id : Type₁

data Type₂ : Set where
    combine : Type₂ → Type₁ → Type₂

data Type₃ : Type₂ → Set where
    combine : {a : Type₂} → Type₃ a → Type₁ → Type₃ (combine a b)

postulate
    eq : {A : Type₂} → combine A id ≡ A
    eq-2 : {A : Type₂} → {a : Type₃ A} → combine a id ≡ a

报错信息 #

A != combine A id of type Type₂
when checking that the expression a has type Type₃ (combine A id)

问题分析 #

核心矛盾在于Agda严格区分定义相等与命题相等：

• 定义相等是语法层面的等价关系，Agda类型检查器会自动识别并统一这类类型（比如x和x直接相等）
• 命题相等（即你用_≡_声明的eq）是逻辑层面的相等，需要显式通过工具告知类型检查器如何基于该相等关系转换类型

在eq-2的声明中，combine a id的类型是Type₃ (combine A id)，但a的类型是Type₃ A——尽管eq断言两者的索引类型相等，但Agda不会自动用命题相等调整类型，因此触发类型不匹配错误。

解决方案 #

可以使用Agda内置的subst函数（代入函数），基于命题相等完成类型转换。subst的类型为：

subst : {A : Set} {x y : A} → (P : A → Set) → x ≡ y → P x → P y

它的作用是：若存在x ≡ y，则可将P x类型的项转换为P y类型的项。

针对你的场景，有两种可行修改方式：

方式1：转换a的类型以匹配combine a id #

修改eq-2的声明，用sym eq反转命题相等方向，再通过subst把a的类型从Type₃ A转换为Type₃ (combine A id)：

postulate
    eq : {A : Type₂} → combine A id ≡ A
    eq-2 : {A : Type₂} (a : Type₃ A) → combine a id ≡ subst Type₃ (sym eq) a

方式2：转换combine a id的类型以匹配a #

反过来，直接用subst把combine a id的类型从Type₃ (combine A id)转换为Type₃ A：

postulate
    eq : {A : Type₂} → combine A id ≡ A
    eq-2 : {A : Type₂} (a : Type₃ A) → subst Type₃ eq (combine a id) ≡ a

关键说明 #

Agda无法直接将命题相等“强制”视为定义相等，但可以通过subst、rewrite（函数定义中使用）、transport等工具，基于命题相等调整类型，让类型检查器接受逻辑合法的相等项。

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