Add polymorphism into the language

[denismerigoux]

trafficstars

The language does not have any polymorphism right now. Support for polymorphism should be added in the default calculus representation via a classic Big-Lambda type abstraction with type variables. Big lambdas should be explicitly annotated in order to avoid big-lambda inference in the type checking algorithm.

Then, the polymorphism should be reflected upwards in the intermediate representations, and reflected as minimally as possible in the surface syntax. In a first thought, surface syntax should not change at all.

[AltGr]

Some related remarks that will need to be considered here; on the current state of the compiler:

• some built-in operators are polymorphic, like collection mapping or reduction. Their types are hard-coded in Shared_ast.Typing, since in fact the big-lambda can't be expressed in the general AST.
• others are merely overloaded, and resolved early on based on the invariant that the types of their arguments must be known upon application. This works well with the "type propagation" we work with

To make the two work together, we have a slightly tricky invariant on the polymorphic operators we can accept: all the type variables in contravariant position are expected to be instanciated with concrete types when typing the arguments from right to left. Concretely, when typing map(f, x), the function argument f is typed once we know on what type it operates.

There is no contradiction with the feature proposed here, though: we will just need to be careful that we fail properly when a polymorphic operator is applied to a universally quantified type variable. The weird bit will be that our built-in collection operators are able to bypass that restriction through the trick above.