Support for Type Inference

[jeromesimeon]

Q*cert includes type checkers for most of the languages. However, this still requires to guess a type derivation. It would be useful to support some kind of type inference in the compiler that can find a type derivation if it exists.

• Type inference for data. Given a brand_relation, this should infer a model (with the same brand relation) and a type which types the data under the model
• And both the data and the model should be the most general ones possible
• Type inference for operators
• Type inference for unary operators
• Type inference for binary operators
• Type inference for CAMP
• Type inference for NRA*
• Type inference for NNRC
• Type inference for DNNRC

The language inference algorithms can assume a typing for the input data.
Polymorphic type inference is known to be NP-complete, but type inference with respect to a given input typing seems to be much simpler.