Skip to content

Fix substitution during kind generalization #3831

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

Merged
merged 1 commit into from
Apr 5, 2020

Conversation

natefaubion
Copy link
Contributor

We were not applying the substitution for generalized kinds to their own
kinds, which can result in unknowns sticking around in a generalized
kind.

I've also fixed an issue wrt to hygiene in kind declarations, where
the names for generalized kinds were not using the usual name generation
scheme.

Fixes #3830

We were not applying the substitution for generalized kinds to their own
kinds, which can result in unknowns sticking around in a generalized
kind.

I've also fixed an issue wrt to hygiene in kind declarations, where
the names for generalized kinds were not using the usual name generation
scheme.
@natefaubion
Copy link
Contributor Author

@kl0tl Can you verify that this fixes your issue?

@kl0tl
Copy link
Member

kl0tl commented Apr 5, 2020

It works 🎉

@joneshf
Copy link
Member

joneshf commented Apr 5, 2020

I'm down to review this for approval, but I've no clue which one of the changes fixes this:

We were not applying the substitution for generalized kinds to their own
kinds, which can result in unknowns sticking around in a generalized
kind.

and which one of the changes fixes this:

I've also fixed an issue wrt to hygiene in kind declarations, where
the names for generalized kinds were not using the usual name generation
scheme.

@natefaubion can you provide some insight?

@natefaubion
Copy link
Contributor Author

natefaubion commented Apr 5, 2020

generalizeUnknownsWithVars is what performs the actual substitution and introduces a forall. It replaces unknowns with a type variable, given a substitution context mapping these unknowns to the type variable. I inserted a call to replaceTypeVariables on the kinds for these generalized type variables, in the same way we are calling replaceTypeVariables on the type we are generalizing. This is why before we had an incorrect type like forall k1 (k2 :: t87). Foo @k1 k2 Bar, where t87 should have been substituted with k1.

The other but is replacing adhoc var generation with freshVar, with generalizeUnknowns which is what is used everywhere else. Our unique identifier generation isn't very unique in practice, and this was generating a name that clashed with another name. generalizeUnknowns, and more specifically unknownVarNames which it calls, makes sure that the names it picks for vars don't clash with any vars mentioned in the type.

Copy link
Member

@joneshf joneshf left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great. Thanks for explaining!

Couple of comments/questions that are non-blocking. Merge it up!

generalizeUnknownsWithVars is what performs the actual substitution and introduces a forall. It replaces unknowns with a type variable, given a substitution context mapping these unknowns to the type variable. I inserted a call to replaceTypeVariables on the kinds for these generalized type variables, in the same way we are calling replaceTypeVariables on the type we are generalizing. This is why before we had an incorrect type like forall k1 (k2 :: t87). Foo @k1 k2 Bar, where t87 should have been substituted with k1.

This seems like the sort of thing we should change the type of. It seems likely there's other bugs like the one you just fixed sitting around that would be sussed out with a type change.

I recognize this is a huge change, so not recommending we do it in this PR.

The other but is replacing adhoc var generation with freshType, with generalizeUnknowns which is what is used everywhere else. Our unique identifier generation isn't very unique in practice, and this was generating a name that clashed with another name. generalizeUnknowns, and more specifically unknownVarNames which it calls, makes sure that the names it picks for vars don't clash with any vars mentioned in the type.

Is generation not working correctly because some of Language.PureScript.TypeChecker.Kinds uses Control.Monad.Supply.Class.MonadSupply _ and some of it is processing values explicitly? If so, what about using one approach everywhere?

@natefaubion
Copy link
Contributor Author

natefaubion commented Apr 5, 2020

This seems like the sort of thing we should change the type of. It seems likely there's other bugs like the one you just fixed sitting around that would be sussed out with a type change.

This is very difficult to do in practice, and I think will either mean having more versions of Type around, or introducing more type variables or GADT like constructions. This amounts to a fully type/phase safe AST and is a larger problem than just this.

Is generation not working correctly because some of Language.PureScript.TypeChecker.Kinds uses Control.Monad.Supply.Class.MonadSupply _ and some of it is processing values explicitly? If so, what about using one approach everywhere?

There's nothing wrong with unique generation per se, it's just that it's not very unique. It's just getting a new monotonically increasing int. If you happen to invoke it early on, then they will be small numbers, which are more likely to be written by users. None of our name generation schemes are fully hygienic. For example, when we generalize an unannotated top-level declaration, we just use the TUnknown integer and prefix it with t. I think the more general solution to this is using something other than Text for Forall vars that better preserves it's purpose and origin (kind of like Ident). This is a very large change, however.

@natefaubion natefaubion merged commit 0aaa490 into purescript:master Apr 5, 2020
@natefaubion natefaubion deleted the fix-3830 branch April 5, 2020 19:31
@joneshf joneshf mentioned this pull request May 23, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Unsolved unification variable with polykinds
3 participants