Type-checker extended to type-inference engine with one line :-)
Type-checker extended to type-inference engine with one line :-)

NOTE: so far we have no propagation rules. The output in our example
is quite close to OCaml's one (up to management of multiple occurrences:
we are less restrictive than OCaml with refs, more restrictive then
OCaml with Hindley-Milner). Maybe we could use propagation to simplify
the output a bit. I expect, however, that propagation will be more useful
when we consider an harder example with multiple calls.

LPCIC/elpi