GHC and type-family rewriting?
benjamin.redelings at gmail.com
Thu Dec 1 02:42:23 UTC 2022
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?
More information about the ghc-devs