diff options
author | Sebastian Graf <sebastian.graf@kit.edu> | 2021-02-09 18:54:47 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-02-18 13:45:41 -0500 |
commit | 2adfb404111c220ef4df0206d9cda20c2fe5db46 (patch) | |
tree | a48cdb916f980d5f083965c0114084584b992835 | |
parent | dbf8f6fe12db67b96412015a01646ce800f9988a (diff) | |
download | haskell-2adfb404111c220ef4df0206d9cda20c2fe5db46.tar.gz |
Document how bottom CPR and dead-ending Divergence are related [skip ci]
In a new `Note [Bottom CPR iff Dead-Ending Divergence]`.
Fixes #18086.
-rw-r--r-- | compiler/GHC/Types/Demand.hs | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs index 0a23e10224..8e2fec9ff6 100644 --- a/compiler/GHC/Types/Demand.hs +++ b/compiler/GHC/Types/Demand.hs @@ -1046,6 +1046,30 @@ not accounted for in the type, by consulting 'defaultArgDmd': it's perfectly possible to enter the additional lambda and evaluate it in unforeseen ways (so, not absent). +Note [Bottom CPR iff Dead-Ending Divergence] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Both CPR analysis and Demand analysis handle recursive functions by doing +fixed-point iteration. To find the *least* (e.g., most informative) fixed-point, +iteration starts with the bottom element of the semantic domain. Diverging +functions generally have the bottom element as their least fixed-point. + +One might think that CPR analysis and Demand analysis then agree in when a +function gets a bottom denotation. E.g., whenever it has 'botCpr', it should +also have 'botDiv'. But that is not the case, because strictness analysis has to +be careful around precise exceptions, see Note [Precise vs imprecise exceptions]. + +So Demand analysis gives some diverging functions 'exnDiv' (which is *not* the +bottom element) when the CPR signature says 'botCpr', and that's OK. Here's an +example (from #18086) where that is the case: + +ioTest :: IO () +ioTest = do + putStrLn "hi" + undefined + +However, one can loosely say that we give a function 'botCpr' whenever its +'Divergence' is 'exnDiv' or 'botDiv', i.e., dead-ending. But that's just +a consequence of fixed-point iteration, it's not important that they agree. ************************************************************************ * * |