Warn about suspected quadratic behavior in handlers

[dolio]

This PR isn't completely finished yet, but I thought I'd put it up to show off what it does. It looks for handlers where each use of an effect from one ability will result in an extra handler for other abilities being pushed onto the stack, which results in stack copying performance that is linear in the number of effects used, and quadratic overall.

For this, I added the ability to report warning notes from type checking, because we're not completely certain that everything caught by the check is actually bad. The warning currently looks like this:

  🤔 I found a suspicious recursive ability handler.
  
  The argument to the recursive occurrence here:
  
      7 |   { tell _ -> k } -> forget (_ -> k())
  
  only needs the abilities:
  
        {Tell a35, 𝕖32}
  
  but handles:
  
        {Tell a41, Ask Nat}

With coloring that doesn't show up above.

The code it's warning about is:

ability Tell a where
  tell : a -> ()

forget : '{Tell a, Ask Nat} x -> x
forget k = handle provide 3 k with cases
  { r } -> r
  { tell _ -> k } -> forget (_ -> k())

At the moment, the warning output is getting duplicated somewhere, and I need to tweak the type checker a bit to (not) catch certain cases. But after that I think it will be ready to go.

One thing I did not do is any sort of LSP integration. I don't really know anything about how it works, or even what sort of facilities it has for warnings. Perhaps Chris could take a look at some later time.

If you have any suggestions about the display of the warning, let me know, too. I'm realizing I could include more information about why this is suspicious, for one.

[pchiusano]

Nice!!

Maybe something like:

This may be a performance bug, since a copy of the `Ask` handler is
being installed for each recursive call. To avoid any performance bug,
move the `Ask` handler to outside the recursive function, so it is 
installed just once.

Or, you can dismiss the warning by providing a type annotation on the
thunk passed here:

<code snippet highlighting the thunk>

[dolio]

Here's the new warning.

  🤔 I found some suspicious recursive ability handlers.
  
  The recursive occurrences of the handlers are called at a subset
  of the declared abilities, which might indicate that a separate
  handler is installed for each recursive call.
  
  The argument:
  
      8 |   { tell _ -> k } -> forget k
  
  only needs the abilities:
  
      {Tell a97}
  
  but the available abilities are:
  
      {Tell a97, Ask Nat}
  
  The argument:
  
     13 |   { tell _ -> k } -> borget do !k
  
  only needs the abilities:
  
      {Tell a35}
  
  but the available abilities are:
  
      {Tell a35, Ask Nat}
  
  To avoid this warning, you can give explicit types to the arguments
  of the recursive call to the handler.

I decided to only include the informational stuff once instead of for every warning. Only the specific details are printed for each trigger. So, the above text is about two handlers.

[dolio]

I think this has all the tweaks I was working on. I haven't run it on anything large scale, but no existing transcripts were affected.

[pchiusano]

Cool. I'm fine with merging once CI passes and you fix the conflict. And can you change -

The recursive occurrences of the handlers are called at a subset
  of the declared abilities, which might indicate that a separate
  handler is installed for each recursive call.

to

The recursive occurrences of the handlers are called at a subset
of the declared abilities, which might indicate that a separate
handler is installed for each recursive call. 

To avoid performance problems, each handler should only be installed
once. 

We'll probably need some more docs on this, and we might do a pass where
for each error message, we make a page on the docs site to explain common reasons why you might encounter that error and how to fix it.