Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
vicuna opened this issue Jul 31, 2017 · 7 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Jul 31, 2017

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

@vicuna
Copy link
Author

vicuna commented Jul 31, 2017

Comment author: mandrykin

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

@vicuna
Copy link
Author

vicuna commented Aug 2, 2017

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
Copy link
Author

vicuna commented Aug 2, 2017

Comment author: @garrigue

Tentative fix: #1272

@vicuna
Copy link
Author

vicuna commented Aug 29, 2017

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
Copy link
Author

vicuna commented Sep 6, 2017

Comment author: @garrigue

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

@vicuna
Copy link
Author

vicuna commented Sep 6, 2017

Comment author: @garrigue

New tentative fix: #1320

@vicuna
Copy link
Author

vicuna commented Sep 12, 2017

Comment author: @garrigue

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants