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

tag-spec-full documentation seems to be incorrect #5926

Closed
vicuna opened this issue Feb 19, 2013 · 7 comments
Closed

tag-spec-full documentation seems to be incorrect #5926

vicuna opened this issue Feb 19, 2013 · 7 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Feb 19, 2013

Original bug ID: 5926
Reporter: @bobzhang
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:31Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.01.0+dev
Category: documentation

Bug description

tag-spec-full is documented as follows:
tag-spec-full ::= `tag-name [ of typexpr ] { & typexpr }

It seems that `tag-name {& expr} will result in a syntax error.
Is there any documentation explaining how conjuctive types work?
I did not get a working example yet.
Thanks

type 'a z = [< `c & u2] as 'a;;

Error: Syntax error

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

Error: Type declarations do not match:
type 'a z = 'a constraint 'a = [< c of & u2 ] is not included in type 'a z = 'a constraint 'a = [< c of & u2 ]

type 'a u3 = [< b | a of & int & bool & int ] as 'a;;

Error: Type declarations do not match:
type 'a u3 = 'a constraint 'a = [< a of & int & bool | b ]
is not included in
type 'a u3 = 'a constraint 'a = [< a of & int & bool | b ]

type 'a u3 = [< b | a of & int & int ] as 'a;;

Error: Type declarations do not match:
type 'a u3 = 'a constraint 'a = [< a of & int | b ]
is not included in
type 'a u3 = 'a constraint 'a = [< a of & int | b ]

@vicuna
Copy link
Author

vicuna commented Feb 19, 2013

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Feb 19, 2013

Comment author: @bobzhang

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

@vicuna
Copy link
Author

vicuna commented Feb 19, 2013

Comment author: @lpw25

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

@vicuna
Copy link
Author

vicuna commented Feb 20, 2013

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Feb 20, 2013

Comment author: @bobzhang

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.

@vicuna
Copy link
Author

vicuna commented Feb 20, 2013

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Feb 20, 2013

Comment author: @bobzhang

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.

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