Re: 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" 
An: "Sebastian Graf" 
Cc: "GHC developers" 
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___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs