Tracking control-flow linearity for effect handlers

[thwfhk]

This PR will track the control-flow linearity for effect handlers, which will resolve issue #544.

It is very incomplete and full of hacks. More explanation to be added. Currently I just want to create a PR to be able to sync with the main branch.

[dhil]

You'll also have to address the CI failures.

[dhil]

Another thing is that you should hide this feature behind a new flag, e.g. track_control_flow_linearity. If that flag is not enabled, then you should emit an error on uses of any of the features included in this PR.

[thwfhk]

There is one remaining problem (or two):

• The linearity kinds of row variables reuse Unl and Any, where e::Unl means the row variable e can only be unified with linear operations, and e::Any means the row variable e can be unified with any operations.
• As a result, we need to change the the type signatures of library functions. For example, the type of plus should be "(Int, Int) { |_::Any}-> Int" instead of (Int, Int) -> Int, because the latter is less general as it can only be used with linear operations. We can also change the parsing and printing to use -> to represent { |_::Any}-> by default.

[SimonJF]

@vcgalpin and @SimonJF are going to try this out on our examples

[dhil]

@thwfhk there are a couple of failures now. I will merge this PR once the regressions have been fixed.

[thwfhk]

@thwfhk there are a couple of failures now. I will merge this PR once the regressions have been fixed.

Ah yes. That's because I forgot to add the files of some new tests. They should be fixed now.

[dhil]

I'll merge after the CI has run successfully to completion.

[jamescheney]

So... does this close #544?

[dhil]

So... does this close #544?

No as per the meeting yesterday. We keep the issue open for a potentially fun gimmick. We will close it during POPL.