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