System F
Philip Wadler raised the possibility to use as 'internal' language a 'Church-style' language such as system F (I believe the reference paper for this is John Reynold's 1974 paper 'Towards a theory of type structure') to allow an easy transformation of expressions and types during optimisation. In such a system types are part of the expressions. Optimisations on such expressions will keep a correct type since the optimisation is done on the expressions and types are part of them.
In my current system though, types are not part of the expression. Instead, once calculated by type inference they are kept for each expression (that is every node of the AST has a type attached to it, which is the type of the expression for which it is the root) as a buffer of what happened during type inference.
I tried looking into a way to merge both things, but didn't come up yet with a solution to change my current system easily. I also played a little with the type-based optimisation itself, but without any breakthrough there either.