GHC and type-family rewriting?

[Benjamin Redelings]

Hi,

I've managed to code up implications and GADTs, and am now working on 
adding type families.  I've been following the OutsideIn paper, but it 
seems that GHC is not really following the same plan for the solver.  
For example, instead of replacing every type family with a metavariable, 
it only does this for occur-check failures.  It talks about "cycle 
breakers" instead of "flattening substitutions".  It creates flatting 
substitutions for both givens and wanteds (I think). And I see this note:

> -- | A 'Xi'-type is one that has been fully rewritten with respect
> -- to the inert set; that is, it has been rewritten by the algorithm
> -- in GHC.Tc.Solver.Rewrite. (Historical note: 'Xi', for years and years,
> -- meant that a type was type-family-free. It does *not* mean this
> -- any more.)
> type Xi = TcType

If I'm understanding correctly, the inert set is now thought of as a 
"generalized substitution" that replaces either an LHS (untouchable type 
variables or type family applications) with an RHS.

I guess what I'm wondering is:

(Q1) Did GHC evolve to this point starting from something fairly close 
to the OutsideIn paper?

(Q2) Is the new approach (i.e. eager type family rewriting) mostly to 
making rewriting faster?

(Q3) Does it sound reasonable to implement the approach from the 
OutsideIn paper, and than gradually transform it to look more like GHC?

-BenRI