[Agda] Help debugging

[Stefan Monnier]

If I pass the code below to Agda-2.2.2, I get the following error,
highlithing the "inHere" argument on the last line:

   /home/monnier/tmp/foo.agda:23,38-44
   Failed to solve the following constraints:
     _40 extBase == Δ : Context
     _41 extBase == τ : Exp (_40 extBase)
   when checking that the pattern inHere has type
   _41 extBase ∈ (Δ :: τ)

If I use the second-to-last line instead, I get another error,
highlighting the same "inHere" argument:

   /home/monnier/tmp/foo.agda:22,17-23
   Δ != _40 extBase of type Context
   when checking that the pattern inHere has type
   _41 extBase ∈ (Δ :: τ)

Could someone explain to me what's going on and/or how I can get Agda's
type checker to accept the code?


        Stefan


module foo where

open import Data.Nat
-- open import Data.List


mutual
  data Context : Set where
    • : Context
    _::_ : (Δ : Context) → Exp Δ → Context

  data Exp (Δ : Context) : Set where
    unit  : Exp Δ

  data _∈_ {Δ} (t : Exp Δ) : Context → Set where
    inHere : t ∈ (Δ :: t)

data Extend (Δ : Context) : Context → Set where
  extBase : Extend Δ Δ

problem : ∀{Δ τ Δ' t} → (P' : Extend (Δ :: τ) Δ') → t ∈ Δ' → ℕ
-- problem extBase inHere = zero
problem{Δ}{τ}{.(Δ :: τ)}{.τ} extBase inHere = zero