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

Type constraints using module types not general enough #6953

Closed
vicuna opened this issue Aug 5, 2015 · 3 comments
Closed

Type constraints using module types not general enough #6953

vicuna opened this issue Aug 5, 2015 · 3 comments

Comments

@vicuna
Copy link

vicuna commented Aug 5, 2015

Original bug ID: 6953
Reporter: @mmottl
Status: closed (set by @xavierleroy on 2017-02-16T14:16:36Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.02.3
Category: typing
Monitored by: @hcarty @mmottl

Bug description

Consider the following code snippet:

--
module type Types = sig type x type y end

module type S = sig
type 'a t constraint 'a = (module Types with type x = 'x and type y = 'y)
(* type 'a t constraint 'a = (module Types) *)
end

module M : S = struct
type 'a t = 'x * 'y
constraint 'a = (module Types with type x = 'x and type y = 'y)
end

It will compile just fine. But if we swap the type definitions for type t in module type S, the compiler will complain that module M is not an instance of module type S anymore. This doesn't quite seem right, because whether or not I bind the types x and y to variables should make no difference if there are no constraints on these variables.

@vicuna
Copy link
Author

vicuna commented Aug 5, 2015

Comment author: @sliquister

The error looks right to me. The type x is quantified universally in the first type, but existentially in the second one. If you build a list of ts, with the first definition of t, the types x are the same, with the second definition of t, they can vary.

@vicuna
Copy link
Author

vicuna commented Aug 6, 2015

Comment author: @mmottl

@sliquister: I think you are right. 'x and 'y receive their universal quantification via 'a. It obviously pays to check dependencies between several type variables more carefully. 'x and 'y almost seem like superfluous bindings in this context, but they don't just bind the type in the modules, they also propagate it out through 'a. That's not the same as in e.g.: type 'a t = int as 'b

@vicuna
Copy link
Author

vicuna commented Nov 24, 2015

Comment author: @xavierleroy

This is a tough example! I agree with user sliquister that the behavior of the typechecker is probably right here, if not intuitive. Marking this PR as resolved.

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

1 participant