Brief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.