Has anyone used Pottier and Gauthier's polymorphic defunctionalization in a modular compiler? Defunctionalization is a program transformation that converts higher-order programs into first-order programs. The idea is that given a program, there are only finitely many lambda-abstractions, so you can replace each lambda with an id, and each function application with a call to an apply procedure which branches on that id.  This is sometimes used in compilers for functional languages, but its applicability is limited by the fact that defunctionalization is a whole-program transformation (you must statically know all of the functions in the program), and so only whole-program compilers make use of it. 

However, Pottier and Gauthier have a given a polymorphic typed defunctionalization algorithm using a more sophisticated typing involving GADTs. Now, given their encoding, it's possible to add a catch-all case to their lambda datatype that isn't a tag, but which contains a higher-order function. This means that it should be possible to use their encoding to defunctionalize on a module-by-module basis. 

Has anyone done this, and point me to a compiler using this idea? (Toy compilers are okay, and in fact preferred.)
One approach is described by

Georgios Fourtounis and Nikolaos S. Papaspyrou. 2013. Supporting Separate Compilation in a Defunctionalizing Compiler. SLATE 2013.

As @gasche mentions:


  A different approach at the problem would be to consider that each module can define its own "defunctionalized functions" type and dispatcher/handler.


You can "link" those types and handlers with a specialized linker.
Unlike using open datatypes, you concatenate the list of constructors and the case functions.
But the linker must add cases for partial application: Without whole-program analysis, you cannot predict which partial applications can be used for which function, so you add all cases. An $n$-ary function can be partially applied to $i$ arguments (with $0&lt; i &lt; n$) and produce a function of arity $n-i$, which can be partially applied again.