Hindley-milnder type inference

[agle]

This forms the skeleton of the hindley-milner type inference system. This comprises:

• A minimal hash-consed type expression representation in a union-find structure used for type inference (typeExpr.ml).

This is essentially:

type 'a type_expr = Var of tvar | TypeConstr of 'a list * string

This should be sufficiently general to represent anything we want.

• Extraction from bincaml expressions to this representation
• Union-find based HM type unification/inference
• Elaboration pass over program

I expect the current inference and elaboration to not cover the whole program structure yet.

• I will write more on the design later to make it reviewable hopefully.
• I will consider this mergable when we have some tests and a function for local expression type inference which we can use to solve the problem with the boogie backend: Fix the typing of generated functions #208. I've had it floating around a while and want to get it in so I can start the migration without getting conflicts.~~

Similarly it doesn't do anything special to make sure the polymorphic ops get typed, identifying type errors, or let-generalisation. It doesn't do much yet as everything comes in typed already from the frontend; that will need a refactor to not enforce typing immediately.

We still generally use online type propagation from variables to get types, over the explicit typ field in each exprssion node; that will also need to be fixed in order to migrate to this system.

[katrinafyi]

My first thoughts are that I think the inference.ml should be split up. There's a few separate things happening inside there. Forgive any imprecision but my impression is that it's roughly...

• expression-level type unification
• intrinsic-level type scheme definition and instantiation (?)
• statement-level
• procedure-level including parameters
• big everything procedure inference
• concretisation back to Bincaml types

I won't direct you about details but you get the idea. It would also let you write module-level docs for each idea closer to the code.

Generally, I would also like to see more.. restrained use of single-letter module names and local opens where possible.

[katrinafyi]

important comments/questions

[katrinafyi]

Suggested change

	| TypeConstr (ls, _) -> List.fold_left ( || ) false ls
	| TypeConstr (ls, _) -> List.for_all Fun.id ls

[katrinafyi]

I don't think it's possible to review this PR properly, so I am really just making sure that it's documented enough and organised enough.

This will be the last major round of comments.