这个问题通常出现在使用归纳类型和递归函数时。当我们在函数中匹配模式时，Agda应该会自动推导剩余的部分。但有时Agda似乎无法确定剩余部分是否会导致死循环或不可终止。这时，Agda在类型检查器中留下了残留的目标，即没有解决的模式匹配子句。

要解决这个问题，有几种方法可供尝试:

1.使用朴素递归而非结构递归。朴素递归是一种从上到下的递归方式，它不会考虑特定的归纳类型结构。这可能会使代码更难以理解，但通常会防止此类问题发生。

2.使用'with”表达式展开模式。"with"表达式用于将模式匹配分解为多个步骤。这有助于Agda更好地理解代码，并消除未消除的模式匹配子句。

3.通过引入自然数等规范形式，让Agda更容易推断结果。结构递归中的问题通常出现在归纳类型的更高级变量（例如长度等）上。通过使用规范形式（例如，Nat而不是ℕ），让Agda更容易推断结果。这有助于消除未解决的模式匹配子句。

例子:

以下是使用"with"表达式展开模式的例子:

data List (A : Set) : Set where
  nil : List A
  cons : A -> List A -> List A

head : {A : Set} -> List A -> A
head {A} (cons x xs) = x
head {A} nil = ?

当我们尝试编写'head nil”的目标时，Agda会留下未解决的子句。为了解决这个问题，我们可以使用"with"表达式展开模式。

head-nil : {A : Set} -> head (nil : List A) = ??
head-nil = {!!}
  with (nil : List A)
  head-nil | nil = {!!}