For good or ill, Simon doesn't want RULES for datacons. T12689 has to be removed (leaving T12689a, which is still fine). But I don't know enough about what you're doing with T12689broken to know how to make it express the right idea after this change. Can you please advise? Thanks, David Feuer Well-Typed LLP