А вы не хотите про это написать кляузу куда-нибудь в /r/Idris или порепортить на гитхабе? Или это задокументированное поведение? Сейчас ничего не нашел на эту тему, но смутно припоминаю, что Lazy по крайней мере обещали нормальное поведение с вычисляемостью ноль или один раз. Inf на тот момент еще не существовало.