Reduce type families in equations' RHS when testing equation compatibility

The reference I found for closed type families with compatible equations is: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/popl137-eisenberg.pdf

There in Definition 8 in section 3.4 it states:

Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.

Examine the following families:

type family If (a :: Bool) (b :: k) (c :: k) :: k where
    If False a b = b
    If True a b = a

type family Eql (a :: k) (b :: k) :: Bool where
    Eql a a = True
    Eql _ _ = False

type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
    Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
    Test a a = a
    Test Nothing _ = Nothing
    Test _ Nothing = Nothing

Applying the check to the equations 1 and 2 of Test we get:

unify(<Just x, Just y>, <a, a>) = Ω = [a -> Just x, y -> x]

Ω(a) = Just x = If (Eql x x) (Just x) Nothing = Ω(If (Eql x y) (Just x) Nothing)

Therefore the equations must be compatible, and when tidying forall a. p a -> p (Test a a) the application should reduce to forall a. p a -> p a

That doesn't happen:

> :t undefined :: p a -> p (Test a a)
p a -> p (Test a a)

Examining the IfaceAxBranches (cf #15546 (closed)) we see:

  axiom D:R:Test::
      Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
      Test k a a = a
      (incompatible indices: [0])
      Test k 'Nothing _ = 'Nothing
      Test k _ 'Nothing = 'Nothing

GHC did not consider the two equations compatible.

Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:80951, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).

The family here doesn't require any of that special consideration because Eql x x reduces right away without any compatibility checks, and If is essentially open (indeed making If open doesn't help anything).

This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?

P.S: An interesting workaround is adding an If t c c = c equation (compatible), and then writing Test as:

type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
    Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
    Test a a = If (Eql a a) a Nothing
    Test Nothing a = If (Eql Nothing a) Nothing Nothing
    Test a Nothing = If (Eql a Nothing) Nothing Nothing

This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.

P.P.S: In ticket:15546#comment:158797 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.

Trac metadata

Trac field	Value
Version	8.4.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire, simonpj
Operating system
Architecture