summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSebastian Graf <sebastian.graf@kit.edu>2021-02-09 18:54:47 +0100
committerMarge Bot <ben+marge-bot@smart-cactus.org>2021-02-18 13:45:41 -0500
commit2adfb404111c220ef4df0206d9cda20c2fe5db46 (patch)
treea48cdb916f980d5f083965c0114084584b992835
parentdbf8f6fe12db67b96412015a01646ce800f9988a (diff)
downloadhaskell-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.hs24
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.
************************************************************************
* *