Unsound optimization with -O in ghc 8.4 and 8.6 when using unsafeCoerce (produced by Agda)
Summary
Unsound optimization of unsafeCoerce
with -O
under GHC 8.4 and 8.6.
The following code was shrunk from code generated by the GHC backend of Agda. Agda in essence targets the untyped lambda calculus, thus, uses unsafeCoerce
excessively. This was unproblematic until GHC 8.2 and seems to be fine again from GHC 8.8.
Steps to reproduce
{-# LANGUAGE NoImplicitPrelude #-}
module Main where
import Prelude (IO, ($), (.), (>>=), putStrLn)
import System.Exit (exitFailure)
import Unsafe.Coerce (unsafeCoerce)
sequ :: IO () -> IO a -> IO a
sequ c c' = c >>= \ _ -> c'
main :: IO ()
main =
unsafeCoerce sequ (putStrLn "Hello,") $
unsafeCoerce sequ (putStrLn "world!") $
exitFailure
With 8.4.x or 8.6.x run
ghc -O Main.hs
./Main
The output is
Hello,
and exitcode is 0.
Expected behavior
Output [UPDATE: this output is produced when compiling with 8.8, 8.2, 8.0]
Hello,
world!
and exitcode 1.
Environment
- GHC version used: 8.4.4 and 8.6.4
Optional:
- Operating System: Mac Mojave