Small questions about injective type families

[jstolarek]

#6018

Short-term todos:

• [ ] Note [Branched instance checking] in FamInstEnv.hs does not exist but is referenced from OptCoercions and CoAxiom

Questions:

• [ ] what are branch indices?
• [ ] I don't understand axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char from Note [Coercion axiom branches] in CoAxiom.lhs
• [ ] what are inert reactions and spontaneous reactions
• [x] what are BuiltInSynFamTyCon ?

[jstolarek]

• I haven't considered coincident overlap for open type families.
• perhaps I should redefine my algorithm in terms of "compatibility"? For open type families every pair of equations needs to be compatible. If this is already being checked then I guess I should check for injectivity together with compatibility.

type family C a b 
type instance C Int b = Int
type instance C a Bool = a

Will my algorithm detect correctly that this is not injective? EDIT: Richard's criterion that all tyvars declared on LHS should be on the RHS should deal with this.