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 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 13 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 13 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 13 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 13 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 13 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 13 months ago by simonpj (previous) (diff)

comment:7 Changed 13 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.