I'm not an expert, I don't know how the community would treat such enums. I think the bottom line is if you can't fail to shuffle the cards, whether through an interesting enums and matching mechanism or through some other part of the type system, then you're good.

I've never used idris, but as far as I understand it encoding state machines in the type system is exactly the kind of thing type-dependent languages in general and idris in particular shine at. This is the prototypical example given, and it's the one Mathew Farwell himself gives in a podcast interview [1]

[1] software engineering radio, episode 296, http://feedproxy.google.com/~r/se-radio/~5/Kg1Py4rd2i0/SE-Ra...