Yes, that would be the basic idea:
1. Compile the Haskell metaprogram. 2. Evaluate main, possibly with a timeout, in a way that keeps all its structure including lambdas accessible (e.g. Core). 3. Compile the resulting program with other tools.
What is this different tool and how does it fit in to your pipeline? This tool(set) is a specialised compiler for some low-level target platform (FPGA, DSP, GPU - again, no clear decision yet), and it is the second half of the pipeline after the GHC phases.
I have nearly the same plan: I want to compile a restrictive form of Haskell to constant time and space C code for hard realtime embedded targets. Except I need a top level monad with different semantics than IO. Wouldn't a fake driver (fakeRun :: Something -> IO ()) at least simplify the problem? It would prevent you from having to modify GHC to handle a different top level type. And during your evaluation of Core, you would simply ignore fakeRun. -Tom