#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