You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
@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
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.
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.
The text was updated successfully, but these errors were encountered: