Hi, everyone. I’ve been working on adding PolyKinds to the compiler. You can see the state of the branch here: https://github.com/natefaubion/purescript/tree/polykinds
Overall it is in a good state. This branch implements
TypeInType, and will infer and check against polymorphic data types like:
data Proxy a = Proxy
Proxy :: forall (k :: Type). k -> Type
This of course is desirable because it lets us eliminate the zoo of proxy types we have, and will also let us use Row constraints with things other than
Type. This also fixes existing bugs in the kind checker, where it is not checking things when it should.
I haven’t been able to take this over the line yet due to life circumstances, and there are a few big things left to take care of.
One big issue remaining is dealing with classes and instances for polykinded data types. If you take
Proxy as an example, it has
Functor instances. However, due to the signatures of the class members, the instance is actually for
Proxy @Type. Currently, elaborated kinds like this are not directly available to the solver, so it will fail to find this instance. It’s not clear to me if I can hydrate these elaborated type from the desugared class and instance declarations, or if we definitely need to kind elaborate the source class and instance declarations and put that in the environment. This requires some investigative work, and potentially extending the kind checker for these other forms.
Error reporting needs to be cleaned up in the kind checker. Right now there are still quite a bit of
internalError placeholders, and they should be replaced with actual errors. We also need to insert more type checking hints in the log, so you can get a good stack trace in any errors.
We need to extend the type declaration syntax to support full kind signatures (like
foreign import data but for regular data types as well), and adjust the checker accordingly (this is a topo-sort issue).
We need to potentially extend externs with this information. I have not fully investigated what the effects would be.
We need to benchmark the compiler to see if there’s anything we need to tune. I would like for this to not regress considerably in performance.
If anyone is interested in seeing this feature land and would like to help out, I can offer guidance. If not, then it might just take a little while . Thanks!