diverges_conflict: @[diverges] where termination is claimed or needed

@[diverges] marks a function that is not claimed to terminate: an event loop, a server’s accept loop, a poll that waits for another task. The checker files no termination obligation for it and never assumes its return type at its own recursive calls.

Two other attributes say the opposite, so a function cannot carry either of them together with @[diverges]:

• @[decreases(...)] claims a metric that falls at every recursive call, which would prove the function does terminate;
• @[measure] makes the function part of the logic the refinement checker reasons in, and a measure must terminate to be a consistent definition.

A measure that calls a @[diverges] function, directly or through other calls, is the same contradiction one step removed, and gets this error too.

A program that triggers it

mod Main do
  @[diverges]
  @[decreases(n)]
  fn down(n : Int) : Int do
    if n <= 0 do 0 else down(n - 1) end
  end

  fn main() do
    down(3)
  end
end

The fix

Keep the attribute that is true. down terminates, so drop @[diverges]:

mod Main do
  @[decreases(n)]
  fn down(n : Int) : Int do
    if n <= 0 do 0 else down(n - 1) end
  end

  fn main() do
    down(3)
  end
end

For a loop that really runs until something outside the program stops it, keep @[diverges] and drop @[decreases]. A measure must not depend on such a loop at all.

Why the rule exists

A metric on a function that is declared to diverge is either false or makes the @[diverges] pointless, and a measure that may not return is an inconsistent axiom: from it, the checker could prove anything. Callers of a @[diverges] function are not required to repeat it; “may diverge” is inferred for them, and --termination-report lists them.

See also: the language reference, termination_unproved.