Fix the typing of generated functions

[agle]

The memory encoding/boogie backend is incorrect currently as it gives the function definitions the type of their return value rather than the type of their function. The problem is the boogie backend to generate the correct (uncurried) declaration needs to identify the return type, which is a function/map type for some. Just returning the last type is wrong in this case as we can't distinguish a -> b -> (c -> d) from a -> b -> c -> d, we return d when we want c -> d.

We need to be able to write code essentially like below, assuming a mutable underlying implementation of unification through unify. Alternatively we could represent function types as uncurried but I'm wary of the impacts of having non-canonical forms of types floating around.

let ret_type = newtype () in
let new_fntype = curry  arg_types x in
let utype = unify new_fntype func_type in
ret_type

I have a partially complete implementation of hindley milner type inference, this aims to fix this but is a large change set. This issue covers just this function unification algorithm, which I will try to merge independently.