I find that Lazy and Inf is very close:
Lazy and Inf are closely related (in fact, the underlying implementation uses the same type). The only difference in practice is in totality checking, where Lazy is erased (i.e. terms are checked for termination normally, ignoring laziness annotations), and Inf uses a productivity checker, where any use of Delay must be constructor guarded.
As described above, the underlying implementation of Lazy and Inf is the same one, the only difference is about totality checking.
I think always use Inf seems much more natural, which is more close to the lazy we used in Haskell, and wondering what is the scene in production which we must use Lazy -- which always do a deep totality checking?