Strange program that requires incoherent instances yet always seems to pick the "right" one?

Question

Consider the following program, which only compiles with incoherent instances enabled:

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}

main = do
  print (g (undefined :: Int))
  print (g (undefined :: Bool))
  print (g (undefined :: Char))

data True

class CA t where
  type A t; type A t = True
  fa :: t -> String
instance CA Int where
  fa _ = "Int"

class CB t where
  type B t; type B t = True
  fb :: t -> String
instance CB Bool where
  fb _ = "Bool"

class CC t where
  type C t; type C t = True
  fc :: t -> String
instance CC Char where
  fc _ = "Char"

class CAll t t1 t2 t3 where
  g :: (t1 ~ A t, t2 ~ B t, t3 ~ C t) => t -> String

instance (CA t) => CAll t True  t2   t3  where g = fa
instance (CB t) => CAll t  t1  True  t3  where g = fb
instance (CC t) => CAll t  t1   t2  True where g = fc

When compiling without incoherent instances it claims multiple instances match. This would seem to imply that when incoherent instances are allowed, the instances would be chosen arbitrarily.

Unless I'm exceedingly lucky, this would result in compile errors as the instance constraints in most cases would not be satisfied.

But with incoherent instances I get no compile errors, and indeed get the following output with the "correct" instances chosen:

"Int"
"Bool"
"Char"

So I can only conclude either one of a few things here:

1. GHC is backtracking on instance context failures (something it says it doesn't do in it's own documentation)
2. GHC actually knows there's only one instance that matches, but isn't brave enough to use it unless one turns on incoherent instances
3. I've just got exceedingly lucky (1 in 3³ = 27 chance)
4. Something else is happening.

I suspect the answer is 4 (maybe combined with 2). I'd like any answer to explain what's going on here, and how much I can rely on this behavior with incoherent instances? If it's reliable it seems I could use this behaviour to make quite complex class hierarchies, that actually behave somewhat like subtyping, e.g. I could say all types of class A and class B are in class C, and an instance writer could make an instance for A without having to explicitly make an instance for C.

Edit:

I suspect the answer has something to do with this in the GHC docs:

1. Find all instances I that match the target constraint; that is, the target constraint is a substitution instance of I. These instance declarations are the candidates.
2. Eliminate any candidate IX for which both of the following hold:
   • There is another candidate IY that is strictly more specific; that is, IY is a substitution instance of IX but not vice versa.
   • Either IX is overlappable, or IY is overlapping. (This "either/or" design, rather than a "both/and" design, allow a client to deliberately override an instance from a library, without requiring a change to the library.)

3. If exactly one non-incoherent candidate remains, select it. If all remaining candidates are incoherent, select an arbitary one. Otherwise the search fails (i.e. when more than one surviving candidate is not incoherent).

4. If the selected candidate (from the previous step) is incoherent, the search succeeds, returning that candidate.

5. If not, find all instances that unify with the target constraint, but do not match it. Such non-candidate instances might match when the target constraint is further instantiated. If all of them are incoherent, the search succeeds, returning the selected candidate; if not, the search fails.

Correct me if I'm wrong, but whether incoherent instances is selected or not, in the first step, there's only one instance that "matches". In the incoherent case, we fall out with that "matched" case at step 4. But in the non-incoherent case, we then go to step 4, and even though only one instance "matches", we find other instances "unify". So we must reject.

Is this understanding correct?

And if so, could someone explain exactly what "match" and "unify" mean, and the difference between them?