OptionTrees
In ML (and Coq, and Haskell by another name) there is a type operator called option; an option X is either the special value None or else a value of type X. It's the stronglytyped language version of a value that might be the nullpointer.
A (tree (option X)) is a tree whose leaves are option X's.
Given an optiontree, you can get back the unique list X consisting of its leaves, in order. In the reverse direction the mapping is not unique.

If there is one thing I've suffered greatly in order to learn about dependentlytyped programming, it is that one should never attempt to concatenate lists. If you find yourself doing this, you probably ought to be using optiontrees instead. 
I don't know for sure why this advice is so useful, but here are three clues:

The theory of lists undecidable because it is the same as the theory of monoids (one binary operator, an axiom making it associative, one constant, and axioms making it neutral). Even the theory of semigroups (take away the constant) is still undecidable. But the theory of trees is the same as the theory of magmas (one binary operator, no axioms) and of optiontrees (one binary operator, one constant, no axioms)
Why worry about this? Typechecking must be decidable. If your types are able to interpret an undecidable theory, you will necessarily encounter valid terms which the typechecker cannot accept in the absence of some humanprovided proof about equality between types. Equality between types (rather than values) is, at the moment, a very poorlyunderstood (and poorly developed) part of type theory.

Strict monoidal categories are evil. Optiontrees are to lists what monoidal categories are to strict monoidal categories.

(Most vague:) redundant representations are a very powerful tool in computer science. Observe that decrementing an nbit counter takes O(log n) time using the usual binary representation; there is a way to get O(1)time decrements by allowing three possible values for each bit (but remaining at radix2). The multiple redundant optiontree representations for a particular list seem to add just the right amount of flexibility in the same way.
