Hmmm. That's interesting. I have a slightly different problem and I don't know if it's relevant or not. I have nested algebraic data types for things like expressions with terms and operators and whatever too, and some of my functions do a transformation that removes all instances of particular constructors (by expressing them in other ways) but that leaves most of the data structure intact. I'd love to use the type system to enforce the constraint that the result from the transformer function has eliminated occurrences of certain constructors within the nested type, but to do that I seem to have to create a whole other near-copy of the data declarations with slightly different names and the occasional constructor missing. I wonder if there's a better way. -- Mark