Simplifier turns value into ok-for-spec thunk

Consider this simplified variant of code in alexGetByte:

data Box a = Box !a

f :: Int -> Maybe (Box Int)
f loc = loc' `seq` Just (Box loc')
  where
    loc' = loc + 1

The code is written to ensure that there are no thunks in the result. Yet this is the simplified output:

f = \ (loc_awU :: Int) ->
      case loc_awU of { ghc-prim:GHC.Types.I# x_aBu ->
      GHC.Maybe.Just
        @(Box Int)
        (T24730.Box
           @Int (ghc-prim:GHC.Types.I# (ghc-prim:GHC.Prim.+# x_aBu 1#)))
      }

Clearly, Just (Box (I# (x +# 1#))) is not a value. It is merely ok-for-spec(-eval). CorePrep is pretty smart, though, and turns this into

T24730.f
  = \ (loc_sEG [Occ=Once1!] :: GHC.Types.Int) ->
      case loc_sEG of { GHC.Types.I# x_sEI [Occ=Once1] ->
      case GHC.Prim.+# x_sEI 1# of sat_sEJ [Occ=Once1] { __DEFAULT ->
      let {
        sat_sEK [Occ=Once1] :: GHC.Types.Int
        [LclId]
        sat_sEK = GHC.Types.I# sat_sEJ } in
      let {
        sat_sEL [Occ=Once1] :: T24730.Box GHC.Types.Int
        [LclId]
        sat_sEL = T24730.Box @GHC.Types.Int sat_sEK } in
      GHC.Maybe.Just @(T24730.Box GHC.Types.Int) sat_sEL
      }
      }

Note that the +# expression would normally run ashore in the RHS of sat, but since it is ok-for-spec we may float it out of the (lazy!) context, rendering sat_sEK and thus sat_sEL and the result of the function a value and not a thunk.

I encounted this effect while re-enacting a fix for a regression in $walexGetByte in !9874 (closed).

Note that the ok-for-spec expr Just (Box (I# (x +# 1#))) seems less informative than the "value decomposition" let x' = x +# 1# in Just (Box (I# x')). Would it make sense for the Simplifier to retain the latter form? I don't know, hence this ticket.