#291 better type synthesis for datatype

[Laurent Voisin]

In Rodin 2.5 AST library, type synthesis is implemented only for type constructors (the easy case).

It was not implemented for constructors and destructors, as this would in the general case be as complex as full type check (i.e., one needs to do unification on types).

However, in very simple cases like enumerated types (where the type is constant) and constructor cons of a list (where the type of the constructor is the same as the type of its second parameter), one could implement a very simple type sythesis algorithm.

This would make the AST library more efficient in these cases, without the need to resort to full type unification during type checking.

[Laurent Voisin]

This has been implemented for destructors (where we already have the full type instantiation of the datatype.
This has also been implemented on constructors when there is no type parameter.

[Guillaume Verdier]

These changes have been merged in commit [df38cb].