Improve error LSP ranges on type mismatches

[ChrisPenner]

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

• LSP diagnostic range tests

Loose ends

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

[ChrisPenner]

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]

@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]

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]

I think this extra space may have been intentional to allow the types and the :s to line up. I would move the space after the : to preserve that the types line up, or just revert this line altogether.

[ChrisPenner]

I think this has caught me like 3 times now, I admit I don't find it very intuitive 🙃
I'll move it to after the : so I don't do this again in 3 weeks haha.

[aryairani]

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]

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]

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.

[ChrisPenner]

@pchiusano is this a reasonable way to do this? I suppose ideally this would be done inside the typechecker itself, but it seems like a pretty simple type to check against 🤔

It works in simple cases; but unsurprisingly doesn't seem to work with polymorphic types; e.g. this doesn't trip the hint:

y : '(e -> Nat)
y =
  _ = 1
  _ = "one two three"
  (_a -> 2)

If adding it correctly to the typechecker is difficult it's still beneficial to get the hint sometimes rather than not at all; but would be nice if it worked in all cases :)

[ChrisPenner]

cc @dolio

[dolio]

So, here's a possible idea for how to make the typechecker facilitate some of this. Up to you if you want to try out implementing it.

So, we can detect do in the typechecker because it turns into Lam body where Var.typeOf (ABT.variable body) = Delay. We can try to detect 't in the typechecker by looking for a check against () -> t. So, you can try to partition the checking problem into three cases:

1. Checking λDelay -> ... against () -> t: this looks fine, so just continue as normal
2. Checking λDelay -> ... against something else: this might be a bad do, so put something in the error scope that indicates this.
3. Checking something else against () -> t: this might be a missing do, so again put something in the error scope.

Then you can try to parse the improved error information in some situations. Like, if you got a leaf mismatch with an arrow vs. something else, you could look to see if one of these do indicators is upstream, and report something about that instead.

I think with this approach, you might be able to identify the example you mentioned above. I'm not 100% sure that it wouldn't cause some other weird corner cases, though.

[dolio]

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.