Skip to content

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

Edited by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information