let loop = loop in if loop then Just 1 else Nothing has type Maybe Int, and it is neither Just nor Nothing. To tell which, a caller needs the condition, and the condition never produces a Boolean. There is no outer constructor to inspect.
Just loop, with the same loop = loop, behaves differently. Its outer Just can be inspected, and only demanding the enclosed integer diverges. What the caller demands is what matters. Mentioning Maybe in the type makes neither expression total.
This stops being academic once an evaluator can halt after a step budget. When the budget runs out, should its wrapper report NotFound, or return its own Unfinished result?
My answer is Unfinished. NotFound belongs to a completed search that has shown absence under the search's rules. An exhausted budget means this evaluation has not finished. It proves nothing about whether a solution exists, or whether more steps would eventually find one.
The extra case earns its place if callers can resume the search, change its budget or explain the uncertainty. If callers treat both cases alike, the extra distinction has little value. Maybe describes absence and presence when evaluation reaches a constructor, and bottom stays possible either way.
