PMC: addConCt and newtypes bottom info

[Rodrigo Mesquita]

Dear Sebastian and GHC devs,

Regarding this bit from the function addConCt in the GHC.HsToCore.Pmc.Solver module,

    Nothing -> do
      let pos' = PACA alt tvs args : pos
      let nabla_with bot' =
            nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
      -- Do (2) in Note [Coverage checking Newtype matches]
      case (alt, args) of
        (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
          case bot of
            MaybeBot -> pure (nabla_with MaybeBot)
            IsBot    -> addBotCt (nabla_with MaybeBot) y
            IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
        _ -> assert (isPmAltConMatchStrict alt )
             pure (nabla_with IsNotBot) -- strict match ==> not ⊥

My understanding is that given some x which we know e.g. cannot be bottom, if we learn that x ~ N y, where N is a newtype (NT), we move our knowledge of x not being bottom to the underlying NT Id y, since forcing the newtype in a pattern is equivalent to forcing the underlying NT Id.

Additionally, we set x’s BottomInfo to MaybeBot —
However, I don’t understand why we must reset x’s BotInfo to MaybeBot — couldn’t we keep it as it is while setting y’s BotInfo to the same info?
An example where resetting this info on the newtype-match is important/necessary would be excellent.

FWIW, I built and tested the PMC of ghc devel2 with

            MaybeBot -> pure (nabla_with MaybeBot)
            IsBot    -> addBotCt (nabla_with IsBot) y
            IsNotBot -> addNotBotCt (nabla_with IsNotBot) y

And it worked without warnings or errors…

Thanks in advance!
Rodrigo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20231027/a8a72b15/attachment.html>