Warn user when a type variable in a type constraint has been instantiated.

[hnrgrgr]

It seems to be a common misunderstanding amongst beginners that type variables in type constraint are unification variables and that they should be explicitly quantified when desired.

This small patch adds a warning when such non-quantified variable has been instantiated by the type checker. The verification is made /a posteriori/ by looking for type constraints in the typed tree.

I'm not sure this warning is really a desired feature, but it is probably worth discussion. For instance, ocamlyacc-generated files use such variables on purpose.

[gasche]

If we accepted '_a in programs and didn't warn on those, we could enable the warning for everyone -- and progressively convert codebases to use '_a for non-generalized inference variables. With the current practices it seems hard to enable the warning except in constrained educational settings, but I think it's still good to have it around.

[trefis]

@gasche do you know why '_a is not accepted?

With the current practices it seems hard to enable the warning except in constrained educational settings

I disagree. I'd be surprised to see people use 'a while expecting it to be unified with int.

I really like the idea of this PR btw!

[gasche]

Let's formulate this differently: you cannot willingly forget 20 years of (admittedly dubious but voluntary) flexible variable semantics and claim that it's actually a mistake to use them that way. It may seem surprising to you but some people are familiar with the current semantics of type variables and have used it in their codebases -- note that there is no alternative, while it is now possible to explicitly enforce rigid variables with ('a . ...). There even are people that consider the current flexible semantics is the right default.
Warnings are generally used to deprecate a feature, send a signal that "from now on you should avoid that" -- unused variables, (or), resolution of ambiguous record labels by the shadowing rule. It is not possible in this case, or rather would severely restrict expressivity of type annotations. In absence of an alternative to avoid the warning when flexible named variables is what you want, it should be considered not a general recommendation for all codebases, but a specialized recommendation for codebases that are simple enough to not need that -- educational purposes.

I like the idea as well. I did a code review but, besides the universal pattern Thomas spotted already, I couldn't comment much, as I'm not familiar with the type-checker codebase. Alain may have more to tell. I wondered whether this should be a delayed check or not, but my understanding is that the implementation only check variables at "safe points" (after checking a toplevel phrase or complete module structure) where it is a precondition that all local inference constraints have been solved.

[hnrgrgr]

Disabling the warning for type variables like '_a would indeed be consistent with warnings triggered by unused (value) variables. Unfortunatly '_a is already used in pretty-printing of weak type variables.

[lefessan]

Actually, there would be some consistency in having no warnings on '_a, as such variables indicates that they are actually not polymorphic, and should be eventually instantiated. So, we should accept such variables, and warn, on the contrary, if they are not instantiated, while not warning if they are.

[lpw25]

Note that -- because of structural types -- some things can only be expressed in OCaml using unification variables. For example, this (nonsense) function can only be written using unification variables:

# let rec f n (x : < m: 'b. 'b -> 'a > as 'a) =
    if n < 0 then x
    else if n = 0 then f (n - 2) (x#m 5)
    else f (n - 2) (x#m 6.0);;
val f : int -> (< m : 'b. 'b -> 'a > as 'a) -> 'a = <fun>

I'm not sure that we should add a warning which goes off for any possible definition of perfectly valid functions.

I also think, that unification variables are used more often than people think: almost every use of as in a type expression for instance.

My preferred approach to helping people to understand the difference between unification variables and type variables would be to have the compiler accept the syntax:

val id: 'a. 'a -> 'a

for value specifications, and also to print value specifications with that syntax by default. This would mean that type variables were consistently bound in OCaml, and unification variables were consistently unbound.

[lpw25]

I think your patch still gives a warning for uses of as like this:

# let rec f (x : < m: int; .. > as 'a) : 'a option =
    if x#m < 0 then None
    else Some x;;
val f : (< m : int; .. > as 'a) -> 'a option = <fun>

which I think are very common.

[hnrgrgr]

Indeed, your example should not trigger a warning. I forgot that case, thanks. I have updated the patch to handle this case. Maybe not the best implementation, but it should be sufficient to test.

[lpw25]

I think your patch still gives a warning for uses of as like this

Oops, I had only seen the changes to extract_vars, and completely missed the addition of extract_aliases. Your updated patch should be fine for the examples I showed.

[hnrgrgr]

Unfortunatly, it isn't.

[hnrgrgr]

Here is an updated version, with proper 'scope handling' for aliased variables.

[bobot]

Even if I don't like it, the implicit coding rules of the compiler forbid this | and the rule have been enforced in other merge request.

[alainfrisch]

There are many occurrences of '|' on the first branch in the compiler code base. I don't think anyone would complain about this style.

[bobot]

Great! Thank you, I'm happy to hear it. I will stop removing them from my patch.

[damiendoligez]

If anything, I would complain about the absence of the first |. But I've learned not to complain too much.

[dra27]

However, changing just this is more of a concern, as the diff is unnecessary!

[mshinwell]

@garrigue It's been more than three years since the most recent update of this patch, as far as I can see. Is it going to be merged? If not then I think we should close the pull request until someone steps forward to bring the code to a mergeable state.

[garrigue]

We are not going to introduce this change, as it is not "backward compatible" (i.e., doesn't fit well with the existing codebase).
But we're still reflecting on improvements to the handling of type variables.