Agda不允许使用匹配类型的项填充类型空洞，因为在类型空洞中可能存在定义上的相等约束。相等约束是指在类型空洞中使用了可以在运行时进行比较的项，这会导致类型检查器无法确定该项的具体类型。为了解决这个问题，可以使用Agda的“with”表达式来处理匹配类型的情况。下面是一个示例代码：

open import Data.Empty
open import Data.Nat

data Even : ℕ → Set where
  even-zero : Even 0
  even-suc  : {n : ℕ} → Even n → Even (suc (suc n))

data Odd : ℕ → Set where
  odd-one  : Odd 1
  odd-suc  : {n : ℕ} → Odd n → Odd (suc (suc n))

even-or-odd : (n : ℕ) → Even n ⊎ Odd n
even-or-odd zero = inj₁ even-zero
even-or-odd (suc zero) = inj₂ odd-one
even-or-odd (suc (suc n)) with even-or-odd n
... | inj₁ ev = inj₂ (odd-suc ev)
... | inj₂ od = inj₁ (even-suc od)

在这个例子中，我们定义了两个归纳类型Even和Odd，它们表示自然数的偶数和奇数。然后我们定义了一个函数even-or-odd，它接受一个自然数作为参数，并返回一个Even n类型或Odd n类型的证明。在函数的定义中，我们使用了with表达式来处理匹配类型的情况。当我们在suc (suc n)上调用even-or-odd时，我们通过使用even-or-odd n来进行模式匹配，从而使用先前的证明构造新的证明。

使用with表达式可以避免使用匹配类型的项填充类型空洞时出现定义上的相等约束。相反，它允许我们根据已知的证明来构造新的证明，从而保证类型的一致性。