<div dir="ltr"><div dir="ltr">Following up on this, I've hacked in the changes locally, by setting `XVar GhcTc = [Name, Type]`, and filling it only for `HsVar`s that used to be `HsUnboundVar`s. The result is remarkable, as it allows for interactive proof search. I've got a proof of concept here: <a href="https://asciinema.org/a/FZjEIFzDoHBv741QDHfsU5cn8">https://asciinema.org/a/FZjEIFzDoHBv741QDHfsU5cn8</a></div><div dir="ltr"><br></div><div>I think the possibilities here warrant making the same change in HEAD. I'd be happy to send an MR if it seems likely to be merged.</div><div><br></div><div>Sandy</div><div dir="ltr"><br></div><div dir="ltr"><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Aug 17, 2019 at 6:27 PM Sandy Maguire <<a href="mailto:sandy@sandymaguire.me">sandy@sandymaguire.me</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div>I'm trying to get my hands on the relevant local binds (as reported by ghc in the presence of a type hole) for editor tooling support. Tracing the code suggests that these things come from the `TcLclEnv`, but afaict, all remnants of `TcLclEnv` are thrown away by the time we get a `TypecheckedModule`.</div><div><br></div><div>Am I mistaken in this? If not, how receptive would y'all be to a patch that puts the `TcLclEnv`, or something similar inside `XUnboundVar GhcTc`. This way editors would have an easy means of getting their hand on whatever is in scope at the site of a hole, without resorting to parsing error messages.</div><div><br></div><div>Cheers,</div><div>Sandy<br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail-m_92690562024616448gmail_signature"><div dir="ltr"><div>I'm currently traveling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! <a href="https://isovector.github.io/erdos/" target="_blank">https://isovector.github.io/erdos/</a><br></div></div></div></div></div>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div>I'm currently traveling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! <a href="https://isovector.github.io/erdos/" target="_blank">https://isovector.github.io/erdos/</a><br></div></div></div>