Track in type qualifiers additional information about restricted types in the presence of polymorphism

[ilyasergey]

At the moment, we impose the following intrinsic restrictions on certain types, that are not imposed by the general-purpose type-checker:

• Keys of maps are always primitive types
• Values of messages are always storable types

This becomes to difficult to enforce statically for the polymorphic functions. For instance, a tfun can take a parameter and then use a value of it as a key for a map.

let tf = 
  tfun 'A =>
  fun (m : Map 'A Bool) =>
  fun (k: 'A) =>  
  let t = True in 
  put m k t (* This is okay *)
in
let tf_applied = @tf (Some (Bool)) in (* <- This should not be allowed *)
tf_applied ...

This should be prevented at the call-site, but for that we need to track the fact that a type is "used" for map keys, and infer it from the corresponding tfun definition. For this, there is currently a "qualifier" in the type checking mechanism.

[ilyasergey]

This depends on #143.