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

Correctly elide type annotations #66

Open
j-hui opened this issue Dec 29, 2021 · 3 comments
Open

Correctly elide type annotations #66

j-hui opened this issue Dec 29, 2021 · 3 comments
Labels
bug Something isn't working

Comments

@j-hui
Copy link
Contributor

j-hui commented Dec 29, 2021

If we write something like:

id (a: t) (b: t) -> t = b

This should be the same as writing:

id a b: t -> t -> t = b

That is, the type variable t across the annotations for a, b, and the return type should be quantified as the same name.

However, the lowering pass lowers these as three separate type annotations, which means they technically become separately quantified, since they reside in three separate type annotations.

I fear this kind of scoping might be tricky to get recover in the type-checking phase, so I should fix the lowering phase to collapse the three annotations into a single type annotation.

@XijiaoLi something to keep in mind while you work on type inference; to be safe, stick with the postfix type annotation syntax (using :) for now.

@j-hui j-hui added the bug Something isn't working label Dec 29, 2021
@sedwards-lab
Copy link
Contributor

Isn't that just a scope-of-type-variables issue? @j-hui doesn't your "scoping" pass go through and make all names globally unique by assigning them, say, a unique integer? The same thing should be done with type variables.

@j-hui
Copy link
Contributor Author

j-hui commented Dec 29, 2021

My scoping pass does not do that---it just checks that everything is scoped correctly. I can easily change it to name mangle the program but I haven't seen a need for that yet.

@j-hui
Copy link
Contributor Author

j-hui commented Aug 25, 2022

This is being handled in #103

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants