[GHC] #15557: Reduce type families in equations' RHS when testing equation compatibility

[GHC]

#15557: Reduce type families in equations' RHS when testing equation compatibility
-------------------------------------+-------------------------------------
           Reporter:  mniip          |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #8423 #15546
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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:

 {{{#!hs
 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:
 {{{#!hs
 > :t undefined :: p a -> p (Test a a)
 p a -> p (Test a a)
 }}}

 Examining the IfaceAxBranches (cf #15546) we see:
 {{{#!hs
   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:
 {{{#!hs
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15557>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler