The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Samuel E. Moelius III wrote:
> What about in a more general setting?  Does anyone know of an example 
> of type family which can be easily expressed/manipulated as an 
> inductive definition, but cannot be so easily expressed/manipulated as 
> a recursive definition?

Most type families don't make sense as recursive definitions.  The 
general trick only works when the family parameters determine the 
"skeleton" of the inhabiting values.  For instance, representing 
abstract syntax trees for programming languages with recursive 
definitions is probably almost always going to bring nothing but pain.