Has anyone used Pottier and Gauthier's polymorphic defunctionalization in a modular compiler?
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.