| So my questions are: Am I right in assuming that CoreLint accepted programs | should not segfault? Yes. Modulo unsafeCoerce, and FFI calls. | What about internal invariants? Should CoreLint check | for those? Is there any pass that checks for invariants and prints helpful | messages in case of a invariant invalidation? Yes; they are documented in CoreSyn, which the data type, and Lint checks them. | As an attempt at debugging the code generated by my plugin, I wrote the | function that is supposed to be generated by my Core pass in Haskell and | compiled with GHC. Generated Core is mostly the same, except at one point it | has an extra lambda directly applied to a void#, something like ((\_ -> ...) | void#). Where can I learn more about why GHC is doing that? Show me the code! Instead of generating x :: Int# = <some expression that might fail> GHC sometimes generates x :: Void# -> Int# = \_ - <some expression that might fail> and then calls (x void#), to make any div-zero failures happen at the right place. I'm not sure if that is what you are seeing, but we can work it out when you give more detail. Simon