Wildcards.

One can now write:

let f (x: _, y: _): _ =
  x + y
in

and type inference will work "out of the box".

This is, internally, translated to:

let flex x' in
let flex y' in
let flex z' in
let f (x: x', y: y'): z' =
  x + y
in

Several remarks.
- We may wish a more lightweight syntax so that this becomes even easier to
  write. I didn't experiment too much.
- Right now, because we don't propagate the expected kind, we assume wildcards
  to be at kind TYPE, but if KindCheck.check did have a kind propagation thing,
  we could put a reference in there that stores the expected kind, and
  KindCheck.check would assume TYPE otherwise.
- I found out that we didn't propagate flexible variable instantiations when
  type-checking a function body. This is a soundness bug, so I fixed it, but of
  course tests are broken (rightly so, I suppose), so this is on a branch for now.
Merge branch 'master' into wildcard

Conflicts:
	testsuite.ml
So at least this branch fixes one of the two flexbugs.
And fix the other soundness bug.

This broke other tests.
Fix tree-coroutine.mz

This actually found another bug in the type-checker, which now crashes on this
example.
Add a missing rule.

The type-checker knew that:

  x @ Cons { head; tail } * x @ list a

implies

  x @ Cons { head; tail } * head @ a * tail @ list a

but it didn't know that

  x @ list a * x @ Cons { head; tail }

implies

  tail @ list a * x @ Cons { head; tail } * head @ a
[iteration.mz] and [mutableTreeMap.mz] are now fixed

Also, the call to stash::stash is mutableTreeMap is no longer needed.