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:
Just y>, <
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: ) 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
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.
|Component||Compiler (Type checker)|