<html><head><style id="css_styles" type="text/css"><!--blockquote.cite { margin-left: 5px; margin-right: 0px; padding-left: 10px; padding-right:0px; border-left: 1px solid #cccccc }
blockquote.cite2 {margin-left: 5px; margin-right: 0px; padding-left: 10px; padding-right:0px; border-left: 1px solid #cccccc; margin-top: 3px; padding-top: 0px; }
a img { border: 0px; }
li[style='text-align: center;'], li[style='text-align: right;'] { list-style-position: inside;}
body { font-family: Segoe UI; font-size: 12pt; }--></style><style><!--#x73ced7da7ffe4c84b3806dbd9b7988d9 a{
color:#00E;
color:#551A8B;
}
:visited{
color:#551A8B;
}
#x73ced7da7ffe4c84b3806dbd9b7988d9{
background-color:#FFF;
color:#000;
margin-left:0px;
margin-right:8px;
}
#x73ced7da7ffe4c84b3806dbd9b7988d9 blockquote{
display:none;
}--></style></head><body><div><div id="x73ced7da7ffe4c84b3806dbd9b7988d9"><div><div>Hi Rodrigo,</div><div><br /></div><div>Happy to see that you resumed your work on the pattern-match checker.</div><div>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. </div><div>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`.</div><div>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.</div><div><br /></div><div>So by all means, open an MR for your change. Good work!</div><div><br /></div><div>Sebastian</div></div></div></div>
<div><br /></div>
<div>------ Originalnachricht ------</div>
<div>Von: "Rodrigo Mesquita" <<a href="mailto:rodrigo.m.mesquita@gmail.com">rodrigo.m.mesquita@gmail.com</a>></div>
<div>An: "Sebastian Graf" <<a href="mailto:sebastian.graf@kit.edu">sebastian.graf@kit.edu</a>></div>
<div>Cc: "GHC developers" <<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>></div>
<div>Gesendet: 27.10.2023 17:34:29</div>
<div>Betreff: PMC: addConCt and newtypes bottom info</div><div><br /></div>
<div id="x68b6bd028cde4a0" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><blockquote cite="FAD4FA8E-59CA-4AB4-8E68-1F2A9CFEB597@gmail.com" type="cite" class="cite2">
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></blockquote></div>
</body></html>