<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Dear Sebastian and GHC devs,<div><br></div><div>Regarding this bit from the function <b>addConCt</b> in the <b>GHC.HsToCore.Pmc.Solver</b> module,</div><div><br></div><div><div> Nothing -> do</div><div> let pos' = PACA alt tvs args : pos</div><div> let nabla_with bot' =</div><div> nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }</div><div> -- Do (2) in Note [Coverage checking Newtype matches]</div><div> case (alt, args) of</div><div> (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc -></div><div> case bot of</div><div><b> MaybeBot -> pure (nabla_with MaybeBot)</b></div><div><b> IsBot -> addBotCt (nabla_with MaybeBot) y</b></div><div><b> IsNotBot -> addNotBotCt (nabla_with MaybeBot) y</b></div><div> _ -> assert (isPmAltConMatchStrict alt )</div><div> pure (nabla_with IsNotBot) -- strict match ==> not ⊥</div></div><div><br></div><div>My understanding is that given some <b>x</b> which we know e.g. cannot be bottom, if we learn that <b>x ~ N y</b>, where <b>N</b> is a newtype (NT), we move our knowledge of <b>x</b> not being bottom to the underlying NT Id <b>y</b>, since forcing the newtype in a pattern is equivalent to forcing the underlying NT Id.</div><div><br></div><div>Additionally, we set <b>x</b>’s BottomInfo to <b>MaybeBot </b>—</div><div>However, I don’t understand why we must reset <b>x</b>’s BotInfo to MaybeBot — couldn’t we keep it as it is while setting <b>y</b>’s BotInfo to the same info?</div><div>An example where resetting this info on the newtype-match is important/necessary would be excellent.</div><div><br></div><div>FWIW, I built and tested the PMC of ghc devel2 with</div><div><br></div><div><div><b> MaybeBot -> pure (nabla_with MaybeBot)</b></div><div><b> IsBot -> addBotCt (nabla_with IsBot) y</b></div><div><b> IsNotBot -> addNotBotCt (nabla_with IsNotBot) y</b></div></div><div><b><br></b></div><div>And it worked without warnings or errors…</div><div><br></div><div>Thanks in advance!</div><div>Rodrigo</div></body></html>