Recursive modules do not correctly handle variance #6492
Description
Original bug ID: 6492
Reporter: @lpw25
Status: acknowledged (set by @damiendoligez on 2014-07-30T20:39:06Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Tags: recmod
Related to: #5984
Bug description
Variance 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>