Improve error LSP ranges on type mismatches

ChrisPenner commented 3 months ago

Overview

When you get a type mismatch on the type of a do or let block the range reported for the error is the ENTIRE block, which lights up the editor like a Christmas tree, which is annoying and less-than-helpful for finding where the error actually is.

This changes the range to be just the "leaf expressions" of the returned value of a block which results in a much more reasonable error highlight.

One time where you may not want this is if the type of the block itself is wrong; e.g. 'Nat vs Nat; I've special cased that situation and will highlight the whole block and print a hint suggesting adding/removing a do.

Old: Highlights the whole humongous block 😢

New: Highlights only the relevant final line.

Hint for superfluous delay:

Hint for missing delay:

Implementation notes

Added an AST crawler to the LSP range calculator for type mismatch errors. It simply crawls down the expression that's causing the type error, if it's a Let/Do block it crawls inside and finds the terminal expressions within the block and returns those annotations instead.
Adds a new typechecking helper that just checks if either of two types are a subtype of the other if a delay is added.

Test coverage

[x] LSP diagnostic range tests

Loose ends

Might we want to alter UCM's type-mismatch message to include the more accurate ranges too?

ChrisPenner commented 3 months ago

Had fun getting ormolu to work properly here... turns out there's a non-determinism bug, if you have a {- -} style comment followed by a -- style comment in an ADT definition 🤷🏼‍♂️

Fixed it by just rewriting the comments.

ChrisPenner commented 3 months ago

@aryairani would be good to test this out on trunk for at least a little bit before it goes out. Shouldn't be outright harmful, but might require a little tweaking for unexpected edge-cases.

TBH though I think it's likely to be a universal improvement over the current version 👍🏼

aryairani commented 3 months ago

Before and after looks good!

Might we want to alter UCM's type-mismatch message to include the more accurate ranges too?

Maybe?

For do it's a little tricky (even in the LSP case), because the do keyword changes the type, adding the delay. e.g. If the expected type is 'Nat and we have 'Int then it makes sense to crawl down to the Int. If the expected type is Nat and we have 'Int then the whole do is wrong.

aryairani commented 3 months ago

Seems obviously good in the let case, but not sure about the do case, and because of that I'm hesitant to merge it as-is.

We could 1) smart match on the () -> part of the delayed computation type and either say the problem is with do (vs let) or with the body, depending?

Or we could 2) change this PR apply to only let and merge that, and then brainstorm some more on do?

Or we could 3) merge it as-is, possibly making do weird, but fixing it later.

@pchiusano Any thoughts?

I guess my preference is 2, 1 (but time-boxed), 3 in that order; unless there's an obvious easy theoretical answer.

ChrisPenner commented 3 months ago

Yeah I think it'd be good to detect a 'Nat vs Nat sort of type-difference anyways and thoughtfully suggest adding/removing a do; that'd be a good UX anyways. I'm not sure what's all involved in that, but it sounds doable haha :D

TBH I'm not sure we actually avoid the issue if we only do it on let cuz if you have:

foo : 'Nat
foo = let
  ...
  1

Then this will show the error on the 1 and say Nat is not 'Nat, which is just as bad as the do case I think; though maybe is less likely to happen.

aryairani commented 3 months ago

Oops, good point. Well... side note, I kind of thought our type provenance algorithm was already supposed to do this, do we just need the ability to drill down into the type automatically? Do we not have that.

Sorry I don't have a laptop this week but maybe there's a tweak or bug in the annotations that's causing this to happen like if we have do 1 and it has type 'Nat ... I don't remember if the Nat part has its own provenance separate from the '? I think no but hope yes, in which case why does it not already do the right thing?

Anyway it would definitely be good to get this working. Sorry I'm rambling.

dolio commented 2 months ago

So, my understanding of the reasons behind these two poor behaviors is as follows.

For the foo : Nat vs. foo = do ... example, the reason for the verbose error is that this is the problem:

check (λ Delay. ...) Nat

However, check only stays in checking mode if a lambda is checked against a function type. So this falls through to just synthesizing the lambda expression's type and matching it against Nat, which fails. Without some kind of special case for this, you're never going to get a nice error directly out of the type checker, because it's just a mismatch of the ascribed type vs. the whole lambda expression. So I guess you need some kind of error parser special case for this, unless more cleverness is added to the case of checking a lambda expression. I'm not sure what would be appropriate for the latter in general, though.

In some sense, this is caused by desugaring do to a lambda expression, and handling the latter generically. If there were some peculiarity that allowed the type checker to reliably detect when something is a do, maybe you could give a more informative error more directly from the type checker. I'm not sure how worthwhile that is, though.

The other case could be improved in the type checker, though, I think. What is happening right now is that

checkWanted (let x = ... ; y) t

eventually directly calls:

checkWanted y t

The reported errors rely on scoping information that is supposed to be pushed/popped during type checking, but the let case is not pushing a scope for its body. So, when you have a string of lets, the only scope in play is the whole let. I think if you replaced the recursive call with checkWantedScoped, it would give a more targeted error, although I don't know how what I see in terminal ucm corresponds to lsp exactly.

Possibly with this change you wouldn't need to crawl to the leaf of the let for some errors. But, you'd need a different strategy for reporting your whole block do error. Maybe it would be nicer this way, though, because there is probably enough context in the scopes for the latter. You could try popping the scope information until you reach a let or something. I'm not 100% certain.

You probably need a couple cases in checkWanted to be tweaked. Like, both Let and LetRec cases. Not sure if any others are missing appropriate scoping information.

unisonweb / unison