Inline anything

[jespercockx]

As the title of this PR suggests, this changes the inline machinery of agda2hs so you can try to inline any function. If a function marked as inline was not inlined, then we get an error upon encountering the non-inlined application. I also added a somewhat interesting test case that makes use of this more advanced inlining.

[jespercockx]

Note that this builds on #430 as I needed the global environment that was added in that PR.

[jespercockx]

So apparently this did cause one regression in the test suite that I didn't spot before because of other unrelated CI failures: underapplied applications of functions that are marked as inlined are no longer eta-expanded automatically. I'd argue that the old behavior was going beyond what would normally be expected of an inlined function. Also there is an easy workaround: you can use a lambda-abstraction in the definition of the inlined function instead (or you can just eta-expand all the calls to it). So I don't think this is a big problem.

[jespercockx]

@flupe since you implemented the original version of the inline pragma, what do you think of the issue with the new version not doing eta-expansion?

[jespercockx]

I see no negative comments so I will assume this is good to merge.