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 |