У let loop = loop in if loop then Just 1 else Nothing тип Maybe Int, и это выражение ни Just, ни Nothing. Тип не делает его тотальным. Это становится важно, когда вычислитель останавливается по исчерпании бюджета шагов. Должна ли обёртка в этот момент сказать NotFound? По-моему, нет, правильный ответ - Unfinished. NotFound принадлежит поиску, который завершился и показал отсутствие. Исчерпанный бюджет ничего не доказывает о том, нашли бы дополнительные шаги решение или нет.
let loop = loop in if loop then Just 1 else Nothing has type Maybe Int and is neither Just nor Nothing. The type doesn't make it total. That matters once an evaluator halts after a step budget. When the budget runs out, should the wrapper say NotFound? I'd say no, and return Unfinished. NotFound belongs to a search that completed and showed absence. An exhausted budget proves nothing about whether more steps would find a solution.