[GHC] #8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!)
#8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!) -------------------------------------------+------------------------------- Reporter: carter | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 7.7 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: -------------------------------------------+------------------------------- attached is an example where the type checker isn't "computing" in the closed type families, or at least doing a one step reduction. this makes sense, given that type families only compute when instantiated... But if we could partially evaluate closed type families (or at least do a one step reduction), the attached example code would type check! interestingly, depending on what order the cases for the PSum are written, the type error changes! I guess I want an "eager matching" closed type family, that when partially instantiated will patch on the first pattern it satisfies, to complement ordered type families. attached is a toy example where I otherwise need an unsafeCoerce to make things type check -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!) --------------------------------------------+------------------------------ Reporter: carter | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.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: --------------------------------------------+------------------------------ Comment (by carter): so maybe this is a "feature request" idea rather than a bug, but i'd like more folks to chime in please :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: --------------------------------------------+------------------------------ Changes (by carter): * type: bug => feature request * milestone: 7.8.1 => 7.10.1 Comment: Though I imagine theres some subtleties to adding such machinery, but it might be a great way to allow more "proofs by computation" to work out in Haskell -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 --------------------------------------------+------------------------------ Comment (by carter): excellent points that i probably agree with (and i'll have to dig into that other ticket as time permits) Hrm, another way of looking at it is that i'd be ok with having to come up with sort of induction principles or the like that let me give the type checker the proofs! Currently we dont have a decent story that plays well with equality constraints. so I either need to "lie about the types" and do something like {{{ reverseShape :: Shape r -> Shape r reverseShape Nil = Nil reverseShape shs@(anIx :* rest) = go shs Nil where --- too weakly typed go :: Shape a -> Shape b -> Shape r -- want r= PSum a b go Nil res = unsafeCoerce $ res -- 0 + b = b ==> b=r go (ix :* more ) res = go more (ix :* res) --- 1+a + b = r }}} (which has a cast in the base case, but is ok othewise) OR try to have some sort of "proof" mapping, which honestly dones't work, and to even "write" the terms required {{{ {-# LANGUAGE AllowAmbiguousTypes #-} }}} that attempt looked like the following {{{ assocSumSucc :: Shape (PSum ('S r2) b) -> Shape ( PSum r2 ('S b)) assocSumSucc = unsafeCoerce assocSumSuccBad :: Shape (PSum a b) -> Shape ( PSum c d) assocSumSuccBad = unsafeCoerce }}} this doesn't quite work, because neither interacts with the equality constraint solving! So the only sane thing of that sort is {{{ shapeCoerce :: Shape a -> Shape b shapeCoerce = unsafeCoerce }}} which is honestly pretty bad! (and apply this in the recursive case) these as all (unlike the other solution inline above) pretty bad, because they break tail calls. I guess what i want is a way have having "proof principles" or something that i could build, which would interact well with the types. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 --------------------------------------------+------------------------------ Comment (by carter): relatedly: Ranjit Jhala took the motiviating code and demo'd checking it with liquid haskell! Which is pretty darn awesome http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1381284690.hs -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 --------------------------------------------+------------------------------ Comment (by carter): honestly i just want a way to check things, my ticket here is just noting limits that happen with type families. I'm open to anything that has a sane usability story and a sane engineering story (on the ghc and users sides both). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 --------------------------------------------+------------------------------ Comment (by goldfire): If you just want a way to check things, please see [https://gist.github.com/goldfirere/6902431 here]. The key step is that you do in fact have to write proofs! These proofs may, sadly, have runtime significance. But, from the optimization results in the "Deferred type errors" [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/icfp12.pdf paper] lead me to wonder if these runtime traces are optimized away. (I haven't checked -- doing so is beyond the scope of my morning Haskell stretches.) I did check, though, that the inliner will remove calls to `gcoerce` and make `go` properly tail-recursive (ignoring the type-cast, which I know is removed at runtime). Thanks for posting this! It's made me realize that `gcoerce` from that example should probably be in the Data.Type.Equality module anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 --------------------------------------------+------------------------------ Comment (by carter): thanks! this is great! Would I want to compare the core? (or just use criterion to benchmark?). I'll add that to my infinite todo list. This example seems to work only in ghc 7.8, how would i adapt those ideas to work on 7.6? (can I even?) that said, having more examples like this about how to prove things in haskell is probably a good idea! Also, figuring out how to erase such proofs as much as possible also would likely be worth while. I'm happy to help contribute a few braincells to chewing on that post 7.8 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 --------------------------------------------+------------------------------ Comment (by goldfire): This should work just fine in 7.6. Just change the closed type family `(+)` to be an open one. Everything else should just work. I've update [https://gist.github.com/goldfirere/6902431#file-shape-7-6-hs the gist] with a 7.6-compatible version. (I also had to inline a few definitions that aren't available in the 7.6 libraries.) Examining the core won't work, because even core needs the proofs to type- check! You might be able to examine something after core, but GHC's behavior after it's done with core is black magic to me. You might have to benchmark it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 --------------------------------------------+------------------------------ Comment (by goldfire): After being prodded via email to consider this issue further, I've made a tiny bit of progress, but nowhere near an actual solution. It turns out that the closed type family case and the open type family case can indeed be considered separately. Why? Because the compatibility check can usefully be turned off in the closed type family case, but not in the open one. Turning off the compatibility check for closed families reduces the number of reductions possible, but doesn't threaten soundness. On the other hand, turning off the compatibility check for unordered, open families destroys soundness. So, I thought about this: during the compatibility check, I normalized both substituted RHSs, but, during the normalization, I ignored compatibility. This seems like a nice, conservative check, but less conservative than the current one, requiring coincidence. It turned out that implementing the check above was non-trivial (it required delicate ordering among family instances), so I did the following (even better) thing instead (this is available in the `wip/recurs-compat` branch): - The existing compatibility check was left unchanged. - During type family simplification, an extra check was added, in parallel with the apartness check. (This follows more closely what is written up in [http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf the paper].) Say the current, matching equation is `e` and the previous one under consideration is `d`. Suppose the target is `t`. - We unify `d` with `t`, possibly producing unifying substitution `ds`. (If unification fails, the new check fails, and no reduction happens. But, note that if `d` and `t` are apart, then the apartness check succeeds, allowing reduction.) - Let `es` be the substitution (sure to exist) that witnesses that `e` matches `t`. - Now, we check if `normalize(ds(d_rhs)) = normalize(ds(es(e_rhs)))`. If this check succeeds, we allow reduction by equation `e`. - The `normalize` function here is special: if it is reducing a closed type family and needs to do a compatibility check, that check ''does not normalize''. Without this restriction, we would often loop, as demonstrated below. There are a few natural questions at this point: - '''Is this type safe?''' I haven't proved anything. But, I believe that it is type safe as long as all type families terminate. Why? Because the type safety proof (appearing in the paper) doesn't seem to be disturbed by this change. That proof requires only ''local'' confluence, meaning that it can take an arbitrary number of steps to recombine two terms after they have diverged. However, I believe that this is '''not''' type-safe in the presence of non-terminating type families. Why? Because the proof in the non-terminating case requires a ''local diamond'' property, which requires single-step recombining after divergence. The normalization step explicitly throws that out. I don't know of a way to repair the proof, so I'm led to think that the property is indeed broken. I have no counter- example, though. - '''Does it work in practice?''' A bit. Take the `PSum` family in comment:3. In GHC 7.8, the third equation won't fire because it conflicts with the second. With the extra check as described here, the third equation can indeed fire. But, the fourth can't, because the compatibility check against the third requires normalization internally to work. I don't see an easy solution to that problem. - '''What about axioms in Core?''' My work didn't touch axioms. So, `-dcore-lint` would fail in my branch if the new checks were used. A real solution here would require changes to Core, essentially to record exactly how two equations are compatible. Given that the proof of compatibility (with normalization) might be arbitrarily large, it would seem to require some new form that is an explicit witness of compatibility. Of course, we could just bake the normalization step into the Core type-checking algorithm, but normalization is potentially non-terminating, so doing so breaks the tenet of "type-checking Core is simple and decidable". - '''Where to go from here?''' I believe that the core problem is that we're currently finding some sort of least fixed point of compatibility, where we really want the greatest fixed point. That is, if we assume that the third and fourth equations of `PSum` are compatible, then we can prove they're compatible. This recursive proof would be productive (that is, there would be a new `'S` constructor), so I think the idea isn't entirely silly. I haven't worked out any details, though. - '''What's the looping example?''' Check this out: {{{ type family F a where F [a] = F a F b = b }}} This is a simple, terminating type family. Yet, if we try to simplify `F c` (which should be stuck), a fully recursive compatibility check would loop, as the check would, in turn, need to simplify `F a`, which is isomorphic to what we started with. Given the complications here (especially the thought of how to update Core), I'm tabling this for now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 jstolarek): * cc: jan.stolarek@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: 8.0.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4259 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (removed) * cc: jstolarek (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8423: Less conservative compatibility check for closed type families -------------------------------------+------------------------------------- Reporter: carter | Owner: Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4259 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * milestone: 8.0.1 => ⊥ Comment: New title and milestone to reflect the realities here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC