[GHC] #8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!)

[GHC]

#8423: contraint solver doesn't  reduce reducible closed type family expressions
(even with undecidable instances!)
--------------------------------------------+------------------------------
        Reporter:  carter                   |            Owner:
            Type:  feature request          |           Status:  new
        Priority:  normal                   |        Milestone:  7.10.1
       Component:  Compiler (Type checker)  |          Version:  7.7
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:  #4259
--------------------------------------------+------------------------------
Changes (by goldfire):

 * related:   => #4259


Comment:

 Yes, closed type families are too weak. But for a good reason.

 Here is the test case boiled down:

 {{{
 data PNat = S !PNat  | Z
 type family PSum (a :: PNat) (b:: PNat) :: PNat  where
   PSum 'Z b = b      -- 1
   PSum a 'Z = a      -- 2
   PSum a ('S b) = 'S (PSum a b)    -- 3
   PSum ('S a) b = 'S (PSum a  b)   -- 4
 }}}

 At some point, the type checker wants to know whether `(PSum (S r2) b) ~
 (PSum r2 (S b))`. To do this, both sides of the `~` need to reduce one
 step. But neither can reduce in practice. Why? An equation in a closed
 type family can fire (that is, be used in a reduction) only when GHC can
 be absolutely positive of one of two things:

 1. No previous equation can fire, or
 2. Any previous equation that can fire will reduce, in one step, to the
 same thing.

 (Technically, (2) subsumes (1), but it's easier to think about the cases
 separately.)

 Let's consider reducing `PSum r2 (S b)`. Clearly, neither of the first two
 equations are applicable. Equally clearly, the third equation is quite
 tempting. Now, we check for these conditions. We quickly see that equation
 (1) might fire, if `r2` ends up becoming `Z`. So, now we need to satisfy
 (2). If equation (1) can fire, then we really are in the case `PSum Z (S
 b)`. If equation (1) fires, we get `S b`. If equation (3) fires, we get `S
 (PSum Z b)`. These are '''not''' the same. So, GHC remains on the fence
 about the whole affair and prudently refuses to take action.

 An obvious question at this point is: Why the one-step restriction? The
 answer: anything else is not obviously well-founded. (Note: I did not say
 "obviously not well-founded", which is quite a different claim!) The
 general case is to check that the reducts (that is, the right-hand sides)
 are ''confluent''. (The current check looks to see if they are
 ''coincident''.) But, to check confluence means reasoning about type
 family reductions... including perhaps the one we are defining... whose
 reduction behavior would depend on the confluence of the equations' right-
 hand sides. Oops; we've just fallen into the rabbit hole.

 There might be a way out of this morass, but I go cross-eyed when I think
 about it for too long. Not that it isn't worth it -- I think that allowing
 code like Carter's to be accepted would be a great boon to GHC! I just
 don't know a way of thinking about this that will solve the problem.

 For more reading on the subject, check out #4259, which is all about this
 problem. It's possible that closed type families address some of the
 examples there, but the core problem discussed in that bug is the same as
 the one here. However, because that bug is about open families and this
 one is about closed, I will leave this one open. It's (barely) conceivable
 that they have different solutions.

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