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.

Sign up for GitHub

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

Jump to bottom

Automatically generate bidirectional hints #11066

Open
SkySkimmer opened this issue Nov 7, 2019 · 4 comments
Open

Automatically generate bidirectional hints #11066

SkySkimmer opened this issue Nov 7, 2019 · 4 comments
Labels
kind: design discussion Discussion about the design of a feature. kind: wish Feature or enhancement requests. part: records Record types, Structures, etc.

Comments

@SkySkimmer
Copy link
Contributor

The bidi hints introduced in #10049 are IIUC expected to be useful when applying constructors like existT. Can we automatically generate them for such constructors?

I guess the simplest case is a record, where we would put the bidi hint between the parameters and the real arguments.
@gares
Copy link
Member

gares commented Nov 11, 2019

It works for all indicatives with parameters, not just unary ones.

@Alizter Alizter added kind: design discussion Discussion about the design of a feature. kind: wish Feature or enhancement requests. part: records Record types, Structures, etc. labels Sep 29, 2021
@JasonGross JasonGross mentioned this issue May 3, 2023
Closed
@JasonGross
Copy link
Member

Suggestion from #11702: call the flag either Set Automatic Bidi Constructors or Set Automatic Bidirectional Constructors

@SkySkimmer
Copy link
Contributor Author

See also #15548

@JasonGross
Copy link
Member

I'd still like to see a flag for turning on automatic bidi hints. Even if there's not much hope for compatibility in general, it'd still be quite useful to be able to set a flag to turn on the heuristic. Can #15548 be revived in the form of a flag that is not set by default?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: design discussion Discussion about the design of a feature. kind: wish Feature or enhancement requests. part: records Record types, Structures, etc.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@JasonGross @gares @SkySkimmer @Alizter