case lazy (Con x y z) -> Con x' y' z' -> ... is not optimised

If I have

module Magic where

import GHC.Magic (lazy)

data Foo = Foo !Int !Int String

mkFoo a b c = lazy (Foo a b c)

function !a !b c = case mkFoo a b c of
    Foo a' b' _c' -> a' + b'

(such code happens when using assert/assertError which happy path is lazy), then

ghc-9.8.1 -O -c Magic.hs -fforce-recomp -ddump-simpl -dsuppress-all

outputs

function
  = \ a_awE b_awF c_awG ->
      case a_awE of { I# ipv_sB9 ->
      case b_awF of { I# ipv1_sBb ->
      case lazy (Foo ipv_sB9 ipv1_sBb c_awG) of
      { Foo bx_dB7 bx1_dB8 _c'_awJ ->
      I# (+# bx_dB7 bx1_dB8)
      }
      }
      }

and I honestly don't understand why case-of-known-constructor doesn't happen with lazy in between.

I'd expect to see

function
  = \ a_awF b_awG _ ->
      case a_awF of { I# ipv_sBc ->
      case b_awG of { I# ipv1_sBe -> I# (+# ipv_sBc ipv1_sBe) }
      }