unisonweb / unison

A friendly programming language from the future
https://unison-lang.org
Other
5.81k stars 271 forks source link

pretty-printer can insert use clauses that don't avoid local variable capture #5336

Open mitchellwrosen opened 2 months ago

mitchellwrosen commented 2 months ago

and even if it did, we don't have a syntax for "not a local variable" (e.g. if a reference is named foo.bar.baz, so we can call it one of baz, bar.baz, or foo.bar.baz, but all might be bound)

mitchellwrosen commented 2 months ago

hm... I'll have to make this issue more precise tomorrow; it seems our pretty-printer does (try to) avoid capture – for example

bar.z = 200
foo =
  z = 100
  bar.z + bar.z

view foo properly renders the references as bar.z, not z, which is the shortest unambiguous suffix, but z is not free. we do have the variable capture issue when we can't add more segments, e.g. if you move.term bar.z z then view foo it'll erroneously render as

foo =
  z = 100
  z + z

however, I made this issue because I observed a line like

stopId = Prediction.stopId prediction

get rendered as

stopId = stopId prediction

during an update. not sure why that'd behave differently than view.

mitchellwrosen commented 2 months ago

ah, I think the issue is with use clauses.

restating the example above, I have a term with a let-binding like

stopId = #xyz prediction

and a naming environment

#xyz => "Prediction2.stopId"

this could render correctly as

stopId = Prediction2.stopId

but due to other uses of #xyz in the same term, our "use"-sprinkler decided to kick in and render

use Prediction2 stopId
stopId = stopId prediction

which is incorrect, since use Prediction2 stopId is to effectively rewrite all freestopId as Prediction2.stopId, but stopId is not free in stopId = stopId prediction

mitchellwrosen commented 2 months ago

I haven't been able to reproduce this one. We do have logic that attempts to avoid inserting a use clause in these cases (see TermPrinter.countHQ), and so far I haven't figured out how to intentionally break it.

ceedubs commented 2 months ago

@mitchellwrosen is it possible that when you hit this you had printed some terms to your scratch file and then ran a command like switch or merge or upgrade that changed pretty-printing environment such that the disambiguation used by the pretty-printer was no longer valid?

mitchellwrosen commented 2 months ago

@ceedubs I don't think so... I believe I saw it by just performing an update, which just rendered a term in the current project context like

whatever =
   use Prediction2 stopId
   ...
   stopId = stopId prediction
   ...

rather than

whatever =
  ...
  stopId = Prediction2.stopId prediction
  ...