类型错误试图模式匹配的东西，应该是荒谬反正

Question

在类型检查的简单类型的演算中间的时候，我有这样的：

check Γ (lam τ′ E) (τ₁ ↣ τ₂) with τ′ T≟ τ₁ 
check Γ (lam τ′ E) (τ₁ ↣ τ₂) | no ¬p = no lem 
    where 
    lem : ¬ Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) 
    lem t = {!!} 

类型的孔是当然，⊥。我希望通过对t进行模式匹配，我可以充分了解这种类型的推导，以证明它是荒谬的。但是，如果我做t的情况分析，我得到这个：

lem : ¬ Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) 
lem (tLam t) = ? 

τ′ != τ₁ of type Type 
when checking that the pattern tLam t has type 
Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) 

是的，这非常的一点是要证明，没有什么的地方，t来写，因为τ■不要匹配...但我怎么告诉Agda？

仅供参考，以下是完整的（简化，但完整）模块：

open import Data.Nat 
open import Data.Fin 
open import Data.Vec 
open import Function using (_∘_) 

data Type : Set where 
    _↣_ : Type → Type → Type 

infixr 20 _↣_ 

open import Relation.Nullary 
open import Relation.Binary.PropositionalEquality 

arr-injˡ : ∀ {τ τ′ τ₂ τ₂′} → τ ↣ τ₂ ≡ τ′ ↣ τ₂′ → τ ≡ τ′ 
arr-injˡ refl = refl 

arr-injʳ : ∀ {τ τ′ τ″} → τ ↣ τ′ ≡ τ ↣ τ″ → τ′ ≡ τ″ 
arr-injʳ refl = refl 

_T≟_ : (τ τ′ : Type) → Dec (τ ≡ τ′) 
(τ₁ ↣ τ₂) T≟ (τ₁′ ↣ τ₂′) with τ₁ T≟ τ₁′ 
(τ₁ ↣ τ₂) T≟ (τ₁′ ↣ τ₂′) | no ¬p = no (¬p ∘ arr-injˡ) 
(τ₁ ↣ τ₂) T≟ (.τ₁ ↣ τ₂′) | yes refl with τ₂ T≟ τ₂′ 
(τ₁ ↣ τ₂) T≟ (.τ₁ ↣ .τ₂) | yes refl | yes refl = yes refl 
(τ₁ ↣ τ₂) T≟ (.τ₁ ↣ τ₂′) | yes refl | no ¬p = no (¬p ∘ arr-injʳ) 

data Expr (n : ℕ) : Set where 
    lam : (τ : Type) → Expr (suc n) → Expr n 

Ctxt : ℕ → Set 
Ctxt = Vec Type 

data _⊢_∷_ : ∀ {n} → Ctxt n → Expr n → Type → Set where 
    tLam : ∀ {n} {Γ : Ctxt n} {τ E τ′} → ((τ ∷ Γ) ⊢ E ∷ τ′) → (Γ ⊢ lam τ E ∷ τ ↣ τ′) 

⊢-inj : ∀ {n Γ} {E : Expr n} → ∀ {τ τ′} → Γ ⊢ E ∷ τ → Γ ⊢ E ∷ τ′ → τ ≡ τ′ 
⊢-inj {E = lam τ E} (tLam t) (tLam t′) = cong (_↣_ τ) (⊢-inj t t′) 

module Infer where 
    check : ∀ {n} Γ → (E : Expr n) → ∀ τ → Dec (Γ ⊢ E ∷ τ) 
    check Γ (lam τ′ E) (τ₁ ↣ τ₂) with τ′ T≟ τ₁ 
    check Γ (lam τ′ E) (.τ′ ↣ τ₂) | yes refl with check (τ′ ∷ Γ) E τ₂ 
    check Γ (lam τ′ E) (.τ′ ↣ τ₂) | yes refl | yes E∷τ₂ = yes (tLam E∷τ₂) 
    check Γ (lam τ′ E) (.τ′ ↣ τ₂) | yes refl | no ¬t = no lem 
    where 
    lem : ¬ Γ ⊢ lam τ′ E ∷ (τ′ ↣ τ₂) 
    lem (tLam t) = ¬t t 
    check Γ (lam τ′ E) (τ₁ ↣ τ₂) | no ¬p = no lem 
    where 
    lem : ¬ Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) 
    lem (tLam t) = ? 

Answer 1

嗯，我不知道这是最好的解决办法，但面对这样的问题，你平时看围绕上下文，看看你可以从哪里得到⊥并试图证明一个导致它的财产。

特别地，您不能在t上模式匹配，因为如您所说，τ′ ≠ τ₁（这是您的一个假设）。但看的tLam的定义，它应该是可以证明：

lam-T≡ : ∀ {n τ₁ τ₂ τ′} {Γ : Ctxt n} {E : Expr (suc n)} → 
     Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) → τ′ ≡ τ₁ 

而事实上，这样的话：

lam-T≡ (tLam t) = refl 

这给你一个证明¬p需求：

lem : ¬ Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) 
lem t = ¬p (lam-T≡ t)