[Apologies for breaking threading...] On Wed May 31, Anthony Clayden wrote:

Leaving aside the question of backtracking on instance non-match, would anybody write a type-level GCD like this?

Your question seems to be "would you use the standard recursive statement of Euclid's algorithm to demonstrate Euclid's algorithm?" This certainly seemed to be a reasonable idea in 2010. If your concern is efficiency, I suggest that not using Peano numerals at all is probably a more profitable direction.

(And Subt needs a nasty kludge in case you're trying to subtract the larger: it returns Z.)

What you call a nasty kludge, I call a standard operation on commutative monoids. [https://en.wikipedia.org/wiki/Monus]

I think these days (esp with TypeFamilies/Assoc types),

You seem to be discovering that closed instance chains can be implemented by writing out truth tables. I discussed this transformation at length, and suggested that doing might make your code harder to write and to read, in my Haskell 2015 paper "Variations on Variants". Of course, you'll have an easier time of it if you limit yourself to only considering type-level definitions, and not the corresponding method definitions. But doing so rather misses the point of instance chains. /g -- Prosperum ac felix scelus virtus vocatur -- Seneca