Type error when trying to pattern-match on something that should be absurd anyway

Question

In the middle of a type checker for the simply-typed lambda calculus, I have this:

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

The type of the hole is, of course, ⊥. I'd hope that by pattern-matching on t, I can learn enough about this type derivation to prove that it is absurd. However, if I do a case analysis on t, I get this:

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

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

Yes, the very point of this is to prove that there's nothing to write in place of that t because the τs don't match... but how do I tell that to Agda?

For reference, here's the full (simplified, but complete) module:

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

Well, I'm not sure if this is the best solution, but when faced with problems like this, you usually look around the context to see where you can get ⊥ and try to prove a property that leads to it.

Specially, you can't pattern match on t because, as you said, τ′ ≠ τ₁ (which is one of your assumptions). But looking at the definition of tLam, it should be possible to prove that:

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

And indeed, this is the case:

lam-T≡ (tLam t) = refl

This gives you a proof that ¬p needs:

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