lsp: unprincipled mess of jump-to-definition

[cuematthew]

In the following all fields with numeric suffixes have the number purely for ease of discussion; they should be considered equal if the non-numeric part matches. E.g. f1 is the same field name as f2.

Currently:

	d: {f1: _} | {f2: _}
	d: f3: _
	e: d.f4

f1 resolves only to itself. f2 resolves only to itself. f3 resolves to {f1, f2, f3}. f4 resolves to {f1, f2, f3}. This is questionable: arguably f1 should resolve to {f1, f3}, and f2 should resolve to {f2, f3}. Because f1 MUST be unified with f3, and f2 MUST be unified with f3. But f3 MAY be unified with f1; it MAY be unified with f2.

If we change the | to &:

	d: {f1: _} & {f2: _}
	d: f3: _
	e: d.f4

now, f1, f2, f3 and f4 all resolve to {f1, f2, f3}. This seems right - all of these fields MUST be unified together.

For if/else:

	c: bool
	d: {
		if c {
			f1: _
		} else {
			f2: _
		}
	}
	
	d: f3: _
	e: d.f4

Unfortunately, here f1, f2 and f3 all resolve to {f1, f2, f3}. This seems very wrong: with the disjunction, we should probably avoid f1 and f2 resolving to each other, but here we should definitely avoid f1 and f2 resolving to each other.

I can see users wanting both MAY and MUST analysis. Currently, they reliably have neither. We currently use jump-to-definition. We could also start to make use of jump-to-declaration, and have one do the MUST and the other do a MAY.

[mvdan]

I've never understood the difference between jump-to-definition and jump-to-declaration; how is that used in other LSPs and languages? Is it perhaps for languages with separate header files?

My instinct is that I want "MAY" instead of "MUST", because I understand the LSP to be a best-effort and high-performance partial evaluator, hence I don't demand precise answers from it. And getting more answers is generally nicer than getting fewer, because I can always select the one I'm actually interested in, rather than having it be omitted sometimes.

[cuematthew]

My instinct is that I want "MAY" instead of "MUST"...I don't demand precise answers from it.

There are a couple of dangers here. One is that this gets you far too many results. Consider something like:

d: e | f

you're deep within e and you care about some field x. There might be hundreds of x declarations within f. Do you want to see them? Sometimes, yes. But the MUST analysis seems to offer a way to limit the scope of your query. Is that useful? Does that help avoid seeing lots of results that are irrelevant?

The second danger is it means the results would include collisions. E.g.:

d: {f: true} | {f: false}

If you saw in the results that f must be both true and false you might think this must be a bug. So if you're already trying to debug some cue and figure out what the mistake is that's causing some conflict somewhere, being presented with a mix of "yes this conflict is fine" and "no this is the real bug you're looking for" might be annoying. Whereas the MUST would definitely not include any of the "yes this conflict is fine" cases.

...I understand the LSP to be a best-effort and high-performance partial evaluator,...

I believe that there would be no computational cost in the LSP to separating out MAY from MUST. I think we're already doing all the work, we're just not modelling things properly.

[mvdan]

Understood about the cases where "MAY" can be too verbose or confusing. That makes sense.

If the LSP already does most of the work towards separating "MAY" from "MUST", it sounds like being able to offer both options to the user is best. The tricky part is the UX; what should the default behavior be for go-to-definition, and what would we use to offer the alternative version?

[mvdan]

I'll say that there is an alternative to a binary choice if we cannot decide which is the best default; the default behavior could instead be a mix of MAY and MUST, based on what we feel is closest to what most users will expect based on the context of where the cursor currently is. And then we could offer MUST and MAY as two other commands/actions.

[seh]

I do think that jump-to-declaration and jump-to-definition should be different things.

Like Daniel said, the difference between them is either confusing or immaterial in some languages. In C or C++, I understand the difference. In Go, I do not, or might instead say that there's no such thing as a declaration, even though the specification most definitely says that there is, but it involves binding the variable to a value, even if only the zero value implicitly.

I haven't through through this as carefully as Matthew, but I expect these two operations to answer different questions:

• jump-to-declaration: Where can I find this struct field on the left side of a colon inside of a struct (or the top-level)?
• jump-to-definition: Where does this struct field wind up getting constraints and values bound to it?

I recognize that in CUE, there's not really a clear—or perhaps any—distinction between those two interests. Still, though, I think about them differently. Consider an example:

#Thing: {
  x: int
  y?: int
}

t: #Thing & {
  x: 42
}

There, the x: int inside of #Thing feels like a declaration, and the x: 42 inside of t feels more like a definition.

Consider if we add in more:

#Thing: {
  x: >1
}

That x: >1 feels like a definition, but not as strongly as x: int does to me.