由于定义相等性约束，Agda不允许我用匹配类型的术语填充类型的孔

Question

这是具有此错误的程序的精简版本：

open import Data.Empty using (⊥-elim)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; punchOut; punchIn; _≟_)
  renaming (zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Relation.Nullary using (yes; no; ¬_)

private
  variable
    n : ℕ

data Type : Set where
  _⇒_ : Type → Type → Type
  T : Type

data Term : ℕ → Set where
  abs : Type → Term (suc n) → Term n
  app : Term n → Term n → Term n
  var : Fin n → Term n

data Ctx : ℕ → Set where
  ● : Ctx 0
  _,-_ : Ctx n → Type → Ctx (suc n)

-- | Increments the variables that are free relative to the inserted "pivot" variable.
lift : Term n → Fin (suc n) → Term (suc n)
lift (abs ty body) v = abs ty (lift body (fsuc v))
lift (app f x) v = app (lift f v) (lift x v)
lift (var n) v = var (punchIn v n)

_[_≔_] : Term (suc n) → Fin (suc n) → Term n → Term n
(abs ty body) [ v ≔ def ] = abs ty (body [ fsuc v ≔ lift def fzero ])
(app f x)     [ v ≔ def ] = app (f [ v ≔ def ]) (x [ v ≔ def ])
(var n)       [ v ≔ def ] with v ≟ n
... | yes refl = def
... | no neq = var (punchOut {i = v} {j = n} λ { refl → neq (sym refl)})

find : Ctx n → Fin n → Type
find (Γ ,- A) fzero = A
find (Γ ,- A) (fsuc n) = find Γ n

private
  variable
    Γ : Ctx n
    a b c f x : Term n
    A B C : Type
    v : Fin n

data _∋_⦂_ : Ctx n → Fin n → Type → Set where
  vzero : (Γ ,- A) ∋ fzero ⦂ A
  vsuc : (Γ ∋ v ⦂ A) → (Γ ,- B) ∋ fsuc v ⦂ A

lookup : (Γ : Ctx n) → (v : Fin n) → Γ ∋ v ⦂ find Γ v
lookup (Γ ,- A) fzero = vzero
lookup (Γ ,- B) (fsuc v) = vsuc (lookup Γ v)

data _⊢_⦂_ : Ctx n → Term n → Type → Set where
  ty-abs : (Γ ,- A) ⊢ b ⦂ B → Γ ⊢ abs A b ⦂ (A ⇒ B)
  ty-app : Γ ⊢ f ⦂ (A ⇒ B) → Γ ⊢ x ⦂ A → Γ ⊢ app f x ⦂ B
  ty-var : Γ ∋ v ⦂ A → Γ ⊢ var v ⦂ A

-- | Inserts a binding in the middle of the context.
liftΓ : Ctx n → Fin (suc n) → Type → Ctx (suc n)
liftΓ Γ fzero t = Γ ,- t
liftΓ (Γ ,- A) (fsuc v) t = (liftΓ Γ v t) ,- A

weakening-var
  : ∀ {Γ : Ctx n} {v' : Fin (suc n)} → Γ ∋ v ⦂ A → liftΓ Γ v' B ∋ Data.Fin.punchIn v' v ⦂ A
weakening-var {v' = fzero} vzero = vsuc vzero
weakening-var {v' = fsuc n} vzero = vzero
weakening-var {v' = fzero} (vsuc v) = vsuc (vsuc v)
weakening-var {v' = fsuc n} (vsuc v) = vsuc (weakening-var v)

weakening
  : ∀ {Γ : Ctx n} {v : Fin (suc n)} {t : Type} → Γ ⊢ a ⦂ A → liftΓ Γ v t ⊢ lift a v ⦂ A
weakening (ty-abs body) = ty-abs (weakening body)
weakening (ty-app f x) = ty-app (weakening f) (weakening x)
weakening (ty-var v) = ty-var (weakening-var v)

lemma : ∀ {Γ : Ctx n} → (v : Fin (suc n)) → liftΓ Γ v B ∋ v ⦂ A → A ≡ B
lemma fzero vzero = refl
lemma {Γ = _ ,- _} (fsuc fin) (vsuc v) = lemma fin v

subst-eq
  : (v : Fin (suc n))
  → liftΓ Γ v B ∋ v ⦂ A
  → Γ ⊢ b ⦂ B
  → Γ ⊢ var v [ v ≔ b ] ⦂ A
subst-eq fzero vzero typing = typing
subst-eq {Γ = Γ ,- C} (fsuc fin) (vsuc v) typing with fin ≟ fin
... | yes refl rewrite lemma fin v = typing
... | no neq = ⊥-elim (neq refl)

subst-neq
  : (v v' : Fin (suc n))
  → liftΓ Γ v B ∋ v' ⦂ A
  → (prf : ¬ v ≡ v')
  → Γ ∋ (Data.Fin.punchOut prf) ⦂ A
subst-neq v v' v-typing neq with v ≟ v'
... | yes refl = ⊥-elim (neq refl)
subst-neq fzero fzero _ _ | no neq = ⊥-elim (neq refl)
subst-neq {Γ = Γ ,- C} fzero (fsuc fin) (vsuc v-typing) _ | no neq = v-typing
subst-neq {Γ = Γ ,- C} (fsuc fin) fzero vzero _ | no neq = vzero
subst-neq {Γ = Γ ,- C} (fsuc fin) (fsuc fin') (vsuc v-typing) neq | no _ =
  vsuc (subst-neq fin fin' v-typing λ { assump → neq (cong fsuc assump) })

subst
  : ∀ {Γ : Ctx n}
  → liftΓ Γ v B ⊢ a ⦂ A → Γ ⊢ b ⦂ B
  → Γ ⊢ a [ v ≔ b ] ⦂ A
subst (ty-abs body) typing = ty-abs (subst body (weakening typing))
subst (ty-app f x) typing = ty-app (subst f typing) (subst x typing)
subst {v = v} {Γ = _} (ty-var {v = v'} v-typing) typing with v' ≟ v
... | yes refl = subst-eq v v-typing typing
subst {v = fzero} (ty-var {v = fzero} v-typing) typing | no neq = ⊥-elim (neq refl)
subst {v = fzero} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq = ty-var v-typing
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fzero} vzero) typing | no neq = ty-var vzero
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq
  with v ≟ v'
... | yes eq = ⊥-elim (neq (cong fsuc (sym eq)))
... | no neq' = ty-var (vsuc (subst-neq v v' v-typing {!neq'!}))

因为我不知道错误的原因，所以我不确定如何在一个简单的程序中重现它。

将焦点对准打孔：

Goal: ¬ v ≡ v'
————————————————————————————————————————————————————————————
typing   : (Γ ,- C) ⊢ b ⦂ B
v-typing : liftΓ Γ v B ∋ v' ⦂ A
neq      : fsuc v' ≡ fsuc v → Data.Empty.⊥
C        : Type
Γ        : Ctx n
b        : Term (suc n)   (not in scope)
A        : Type   (not in scope)
B        : Type   (not in scope)
neq'     : ¬ v ≡ v'
v'       : Fin (suc n)
v        : Fin (suc n)
n        : ℕ   (not in scope)

[neq'显然具有与孔相同的类型，并且没有列出相同项。

但是，当我尝试用neq'填充孔时，出现以下错误：

(neq' x) !=
((λ { refl
        → Relation.Nullary.Reflects.invert (Relation.Nullary.ofⁿ neq')
          (Data.Fin.Properties.suc-injective (sym refl))
    })
 (cong fsuc x))
of type Data.Empty.⊥
when checking that the expression neq' has type ¬ v ≡ v'

什么给了？

• 此平等约束来自何处？
• 由于Data.Empty.⊥无人居住，难道所有居民都是平等的吗？为什么平等约束很重要？

我正在使用Agda 2.6.1版和标准库1.3版。

Answer 1

平等约束来自整个右侧形式的目标

(Γ ,- C) ⊢ 
  var (fsuc (punchOut 
             (λ x →
                (λ { refl → neq' (Data.Fin.Properties.suc-injective (sym refl)) })
                (cong fsuc x))))
  ⦂ A

虽然您建议的证据的推断类型是

(Γ ,- _B_480) ⊢ var (fsuc (punchOut neq')) ⦂ A

[Agda指出，这些类型可以匹配的唯一方法是neq'等于更复杂的证明，这就是得到错误的原因。

关于⊥中的函数相等性，Agda不假定它们在定义上都相等，因为这通常会导致不确定的类型检查。

好消息是，阿格达（Agda）已经知道这里的证明！因此，如果您将目标替换为_，它将推断应该去哪里。

... | no neq' = ty-var (vsuc {B = C} (subst-neq v v' v-typing _))