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
