That's exactly what I mentioned in the second note. Of course, even though the collections of all values of a given type may not be finite; this encoding does give a specification of a finite subset of values from that type. Thus, it can be considered an alternative to strict lists for ensuring finiteness of a collection.

Of course, as an attempt to enumerate all values in the type, your instance isn't morally correct. In this case, the morality in question can be enforced with dependent types. Can you find any way to break the dependent version? (nontermination doesn't count.)