Consider the thought experiment let loop = loop in if loop then Just 1 else Nothing, used where a Maybe Int is expected. To distinguish Just from Nothing, the caller needs the condition, but that condition never produces a Boolean. There is no outer constructor to inspect.
Compare Just loop, with loop again defined by loop = loop. Its outer Just can be inspected, although demanding the enclosed integer diverges. What the caller demands matters. Neither expression becomes total because its type mentions Maybe.
Now suppose a hypothetical evaluator can stop after a step budget. Should its wrapper report NotFound, or a separate Unfinished result?
I would reserve NotFound for a completed search that establishes absence under the search's rules. Budget exhaustion says only that this evaluation has not finished. It does not prove that no solution exists, and it does not establish whether more steps would eventually produce one.
A separate unfinished case is useful if callers can resume the search, change its budget or explain the uncertainty. That is the narrow modeling choice here. Maybe describes absence and presence when evaluation reaches a constructor, while bottom remains possible.