## 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 |