Opened 13 months ago

Last modified 13 months ago

## #15557 new feature request

# Reduce type families in equations' RHS when testing equation compatibility

Reported by: | mniip | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.6.1 |

Component: | Compiler (Type checker) | Version: | 8.4.3 |

Keywords: | TypeFamilies | Cc: | simonpj, goldfire |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | #8423 #15546 | Differential Rev(s): | |

Wiki Page: |

### Description

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) 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:10, 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:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.

### Change History (7)

### comment:1 Changed 13 months ago by

### comment:2 Changed 13 months ago by

Yes, of course, being unable to unify `a ~ Test a a`

is a more "severe" way to put it, but the fact that it doesn't reduce in `:t`

is a more quick test.

### comment:3 Changed 13 months ago by

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.

### comment:4 Changed 13 months ago by

Correction: an `apart`

constraint might sometimes not get discharged if the same tyvar occurs multiple times, e.g:

type family Eq a b where Eq a a = True Eq a b = False

TF a a ~ True apart(<c, c>, <a, b>) => TF a b ~ False

### comment:5 Changed 13 months ago by

I'm not sure what you're suggesting here. comment:3 and comment:4 seem (I didn't fully dig through them) to be a restatement of some of the arguments in #8423. Is that correct?

The algorithm in comment:10:ticket:8423 is long lost on some probably-obliterated git branch. Do you think it would address your use case?

Maybe what you're suggesting is that (for closed type families at least) we can reduce fully-known (i.e. not in the same recursive group) type families on the RHS. That may indeed be true. For open type families, though, we're stuck, because they're never fully known. And if there is a way for these type families not to terminate, I'm lost as to what the answer is.

My bottom line: I'm sure there is room for improvement in this direction, but the path forward is narrow and bordered by heffalump traps. The CTFwOE team got mired in many of them. I'd want a solid proof before implementing any new ideas in this area.

### comment:6 Changed 13 months ago by

Nevertheless, Richard, do you agree with comment:1. That is, we currently have an outright bug? And if so, can you see how to fix it?

PS: ah, looking a bit harder, I see that maybe it's a feature request after all: when two LHSs unify, you want a stronger notion of what "the substituted RHSs are equal" means (something more like "equal after normalisation". And maybe that is hard -- perhaps that is what #8423 is about?

### comment:7 Changed 13 months ago by

**Note:**See TracTickets for help on using tickets.

I think you mean more than

`:t`

reports the wrong result. ConsiderThis indeed fails with

I'd need to look back carefully at the paper to see what should happen, but no time for that today. Richard may opine on his return.