Background

Consider the example below - what should be the type for f?

let f ~g x = g (x: _ @@ local) x [@nontail]

Ideally it should be something like g:(x @ local -> x -> y) -> x -> y. (Both x and y are both types and variables names, for easier reading). Note that g could also be of type x @ local -> (x -> y), but this is undesirable because it has extra parentheses. However, for printing and generating mli-less .cmi files, the defaulting will push modes on arrows to legacy (global), giving the undesirable type.

The original check_local_application_complete solves this problem by enforcing currying constraint in a single application. For the above example, x being local forces the partially-applied g x to be local as well.

The improvement

This PR does two things:

• The function was intended only for the locality axis, for which mode_fun <= mode_ret and mode_arg <= mode_ret. In general we have monadic and comonadic axes, for which the constraints should be partial_apply mode_fun <= mode_ret and close_over mode_arg <= mode_ret.

• The constraint is not for soundness but just for better types. Therefore, failed constraints should be warning instead of error.

Please review by commits.