Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Variance of constrained parameters causes principality issues #8701

Open
lpw25 opened this issue May 30, 2019 · 6 comments

Comments

@lpw25
Copy link
Contributor

commented May 30, 2019

The variance of constrained parameters is only checked, not fully inferred. This means that a type alias with constrained parameters can have a less general variance than the aliased type. For example:

# type 'a t = 'a constraint 'a = 'b list;;
type 'a t = 'a constraint 'a = 'b list

is treated as invariant in its parameter which basically means that 'b is treated as invariant even though it is really covariant.

This means that the relaxed value restriction will not apply if the type is written with t but will apply otherwise. Since unification must arbitrarily choose between aliases this leads to non-principal behaviour:

# type 'a s = 'a list;;
type 'a s = 'a list

# let x : [ `Foo of _ s | `Foo of 'a t ] = id (`Foo []);;
val x : [ `Foo of 'a s ] = `Foo []

# let x : [ `Foo of 'a t | `Foo of _ s ] = id (`Foo []);;
val x : [ `Foo of '_weak24 list t ] = `Foo []

This particular case can be fixed by annotating the definition of t:

# type +'a t = 'a constraint 'a = 'b list;;
type +'a t = 'a constraint 'a = 'b list

However, in general this doesn't work because a parameter may contain multiple type variables of different variance. For example:

type 'a t = 'b -> 'c constraint 'a = 'b * 'c

I expect this is a known problem, and that there is no easy solution, but I thought it was worth reporting all the same.

@gasche

This comment has been minimized.

Copy link
Member

commented May 30, 2019

In the compute_variance_type function in typedecl_variance, we do compute variances for those "constrained parameters" (extra variables that do not occur in the parameter list, only in constraints). I think that it would make sense to consider the variance information of a type to be determined not by a variance for each of its apparent parameters (here 'a), but a variance for all non-constrainted parameters (here none) and for all constrainted parameters (here 'b, 'c) -- this corresponds to the tvl environment in that code. We could compute the most general variance for those parameters, and use that in the code.

I believe this makes sense because constraints cannot be hidden: an instance of the type that is not unifiable with the constraint is ill-formed and rejected at type-checking time. We can thus completely ignore the constrained parameters (here 'a) because they never occur rigidly in programs. This is important, because those constrained parameters do not have a most general variance -- this is exactly the point of your last example, where 'a can vary (it is better than invariant) but it is neither covariant nor contravariant. Its most general variance would be -b * +'c, if that was a thing.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented May 31, 2019

Actually, there is a more direct way to fix that: when variance information is required, one should expand types which have constrained parameters. Actually I think this is done in most cases, but apparently not when applying the relaxed value restriction (looks like I missed this interaction, thanks @lpw25 for pointing it).
What @gasche describes could be a useful optimization if the above appears to be costly.

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Jun 13, 2019

#8725 fixes the example I gave above, but variance information is used for more than just the relaxed value restriction, and these other places also have similar issues. For example:

# type 'a t = int constraint 'a = 'b list;;
type 'a t = int constraint 'a = 'b list

# type 'a s = int;;
type 'a s = int

# let f (o : < m : 'a . [ `Foo of 'a list t | `Foo of 'a list s ] >) : < m : 'b > = o;;
Characters 82-83:
  let f (o : < m : 'a . [ `Foo of 'a list t | `Foo of 'a list s ] >) : < m : 'b > = o;;
                                                                                    ^
Error: This expression has type < m : 'a. [ `Foo of 'a list t ] >
       but an expression was expected of type < m : 'b >
       The universal variable 'a would escape its scope

# let f (o : < m : 'a . [ `Foo of 'a list s | `Foo of 'a list t ] >) : < m : 'b > = o;;
val f : < m : 'a. [ `Foo of 'a list s ] > -> < m : [ `Foo of 'a list s ] > =
  <fun>
@garrigue

This comment has been minimized.

Copy link
Contributor

commented Jun 14, 2019

There are indeed two other occurrences: occur_univar and univars_escape.
However, the same fix doesn't seem to work, for a reason that looks like a bug: namely, expanding 'a list t inside occur_univar fails with a scoping error (it succeeds inside univars_escape).
I'll give it a better look later.

I'm starting to think that @gasche 's suggestion makes sense, at least computation costwise. However, it would involved rather extensive changes: add a list of free variables and their variances to type declarations, and modify variance inference to handle these.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Jun 14, 2019

After looking in more detail, the problem is deeper here: one cannot expand a type with a constrained parameter where the universal variable occurs deep inside this parameter.
It results in attempting the unification of 'x list with 'a list (with 'x fresh and 'a universal), which is not allowed (unifying 'x with 'a list is allowed through a trick).
This problem is there from the very beginning, and I never found a simple solution for that.
So yes, when universal variables are involved, there are some principality problems related to the representation of types, but fixing the problem with variance is not sufficient to fix all of them.
There doesn't seem to be a need to hurry too much about that.
Still, @gasche approach would at least solve your example, since it avoids having to expand the type in the first place.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Jun 14, 2019

But I forgot to mention a problem with @gasche approach: currently, the variances of types are not recomputed after functor applications. This means that they are not accurate, and in particular one has to expand types (even if there are no constrained parameters). So a prerequisite would be to implement the recomputation of variances after functor applications (or just compute them when adding types to the environment?)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.