0005926: tag-spec-full documentation seems to be incorrect

(0008873)
lpw25 (developer)
2013-02-19 18:33
edited on: 2013-02-20 16:19

I think that the documentation should probably be something like:

tag-spec-full ::= `tag-name [ of [ typexpr ] { & typexpr } ]

A "correct" (although non-sensical) example would be:

type 'a z = [< `c of int & float] as 'a;;

I'm not sure, but I think that some of your examples may actually be failing because of a bug in the type-checker. The type [< `Tag of & t ] means that `Tag (if it exists) is both a constant and has an argument of type t. Since it is basically impossible to actually use such a type for anything it wouldn't surprise me if there were some bugs in how they were type-checked.

(0008874)
hongboz (developer)
2013-02-19 18:44
edited on: 2013-02-19 18:45

leo, thanks! I am exploiting some sophisticated usage of polymorphic variants. It would be nice the detailed behavior is documented

(0008876)
lpw25 (developer)
2013-02-19 20:01
edited on: 2013-02-19 20:02

I've submitted a bug report (0005927) and patch for those examples that I think are failing due to a bug.

(0008879)
garrigue (manager)
2013-02-20 07:34

I've fixed the grammar in the manual.
I've also added a comment that unsolvable constraints may fail when given as input to the compiler.
Basically, you are describing an impossible type, so there is no good reason to accept it, and doing so may be complicated.

(0008884)
hongboz (developer)
2013-02-20 15:27

I can make a working example now
# type 'a z = [< `c of int & int ] as 'a;;
type 'a z = 'a constraint 'a = [< `c of int ]
# let u : 'a z = `c 3 ;;
val u : [ `c of int ] z = `c 3

But I do not get a working example for 'of &' directly

Did I miss something? thanks,

# type 'a v = [< `c ] as 'a;;
type 'a v = 'a constraint 'a = [< `c ]
# type 'a z = [< `c of & 'a v ] as 'a ;;
Characters 12-36:
type 'a z = [< `c of & 'a v ] as 'a ;;
^^^^^^^^^^^^^^^^^^^^^^^^
Error: Constraints are not satisfied in this type.

(0008885)
garrigue (manager)
2013-02-20 16:10

I'm not sure what you are trying to do.
The point is that constructors of the form "of & int" are by definition unusable.
So there is no real point in making efforts to allow them.
But maybe you have some specific goal.
However, as a general suggestion, I think that if you want to hack with types,
GADTs are going to be more rewarding. Polymorphic variants have many
nice applications, but type inference creates some limitations.

(0008886)
hongboz (developer)
2013-02-20 16:17

garrigue, I found some bugs in camlp4 when handling polymorphic variants, so I want to make sure that I understand every corner case of variants before I try to fix it.
I am not hacking types, thanks for your response.

Notes
(0008873) lpw25 (developer) 2013-02-19 18:33 edited on: 2013-02-20 16:19	I think that the documentation should probably be something like: tag-spec-full ::= `tag-name [ of [ typexpr ] { & typexpr } ] A "correct" (although non-sensical) example would be: type 'a z = [< `c of int & float] as 'a;; I'm not sure, but I think that some of your examples may actually be failing because of a bug in the type-checker. The type [< `Tag of & t ] means that `Tag (if it exists) is both a constant and has an argument of type t. Since it is basically impossible to actually use such a type for anything it wouldn't surprise me if there were some bugs in how they were type-checked.

(0008874) hongboz (developer) 2013-02-19 18:44 edited on: 2013-02-19 18:45	leo, thanks! I am exploiting some sophisticated usage of polymorphic variants. It would be nice the detailed behavior is documented

(0008876) lpw25 (developer) 2013-02-19 20:01 edited on: 2013-02-19 20:02	I've submitted a bug report (0005927) and patch for those examples that I think are failing due to a bug.

(0008879) garrigue (manager) 2013-02-20 07:34	I've fixed the grammar in the manual. I've also added a comment that unsolvable constraints may fail when given as input to the compiler. Basically, you are describing an impossible type, so there is no good reason to accept it, and doing so may be complicated.

(0008884) hongboz (developer) 2013-02-20 15:27	I can make a working example now # type 'a z = [< `c of int & int ] as 'a;; type 'a z = 'a constraint 'a = [< `c of int ] # let u : 'a z = `c 3 ;; val u : [ `c of int ] z = `c 3 But I do not get a working example for 'of &' directly Did I miss something? thanks, # type 'a v = [< `c ] as 'a;; type 'a v = 'a constraint 'a = [< `c ] # type 'a z = [< `c of & 'a v ] as 'a ;; Characters 12-36: type 'a z = [< `c of & 'a v ] as 'a ;; ^^^^^^^^^^^^^^^^^^^^^^^^ Error: Constraints are not satisfied in this type.

(0008885) garrigue (manager) 2013-02-20 16:10	I'm not sure what you are trying to do. The point is that constructors of the form "of & int" are by definition unusable. So there is no real point in making efforts to allow them. But maybe you have some specific goal. However, as a general suggestion, I think that if you want to hack with types, GADTs are going to be more rewarding. Polymorphic variants have many nice applications, but type inference creates some limitations.

(0008886) hongboz (developer) 2013-02-20 16:17	garrigue, I found some bugs in camlp4 when handling polymorphic variants, so I want to make sure that I understand every corner case of variants before I try to fix it. I am not hacking types, thanks for your response.

Issue History
Date Modified	Username	Field	Change
2013-02-19 15:57	hongboz	New Issue
2013-02-19 18:33	lpw25	Note Added: 0008873
2013-02-19 18:44	hongboz	Note Added: 0008874
2013-02-19 18:45	hongboz	Note Edited: 0008874	View Revisions
2013-02-19 20:01	lpw25	Note Added: 0008876
2013-02-19 20:02	lpw25	Note Edited: 0008876	View Revisions
2013-02-20 07:34	garrigue	Note Added: 0008879
2013-02-20 07:34	garrigue	Status	new => resolved
2013-02-20 07:34	garrigue	Fixed in Version	=> 4.01.0+dev
2013-02-20 07:34	garrigue	Resolution	open => fixed
2013-02-20 07:34	garrigue	Assigned To	=> garrigue
2013-02-20 15:27	hongboz	Note Added: 0008884
2013-02-20 16:10	garrigue	Note Added: 0008885
2013-02-20 16:17	hongboz	Note Added: 0008886
2013-02-20 16:19	lpw25	Note Edited: 0008873	View Revisions

Relationships