It seems like a hidden non-generalized type variable remains in some inferred signatures, which leads to strange errors

[vicuna]

Original bug ID: 7601
Reporter: mandrykin
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-09-12T23:35:43Z)
Resolution: fixed
Priority: low
Severity: minor
Platform: x86_64
OS: Linux 4.4.0
OS Version: Ubuntu 16.04.2
Version: 4.05.0
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing

Bug description

The following fragment:

module type Analysis = sig
  type t
  type 'a maybe_region =
    [< `Location of t
    |  `Value of t
    |  `None ] as 'a
  val of_var : ?f:string -> string -> [ `Location of _ | `Value of _  | `None ] maybe_region
end

module Make (Analysis : Analysis) = struct
  include Analysis
  let of_var = of_var ~f:""
end

produces the following inclusion error:

At position module Make(Analysis) : <here>                                                                                                 Values do not match:                                                                                                                
         val of_var : string -> [ `Location of t | `None | `Value of t ]
       is not included in
         val of_var : string -> [ `Location of t | `None | `Value of t ]

(no observable difference in types and no visible type variables) (in 4.05.0)

However, if either generalization is requested for the value `of_var' using eta-expansion or a type annotation that does not involve the type maybe_region is added, the error disappears. So either of the following works:

module Make (Analysis : Analysis) = struct
  include Analysis
  let of_var x = of_var ~f:"" x
end

or

module Make (Analysis : Analysis) = struct
  include Analysis
  let of_var : _ -> [ `Location of _ | `None | `Value of _] = of_var ~f:"" 
end

but not

module Make (Analysis : Analysis) = struct
  include Analysis
  let of_var : _ -> [ `Location of _ | `None | `Value of _] maybe_region  = of_var ~f:"" 
end

Additional information

The types like [`A of _ | `B of _ | `C] t where 'a t = 'a constraint 'a = [`A of t1 | `B of t2 | `C of t3 | `D of ... | .... | `X of tn] are convenient for avoiding repeating the types of the polymorphic constructors if they are taken from some pre-defined set e.g. using
[`Location of _ | `None] maybe_region instead of
[`Location of U.t * [`None | `Value of U.t] | `None].

File attachments

• example.ml
• slice.ml

[vicuna]

Comment author: mandrykin

Added another more minimal example, the presence of an abstract type among the types of constructors does also matter.

[vicuna]

Comment author: @garrigue

Interesting. This bug is related to the change in 4.04, where locally defined abstract types cannot be used to instantiate non-generalizable type variables once the defining module is left.

First remark: there is an easy workaround, adding a variance annotation:

type +'a maybe_region = ...

I'm thinking of a fix that wouldn't break principality for this case.

[vicuna]

Comment author: @garrigue

Tentative fix: #1272

[vicuna]

Comment author: @garrigue

Fixed in 4.05 branch after 4.05.0 by #1272.

Note that the fix requires copying signatures, which seems to increase the size of cmi's when there is no mli.

[vicuna]

Comment author: @garrigue

Fix was breaking camomille and Frama-C. Reverted it.

[vicuna]

Comment author: @garrigue

New tentative fix: #1320

[vicuna]

Comment author: @garrigue

Fixed in trunk by commit ab7af2a, by replacing row variables of static variant types with Tnil.