Add tests to serve as some documentation for PostInferenceChecks

[Smaug123]

Below the line is what I thought beforehand, but I'm pretty sure it's false. So I've simply reverted all the actual changes in behaviour and left the tests, in the hope that Those Who Come After will be better able to see what properties these functions have and can save a bit of time working it out.

---

There was no need for this to be in continuation-passing style, and the stack traces look a lot nicer this way - much less pollution.

Handwavy proof of correctness:

There is only one caller of CheckExprLinear other than CheckExprLinear itself, and that caller passes id as the continuation.

The call on line 1004 supplies NoLimit as the base case of the recursion; I have extracted this out to the ultimate non-recursive caller of CheckExprLinear.

The only other call to CheckExprLinear which manipulates its result is the one on line 1011. That calls CombineLimits [lim1; result]. CombineLimits is defined as follows:

let CombineLimits limits =
    (NoLimit, limits)
    ||> List.fold CombineTwoLimits

CombineTwoLimits can be observed to be commutative and associative (as verified by property-based test), which simplifies the analysis because we don't have to care about the order of the recursion changing.

[Smaug123]

Is it generally acceptable to put an internal function into the corresponding FSI file so that it can be unit tested? In this case, CombineTwoLimits, which I want to assert has the properties I claim it has (to make this refactor safe).

[T-Gro]

Is it generally acceptable to put an internal function into the corresponding FSI file so that it can be unit tested? In this case, CombineTwoLimits, which I want to assert has the properties I claim it has (to make this refactor safe).

I would say go ahead, the test projects are IVT'd, incl. FSharp.Compiler.UnitTests.
We already have FsCheck in Fsharp.Core test project, so you can also bring it over to the Compiler.UnitTests.

[T-Gro]

(didn't mean to close this PR, was an accidental mispress. I am sorry)

[vzarytovskii]

Is it generally acceptable to put an internal function into the corresponding FSI file so that it can be unit tested? In this case, CombineTwoLimits, which I want to assert has the properties I claim it has (to make this refactor safe).

Yes, this is fine, go ahead.

[Smaug123]

I am not remotely convinced that my understanding of Limit here is correct, but I've tried to document it.

[Smaug123]

(I still intend testing these functions now I've exposed them, by the way.)

[Smaug123]

So it turned out that one of my claimed properties is not true ("NoLimit is a zero for CombineTwoLimits"), which the tests immediately discovered. I'm just thinking through whether that affects the proof that I haven't changed any behaviour. The semantics of Limit (and more particularly the scope field) are really not obvious!

[Smaug123]

I've chosen not to use FsCheck here, since it was very easy to stamp out a rough approximation of it, but if you prefer I can pull it in so we get e.g. better distributions over the generated integers.

[Smaug123]

Sorry about that, things have been busy - let me merge in main and see what's up.

[Smaug123]

As of this commit, I intend to have removed all the changes in behaviour again; I propose merging the tests and just leaving it at that. It took me a nontrivial amount of time to convince myself of the properties that I assert here with tests, so I think this is a small improvement over main because they're now documented.