I'm re-reading the Instance Chains paper. http://dl.acm.org/citation.cfm?id=1863596 [2010, so before Type Families got off the ground] And wondering about some of [*] their motivating examples. [Disclaimer: with a view to writing up something I think is better.] Leaving aside the question of backtracking on instance non-match, would anybody write a type-level GCD like this? We have the usual type-level Naturals and Booleans:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, OverlappingInstances, EmptyDataDecls #-}

data Z; data S n

data T; data F

And then:

class Gcd m n p | m n → p --p=gcd(m,n) instance Gcd m m m -- OVERLAPPABLE OK instance (Lte n m T, Subt m n m', Gcd m' n p) ⇒ Gcd m n p instance (Lte n m F, Subt n m n', Gcd m n' p) ⇒ Gcd m n p

Those latter two instances overlap (heads are identical) in an irresolvable way. (They're trying to distinguish the `m > n` vs `m < n` cases.) The code is closely following how you might write with Integers, I guess. But I'm not convinced it's such a good approach for Peanos. Class Lte compares two Peanos, tells which is the larger. Class Subt subtracts one from the other. They're both traversing the (S (S (S ... Z...))) nesting. (And Subt needs a nasty kludge in case you're trying to subtract the larger: it returns Z.) I think these days (esp with TypeFamilies/Assoc types), I'd write those latter two instances with a case helper. And a discriminator type fun `Diff` that provides the absolute diff, and tells which param is smaller. But to keep in the same style, I'll put `Diff` as a class:

instance (Diff m n d, GcdCase d m n p) => Gcd m n p -- single 'catch all' instance

class GcdCase d m n p | d m n -> p instance (Gcd d' n p) => GcdCase (T, d') m n p instance (Gcd m d' p) => GcdCase (F, d') m n p

class Diff m n d | m n -> d instance Diff Z (S n') (T, S n') instance Diff (S m') Z (F, S m') instance (Diff m' n' d) => Diff (S m') (S n') d

Seems to me the code is more succinct, and easier to follow. (And by the way doesn't need egregious overlaps.) [*] Actually, I'm dubious about all of their examples. More to follow ... AntC