Seemingly inconsistent divergence results from CPR and demand analyses
While looking into #18086 (closed) I noticed that some expressions get assigned bottoming CPR signatures yet non-bottoming strictness signatures. For instance, consider this program:
ioTest :: String -> IO a
ioTest x = do
putStrLn "hello"
undefined
Clearly this will diverge when given a single value argument.
However, when compiled with -O
GHC produces the following simplified Core:
$wioTest [InlPrag=NOUSERINLINE[2]]
:: forall {a}. State# RealWorld -> (# State# RealWorld, a #)
[GblId, Arity=1, Str=<L,U>, Cpr=b, Unf=OtherCon []]
$wioTest
= \ (@a_s1Ac) (w_s1Ch [Occ=Once] :: State# RealWorld) ->
case ((hPutStr' stdout lvl14_r1B9 True) `cast` <Co:2>) w_s1Ch of
{ (# _ [Occ=Dead], _ [Occ=Dead] #) ->
case lvl12_r1B7 of { }
}
lvl12_r1B7 :: forall {a}. IO a
[GblId, Str=b, Cpr=b]
lvl12_r1B7
= \ (@a_a1km) ->
case unpackCString# lvl11_r1B6 of sat_s1Cg [Occ=Once]
{ __DEFAULT ->
error @'LiftedRep @(IO a_a1km) (lvl10_r1B5 `cast` <Co:4>) sat_s1Cg
}
Note the strictness and CPR signatures of $wioTest
: CPR has correctly realized that the function bottoms. The demand analyser on the other hand came to no such conclusion; I would have rather expected a signature of <L,U>b
.
What is going on here? Should there be some sort of invariant requiring agreement between these two passes? Is there a distinction between their respective notions of "bottoming" that I'm not seeing?
CC @sgraf812