|Anonymous | Login | Signup for a new account||2017-02-21 17:31 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006527||OCaml||OCaml typing||public||2014-08-30 00:52||2016-12-07 11:49|
|Target Version||4.02.2+dev / +rc1||Fixed in Version|
|Summary||0006527: constraints dropped on included signature|
|Description||It seems constraints are dropped when including a signature in the following way:|
OCaml version 4.01.0
# module type With_constraint = sig type 'a t constraint 'a = [> `Foo] end;;
module type With_constraint = sig type 'a t constraint 'a = [> `Foo ] end
# module type S = sig type 'a t include With_constraint with type 'a t := 'a t end;;
module type S = sig type 'a t end
This surprised me, since the constraint doesn't get dropped if there's a constraint on the type already defined in S:
# module type S' = sig type 'a t constraint 'a = [> `Bar] include With_constraint with type 'a t := 'a t end;;
Error: In this `with' constraint, the new definition of t
does not match its original definition in the constrained signature:
Type declarations do not match:
type 'a t = 'a t constraint 'a = [> `Bar | `Foo ]
is not included in
type 'a t constraint 'a = [> `Foo ]
Their constraints differ.
|Tags||No tags attached.|
This behaviour is probably the correct approach for handling this situation, as I think it is the most flexible sound approach.
For a module type like:
module type S = sig type 'a t constraint 'a = [> `Foo] end
You can think of
S with type 'a t := 'a s
as meaning "S with all occurrences of [> `Foo] t replaced by [> `Foo] s".
This operation works if "[> `Foo] s" is a valid type (e.g. your first example), and fails if "[> `Foo] s" is not a valid type (e.g. your second example).
It may appear that [> `Foo] s is valid in your second example, but really if you write [> `Foo] s you actually get [> `Foo | `Bar] s instead -- it is not possible to have precisely [> `Foo] s.
Also note that the only alternative is to have:
> module type With_constraint = sig type 'a t constraint 'a = [> `Foo] end;;
> module type S = sig type 'a t include With_constraint with type 'a t := 'a t end;;
result in an error.
It would not be safe to have the include of With_constraint retroactively change the definition of the type t to add constraints.
|2014-08-30 00:52||mkoconnor||New Issue|
|2014-09-15 15:22||doligez||Status||new => acknowledged|
|2014-09-15 15:22||doligez||Target Version||=> 4.02.2+dev / +rc1|
|2015-05-05 18:21||lpw25||Note Added: 0013813|
|2015-05-05 18:23||lpw25||Note Added: 0013814|
|2015-05-05 18:40||lpw25||Status||acknowledged => resolved|
|2015-05-05 18:40||lpw25||Resolution||open => won't fix|
|2015-05-05 18:40||lpw25||Assigned To||=> lpw25|
|2016-12-07 11:49||xleroy||Status||resolved => closed|
|Copyright © 2000 - 2011 MantisBT Group|