PMC: addConCt and newtypes bottom info

[Sebastian Graf]

Hi Rodrigo,

Happy to see that you resumed your work on the pattern-match checker.
I think you are right; we could reasonably just go with your code, not 
least because it is less confusing to retain as much info about `x` as 
possible.
I don't think it makes a difference, because whenever we add a 
constraint `x ≁ ⊥` afterwards, we call `addNotBotCt` which will 
interpret this constraint as `y ≁ ⊥` via `lookupVarInfoNT`, and we have 
accurate BotInfo for `y`.
Basically whenever we have seen `x ~ T y`, `T` Newtype, we will never 
look at `BotInfo` of `x` again. I thought it might become relevant in 
`generateInhabitingPatterns` for warning messages, but there we eagerly 
instantiate through NTs anyway.

So by all means, open an MR for your change. Good work!

Sebastian

------ Originalnachricht ------
Von: "Rodrigo Mesquita" <rodrigo.m.mesquita at gmail.com>
An: "Sebastian Graf" <sebastian.graf at kit.edu>
Cc: "GHC developers" <ghc-devs at haskell.org>
Gesendet: 27.10.2023 17:34:29
Betreff: PMC: addConCt and newtypes bottom info

>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/44e05cbc/attachment.html>