Opened 17 months ago

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

Reported by: Owned by: mniip normal 8.6.1 Compiler (Type checker) 8.4.3 TypeFamilies simonpj, goldfire Unknown/Multiple Unknown/Multiple GHC rejects valid program #8423 #15546

### 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: )
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.

### comment:1 Changed 17 months ago by simonpj

That doesn't happen:

I think you mean more than `:t` reports the wrong result. Consider

```f :: Proxy b -> Proxy b -> Int
f = error "urk"

g :: Proxy a -> Proxy (Test a a) -> Int
g x y = f x y
```

This indeed fails with

```T15557.hs:25:13: error:
• Couldn't match type ‘a’ with ‘Test a a’
```

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.

### comment:2 Changed 17 months ago by mniip

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 17 months ago 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.

### comment:4 Changed 17 months ago by mniip

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 17 months ago by goldfire

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 17 months ago by simonpj

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?

Last edited 17 months ago by simonpj (previous) (diff)

### comment:7 Changed 17 months ago by goldfire

I agree with the PS in comment:6. I see this as a pure feature request, not a bug. The behavior in comment:1 is consistent with the design of closed type families in the paper and the manual.

Note: See TracTickets for help on using tickets.