[Agda] An exercise in typing

[Roman]

Hi,

I stumbled upon a funny challenge some time ago and wanna share the
essential part of it.

Can you define `recN` that computes like this:

    recN 0 ~>* λ k f -> f
    recN 1 ~>* λ k f -> f (k λ x -> x)
    recN 2 ~>* λ k f -> f (k λ x y -> x) (k λ x y -> y)
    recN 3 ~>* λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)
    ...

where `x`, `y` and `z` all have different implicitly bound types.

If that doesn't sound hard enough, here's an additional condition:
don't use any `data` or `record` types (tuples included) apart from
the type of natural numbers.

If you're curious where the functions that `recN` computes to arise
from, they're a part of the "Unraveling recursion: compiling an IR
with recursion to System F" paper [1].

The challenge template with full details can be found here:
https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda

Copy the file and replace

    postulate
      kitRecN : KitRecN

with an actual definition of `kitRecN`.

Hope I'm not alone thinking it's a funny challenge.

--------------------

[1] https://files.zotero.net/eyJleHBpcmVzIjoxNjU1MDQzNzQ3LCJoYXNoIjoiNTUwYjc1ZjVkNGYyNzVlMjQ2OWNhMWIxYjUxODkyZTAiLCJjb250ZW50VHlwZSI6ImFwcGxpY2F0aW9uXC9wZGYiLCJjaGFyc2V0IjoiIiwiZmlsZW5hbWUiOiJLaXJlZXYgZXQgYWwuIC0gMjAxOSAtIFVucmF2ZWxpbmcgcmVjdXJzaW9uIGNvbXBpbGluZyBhbiBJUiB3aXRoIHJlY3Vyc2kucGRmIn0%3D/355301e3f049d523f8705af363927604bca986aed61c7c350fddc70a5e70f109/Kireev%20et%20al.%20-%202019%20-%20Unraveling%20recursion%20compiling%20an%20IR%20with%20recursi.pdf