[GHC] #15557: Reduce type families in equations' RHS when testing equation compatibility

[GHC]

#15557: Reduce type families in equations' RHS when testing equation compatibility
-------------------------------------+-------------------------------------
        Reporter:  mniip             |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8423 #15546      |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by mniip):

 After giving it a little thought:

 Equation compatibility check can be regarded as a quantified implicational
 constraint:

 {{{
 [p] forall ps. TF lhs_p = rhs_p
 [q] forall qs. TF lhs_q = rhs_q
 }}}

 {{{
 compat(TF, p, q) = forall ps qs. (lhs_p ~ lhs_q) => (rhs_p ~ rhs_q)
 }}}

 Since `lhs_k` in Haskell are always a simple tycon/tyvar superposition,
 one can, as the CTFwOE paper implies, just run unification on `lhs_p ~
 lhs_q`. If the unification fails the implication holds vacuously,
 otherwise we have a substitution to apply to `rhs_p`/`rhs_q`. In such case
 we are left with:

 {{{
 compat(TF, p, q) = forall as. Omega(rhs_p) ~ Omega(rhs_q)
 }}}

 This constraint is still quantified but at least not implicational.

 Now we can kind-of express compatibility checking in the language of
 constraint solving: we have implicational axioms:

 {{{
 (apart(lhs_1, lhs_i), ..., apart(lhs_i-1, lhs_i)) => TF lhs_i ~ rhs_i
 (compat(TF, 1, i), ..., compat(TF, i-1, i)) => TF lhs_i ~ rhs_i
 }}}

 ...But also every other combination of `apart` and `compat` constraints,
 provided either is given for each j in [0 .. i-1]. Again `lhs_k` are
 simple enough that `apart` constraints can be easily immediately
 discharged to either trivially false or trivially true constraints. We are
 then left with, really, one implication constraint for each equation:

 {{{
 (compat(TF, c_1, i), ..., compat(TF, c_k, i)) => TF lhs_i ~ rhs_i
 }}}

 Where c_1,...,c_k are exactly the indices of equations that come before
 ith but whose lhs are not apart from ith equation's.

 This is where @goldfire's comment comes in: if we are left with a system
 of constraint implications that has multiple solutions, e.g:

 {{{
 compat(A, 0, 1) => compat(B, 0, 1)
 compat(B, 0, 1) => compat(A, 0, 1)
 }}}

 Here the two either simultaneously hold or simultaneously don't hold. Here
 it is actually type-safe to pick the most truthy solution: the greatest
 fixed point rather than the least.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15557#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler