Type inference ignores unreachable code

[myreen]

Surprisingly the compiler accepts:

foo n = if n + () then () else ()

main = Ret ()

While it rejects the following:

foo n = if n + () then () else ()

main = Ret (foo 5)

[hrutvik]

Currently, letrec transformations happen before type inference, removing such unreachable top-level declarations before inference sees them. I believe we chose this ordering due to a lack of type signature support (#25), which makes it more efficient to untangle letrecs before attempting to infer their types from scratch. We can reorder inference/transformation provided we prove that the letrec transformations preserve typing, at a (small?) loss of efficiency until type signatures are supported.

[hrutvik]

As discussed in a meeting, we have decided to:

• topologically sort letrecs and convert non-recursive ones into lets before type inference (as before)
• move the pass which deletes unreachable letrecs after type inference

This ensures that dead code will still be type-checked, but removed before demands analysis. We will need to prove that deletion of unreachable letrecs preserves typing. We should also be able to prove that the passes before type inference preserve free variables, so that the parser no longer needs to check for closedness.

[hrutvik]

65f55650c57cd04e5cd36f0aed2c9e59faf00252 moves both conversion of non-recursive letrecs and deletion of unreachable letrecs to after type inference. The pass making letrecs distinct and the topological sort remain before type inference.

Unfortunately the parser still has to check for closedness (contrary to the comment above): the distinctness pass can delete free variables. Users can still trigger some of the unexpected behaviour by duplicating declarations, e.g. the following is accepted:

foo = <ill-typed>

foo = <well-typed>

main = do
  Ret foo
  Ret ()