Positivity check in type constructors

[loutr]

Right now, EasyCrypt refuses the definition

type 'a tree = [
  | Leaf of 'a
  | Children of 'a tree list
].

This is because the positivity checker refuses any occurrence of the datatype within the parameters of another type constructor (here, list). This PR changes the positivity check algorithm and allows such definition. Please note that induction principle generation is left unchanged for now, and that the corresponding induction principles are not useful as-is (see note below).

Also, this PR includes some typo fixing. If the changes are considered to big, I can make it into a separate PR.

---

Note that there is some code duplication in the functions below because the current algorithm performs at two levels: first it evaluates, for a given path p (i.e. a type constructor in the AST), whether all its occurrences are positive. This requires, at a second level, to evaluate whether all occurrences of type variables instantiated by p also appear strictly positively in the corresponding type constructor.

Future developments

Additionaly, note that EasyCrypt allows to declare inductive types which change the order of their type parameters, e.g.:

type ('a, 'b) permlist = [
  | Nil
  | Cons of ('a * ('a, 'b) permlist)
  | Perm of ('b, 'a) permlist
].

These types may not be used right now in some positions as it would make the check (potentially much) slower. In the future:

• lift this restriction with a new implementation that uses some form of union find/constraint-solving structure in order to evaluate strict positivity for every type variable of the constructor, and store the resulting list/array in its definition. This would also make the check faster in general, as type declarations would only need to be traversed once, when they are being defined;
• maybe remove the corresponding inductive principle for these types. Also, provide a correct induction principle for simpler types (e.g. tree defined above).

[loutr]

I think this extension of the positivity checker is satisfactory for now. In the long run it would be nice to replace it with a more robust analysis (using some union/find structure & constraint solving, as described in the original message). Several notes:

• Error reporting has a stack-based look, which aims at being more informative. I don't master the (weird) arcanes of the Format library so boxes tend to put line breaks at unexpected places sometimes (in the middle of a type for instance)

type ('a, 'b) arr = 'a -> 'b.
type ('a, 'b) orr = ('a, 'b) arr.
fail type 'a u = [ S | U of ('a u, bool) arr ].
====================================================
Could not verify strict positivity of type u:

  ... in variant U of type u
  ... in type arr (in an instance of type variable 'a)
  non-positive occurrence of 'a in type 'a -> 'b

• This reporting uses a stack that is generated when an error is caught. Because of the structure of the project, this stack is processed in a separate file (EcUserMessages), which I find cumbersome, as it requires to expose all the intermediate types that are used during error reporting. The alternative would be to process the error in the EcInductive module. I believe it isn't possible as is, given that this requires at least to have access to the definitions of EcPrinting.pp, EcPrinting.pp_type and a few other values. However requiring EcPrinting causes a cyclic dependency between modules.
• This PR does not attempt to solve Non-emptiness test does not always terminate #859 as non-emptiness test is a distinct feature.