Anonymous | Login | Signup for a new account 2017-10-20 20:01 CEST
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006492OCamltypingpublic2014-07-19 13:062017-03-15 06:57
Reporterlpw25
Assigned To
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen
PlatformOSOS Version
Product Version
Target VersionlaterFixed in Version
Summary0006492: Recursive modules do not correctly handle variance
DescriptionVariance calculation is done by looking up the variance of any used type constructors in the environment. When types in recursive modules depend on each other, the variance information only travels through one level of indirection.

For example, `Bar.t` is covariant but `Baz.t` is invariant in the following example:

# module rec Foo : sig type 'a t = Foo of 'a end = Foo
and Bar : sig type 'a t = Bar of 'a Foo.t end = Bar
and Baz : sig type 'a t = Baz of 'a Bar.t end = Baz;;
module rec Foo : sig type 'a t = Foo of 'a end
and Bar : sig type 'a t = Bar of 'a Foo.t end
and Baz : sig type 'a t = Baz of 'a Bar.t end

# let f x = (x : <m:int> Bar.t :> < > Bar.t);;
val f : < m : int > Bar.t -> < > Bar.t = <fun>

# let f x = (x : <m:int> Baz.t :> < > Baz.t);;
Characters 10-42:
let f x = (x : <m:int> Baz.t :> < > Baz.t);;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Type < m : int > Baz.t is not a subtype of < > Baz.t
The second object type has no method m

whereas if the types had been defined recursively then `baz` would be covariant:

# type 'a foo = Foo of 'a
and 'a bar = Bar of 'a foo
and 'a baz = Baz of 'a baz;;
type 'a foo = Foo of 'a
and 'a bar = Bar of 'a foo
and 'a baz = Baz of 'a baz

# let f x = (x : <m:int> baz :> < > baz);;
val f : < m : int > baz -> < > baz = <fun>

Variance calculation is also overly conservative when using approximate type definitions from `approx_type_decl`, which means that variance annotations can lead to spurious errors. For example:

# module rec Foo : sig type +'a t end = Foo
and Bar : sig type +'a t = Bar of 'a Foo.t end = Bar;;
Characters 63-86:
and Bar : sig type +'a t = Bar of 'a Foo.t end = Bar;;
^^^^^^^^^^^^^^^^^^^^^^^
Error: In this definition, expected parameter variances are not satisfied.
The 1st type parameter was expected to be covariant,
but it is injective invariant.

If the covariance annotation is removed from `Bar.t` then there is no error, and `Bar.t` is considered covariant:

# module rec Foo : sig type +'a t end = Foo
and Bar : sig type 'a t = Bar of 'a Foo.t end = Bar;;
module rec Foo : sig type +'a t end
and Bar : sig type 'a t = Bar of 'a Foo.t end

# let f x = (x : <m:int> Bar.t :> < > Bar.t);;
val f : < m : int > Bar.t -> < > Bar.t = <fun>
Tagsrecmod
Attached Files

Relationships
 related to 0005984 confirmed garrigue Variance information is not properly propagated through functor applications

 Notes There are no notes attached to this issue.

 Issue History Date Modified Username Field Change 2014-07-19 13:06 lpw25 New Issue 2014-07-30 13:41 doligez Tag Attached: recmod 2014-07-30 22:39 doligez Status new => acknowledged 2014-07-30 22:39 doligez Target Version => 4.02.1+dev 2014-09-04 00:25 doligez Target Version 4.02.1+dev => undecided 2014-09-15 16:14 doligez Target Version undecided => 4.02.2+dev / +rc1 2015-01-20 22:04 doligez Target Version 4.02.2+dev / +rc1 => 4.03.0+dev / +beta1 2016-04-06 13:55 doligez Target Version 4.03.0+dev / +beta1 => later 2017-02-23 16:45 doligez Category OCaml typing => typing 2017-03-15 06:57 garrigue Relationship added related to 0005984 2017-03-15 06:57 garrigue Severity minor => feature