Skip to content

Precise exceptions: `stToIO` and `ioToST` can circumvent analysis in Note [Which scrutinees may throw precise exceptions]

Summary

The analysis described in Note [Which scrutinees may throw precise exceptions] is oblivious wrt. computations in forall s. ... State# s ..., even though it triggers for its instance State# RealWorld#.

This means we can circumvent the analysis by defining most of the code in ST s r, parameterising over computations that are actually in IO, and then run the supposedly pure ST s r computation with those impure IO actions supplied as parameters.

Steps to reproduce:

Compile and run with -O:

import GHC.IO
import GHC.ST

foo :: Int -> ST s r -> ST s Int
foo a act = act >> (pure $! a+1)
{-# NOINLINE foo #-}

main = stToIO $ foo (error "Not OK") (ioToST (throwIO (mkUserError "OK")))
test: Not OK

Expected behavior

test: user error (OK)

Discussion

It is questionable whether this is actually desirable. Potentially, the performance of every morally pure ST s a computation such as foo might be affected for the worse: We may not ever use call-by-value for foo, unless it forces a before calling act.

I'm inclined to simply ignore this issue.

(CC) @clyring and @simonpj with whom I discussed this issue today.

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