data and co-data are kind of like the -X and +X modalities in Prolog programs. Most of the time, it doesn't matter which one you use, but sometimes you need to write it backwards.

Seeing the paper at http://www.jucs.org/jucs_10_7/total_functional_programming/j... it's more related to proofs, and indeed Idris seems somewhat similar to Coq (a "programming" language for writing proofs). Or maybe I'm just totally lost.