Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006492OCamlOCaml typingpublic2014-07-19 13:062014-09-15 16:14
Reporterlpw25 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target Version4.02.2+devFixed 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

-  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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker