Printing polymorphic mode variables

[ageorg29]

Prints polymorphic mode variables and their constraints. In general, mode variables is printed in [...] containing its lower and upper bounds and constraints as follows: [< ... & ... > ... | ...]. Lower and upper bounds refer to the constant bounds on the polymorphic variable, and constraints might refer to other mode variables.

If a mode variable has no bounds or constraints, it is printed as a fresh mode variable name: 'm, 'n, 'o, etc.

Printing mode variables requires an expensive pre-processing step, which is only applied when -extension -mode_polymorphism_alpha is on.

Below are some examples:

• val id : 'a @ [< 'm] -> 'a @ [> 'm]
• let fst x y = x involves currying, and gets printed to val fst : 'a @ [< 'm & global many > aliased] -> 'b @ 'n -> 'a @ [> 'm | aliased]. Here, since the curry mode is zapped to legacy, the first parameter gets constrained to global many aliased.
• let fst x = fun y -> x on the other hand is eta-expanded, and has slightly different constrains: 'a @ [< 'm & global many] -> ('b @ 'n -> 'a @ [> 'm | aliased]) @ [> nonportable]. The returned closure is polymorphic, but must be nonportable since it must account for the case where the input is uncontended.
• let type 'a mytyp = { a : 'a @@ portable } then let f x = x.a is inferred and printed as val f : 'a mytyp @ [< 'm] -> 'a @ [> 'm mod portable]. Here mod portable stands for a meet, and the type expresses the output is lower bounded by 'm, except for the portability axis, which is lower bounded by portable.