-
Notifications
You must be signed in to change notification settings - Fork 571
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
Conversation
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.
@kl0tl Can you verify that this fixes your issue? |
It works 🎉 |
I'm down to review this for approval, but I've no clue which one of the changes fixes this:
and which one of the changes fixes this:
@natefaubion can you provide some insight? |
The other but is replacing adhoc var generation with |
There was a problem hiding this 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 toreplaceTypeVariables
on the kinds for these generalized type variables, in the same way we are callingreplaceTypeVariables
on the type we are generalizing. This is why before we had an incorrect type likeforall k1 (k2 :: t87). Foo @k1 k2 Bar
, where t87 should have been substituted withk1
.
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
, withgeneralizeUnknowns
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 specificallyunknownVarNames
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?
This is very difficult to do in practice, and I think will either mean having more versions of
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 |
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