失败块

失败块允许用户检查某些代码虽然能通过解析但在细化阶段被拒绝。其最简单的形式是使用关键字 failing 后跟一些缩进的 Idris 代码：

failing
  trueNotFalse : True === False
  trueNotFalse = Refl

将上述代码放入文件并让 Idris 检查它不会产生错误消息，因为 failing 块中的代码被拒绝了，即失败了。

failing 关键字可以选择性地接受一个字符串参数。如果提供了该参数，附加到失败块的字符串将与产生的错误消息进行比对，以检查它是否出现在错误中。这使用户可以记录块中预期的错误类型，同时验证错误消息确实符合我们的预期。例如，在下面的例子中，我们确保 Idris 在统一字符 'a' 和 'b' 时抛出错误，从而拒绝它们相等的证明：

failing "When unifying"
  noteq : 'a' === 'b'
  noteq = Refl

失败块在演示程序或示例中的错误路径或起点时很有用。失败块中允许使用有效的代码，因此只要块中至少有一个语句失败（不必是第一个或最后一个语句！），就可以使用中间辅助函数：

failing "Mismatch between: Integer and Double"
  record Point where
    constructor MkPoint
    x : Integer
    y : Integer

  Origin : Point
  Origin = MkPoint 0 0

  dist : Point -> Point -> Integer
  dist p1 p2 = sqrt $ (pow (p2.x - p1.x) 2) + (pow (p2.y - p1.y) 2)

无效的失败块

如果失败块没有失败，即其中的代码在细化阶段被接受，编译器将报告错误：

failing
  validRefl : 1 === 1
  validRefl = Refl

检查上述代码会得到：

Error: Failing block did not fail.

同样，如果提供了预期的错误（子）字符串但错误输出不匹配，我们会得到：

Error: Failing block failed with the wrong error.

后面跟着给定的预期错误字符串和实际的错误输出，允许我们进行比较和对比。

每个错误一个块

注意为每个要检查的内容使用单独的 ``failing`` 块。 使用单个块可能导致意外结果。以下示例通过，因为第二个语句失败：

failing
  stmt1 : True === True
  stmt1 = Refl

  -- at least one failing statement, so the block is accepted
  stmt2 : 'a' === 'b'
  stmt2 = Refl

  stmt3 : 1 === 1
  stmt3 = Refl

相反，将语句分离到单独的失败块中：

failing
  stmt1 : True === True
  stmt1 = Refl

failing
  stmt2 : 'a' === 'b'
  stmt2 = Refl

failing
  stmt3 : 1 === 1
  stmt3 = Refl

这会发出两个 Error: Failing block did not fail 消息，正如预期的那样。