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