Hi, I first planned to post this to https://ghc.haskell.org/trac/ghc/ticket/1600 but it might be of wider interest, and is not only related to CPR. SPJ pointed me to this¹ paper by Graham Hutton (thanks for that). It lists three sufficient conditions for the w/w-wrapper to be semantically correct: (1) wrap ◦ unwrap = id (2) wrap ◦ unwrap ◦ body = body (3) fix (wrap ◦ unwrap ◦ body) = fix body The first one is often not true when we do w/w in GHC. The third one seems to be out of reach: Arguing about a recursive function in this way smells like solving the halting problem. So it seems that we should be aiming for (2) wrap ◦ unwrap ◦ body = body With this in mind, setting the CPR info of recursive things to ⊤, i.e. “we don’t know anything” _when analyzing their RHS_ should do the right thing: If we assume nothing about the argument of `body`, the result will hold for all, which precisely is `wrap ◦ unwrap ◦ body = body`. And this should be the case not only for CPR, but for anything that does a w/w-transformation, i.e. Demand analysis as well. But what about strictness analysis? Clearly, for f :: Int -> Int -> Int f n m = if n == 0 then m else f (n-1) m we want to know (as we do in 7.6. and in HEAD) that it is strict in m... Interesting fact here: GHC-7.6 will find this worker signature wf :: Int# -> Int -> Int (which is compatible with condition (2)), but GHC HEAD will do wf :: Int# -> Int# -> Int# where equation (2) is no longer holds. In this case (3) happens to hold (at least wrt to a semantics that does not distinguish non-termination of other kinds of ⊥). Conclusion: The correctness of GHC’s w/w-transformation is currently not formally well supported, and it only works due to delicate and non-obvious² interaction between the analysis and the transformation (see comment 20 of #1600 for an example how easily it breaks). But if we systematically ensure the correctness, by always guaranteeing (2), we are losing existing chances for optimization. Some more less consistent thoughts: There seems to be a conceptual difference between the CPR w/w-transformation and the others: Unboxing arguments pulls work out of the worker to be done _before_ it is being called. Clearly, this will never make the recursive call to the work diverge, unless it would diverge anyways. And if the work pulled out diverges (e.g. if m = undefined in the example above), then either the worker would have diverged (but that is fine) or, assuming the analysis is correct, would have performed the work. So for these transformations it is ok to use the full information in the recursive case. But the CPR transformation is different: The w/w transformation forces the evaluation of the result of the recursive call and in that sense moves work into it. And if this again triggers work to be moved into the next recursive calls, we can cause divergence. So by this handwavy argument, we are fine for unboxing arguments and strictness analysis, but for CPR we really should forget what we know about the f when analyzing f’s body. Thanks for your attention, Joachim ¹ http://www.cs.nott.ac.uk/~gmh/wrapper.pdf ² to me at least – I might be missing something -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org