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
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"
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
participants (2)
-
Rodrigo Mesquita -
Sebastian Graf