類型錯誤試圖模式匹配的東西，應該是荒謬反正

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)