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

[github patch] warn user when a type variable in a type constraint has been instantiated #6313

Closed
vicuna opened this issue Feb 1, 2014 · 5 comments

Comments

@vicuna
Copy link

vicuna commented Feb 1, 2014

Original bug ID: 6313
Reporter: @gasche
Status: acknowledged (set by @damiendoligez on 2014-07-16T13:08:38Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.0+dev
Category: typing
Tags: patch

Bug description

Reported by Grégoire Henry:
#6
Patch is available at:
https://github.com/ocaml/ocaml/pull/6.patch

It seems to be a common misunderstanding amongst beginners that type
variables in type constraint are unification variables and that they
should be explicitly quantified when desired.

This small patch adds a warning when such non-quantified variable has
been instantiated by the type checker. The verification is made /a
posteriori/ by looking for type constraints in the typed tree.

I'm not sure this warning is really a desired feature, but it is
probably worth discussion. For instance, ocamlyacc-generated files use
such variables on purpose.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 13, 2020
@gasche
Copy link
Member

gasche commented May 13, 2020

This still sounds like an excellent idea to me. Would people that know about the type-check be able to tell whether the patch was correct and still makes sense? (cc @garrigue @lpw25 @trefis @let-def).

I think that if we wanted to gather consensus on this, we would need to ensure that people that use the feature for something else than instantiation have a way to avoid the warning. I believe that ... as 'a should obviously not warn, so _ as 'a is a correct but devious way to disable the warning, but I would rather ensure that '_a is supported by the parser, because it is obviously the right notation for not-necessarily-generalized unification variables.

@gasche gasche removed the Stale label May 13, 2020
@garrigue
Copy link
Contributor

Using '_a is rejected by the parse, as denoting a non-generalisable variable.
You suggest allowing that?
Note that since weak variables all start with '_weak it could make sense to remove this error (or restrict it to variable starting with '_weak).

@gasche
Copy link
Member

gasche commented May 13, 2020

We need a syntax for (1) a variable that may or may not be instantiated and generalizable (this is what people typically use 'a-as-sharing for), and a syntax for (2) a variable that may not be instantiated and is generalizable. I think the most natural is to use 'a for (2) and '_a for (1), so yes, this suggests allowing them in the parser, and also changing the semantics slightly (in general '_a would not mean "cannot be generalized" but "may not generalize"; of course when inference uses one, we know it actually could not generalized). But other syntaxes might be possible (eg. a for (2) ?).

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

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

3 participants