A few questions about supercompilation

[Hirrolot]

Thank you for your work on this project. It was really helpful for me to study the code after reading papers on supercompilation.

I have a few questions on the subject matter (I hope this is an adequate place to ask questions):

1. Suppose we have a higher-order language. We can write a supercompiler for it directly (as in the project HOSC), or we can perform closure conversion and launch supercompilation on a closure-converted language term. The advantage is that writing a supercompiler for a first-order language is much simpler. Do you see any obstacles of doing so? Have people already experimented with this approach?
2. Have you seen a project/paper where supercompilation is used for deciding equivalence of terms during dependent type checking?
3. Where can I find samples of SLL code for stress-testing a supercompiler? In the future, I want to do some profiling of supercompilation and, possibly, find ways to optimize it.

Thanks again and enjoy the New Year!