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.)