Original bug ID: 5984
Reporter: @yallop
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2017-03-15T05:58:24Z)
Resolution: won't fix
Priority: normal
Severity: feature
Target version: later
Category: typing
Related to: #2696 #6492 #7212
Parent of: #5985 #7321
Monitored by: @lpw25

Bug description

Type constructors that pass transparently through functors lose certain variance information along the way. For example, the following program

   module F(S : sig type 'a t end) = S

   module N : sig type +'a t end = F(struct type 'a t = 'a list end) 

is rejected with this error:

   Error: Signature mismatch:
       Modules do not match:
         sig type 'a t = 'a list end
       is not included in
         sig type +'a t end
       Type declarations do not match:
         type 'a t = 'a list
       is not included in
         type +'a t
       Their variances do not agree.

However, despite this error, the type that results from the functor application is actually marked as covariant, as illustrated by the fact that the following program is accepted:

  module F(S : sig type 'a t end) = S

  module N = F(struct type 'a t = 'a list end) 

  let f (x : [`A] N.t) = (x :> [`A | `B] N.t)