Help getting PolyKinds over the line


Hi, everyone. I’ve been working on adding PolyKinds to the compiler. You can see the state of the branch here:

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 :laughing:. Thanks!


Super excited to say I’ve been able to make some more progress on this, and have overcome the instance issue above. It’s pretty cool to see things like a polykinded Row.Cons working!

module Test where

import Prim.Row as Row

data Proxy a = Proxy

class Functor f where
  map :: forall a b. (a -> b) -> f a -> f b

instance functorProxy :: Functor Proxy where
  map f Proxy = Proxy

data Id a = Id a

type Test = (a :: Id, b :: Proxy)

data Lookup a b

testLookup ::
  forall sym ty tail row.
  Row.Cons sym ty tail row =>
  Proxy (Lookup sym row) ->
  Proxy ty
testLookup _ = Proxy

test1 = testLookup (Proxy :: Proxy (Lookup "a" Test))
Warning found:
in module Test
at Test.purs:26:1 - 26:54 (line 26, column 1 - line 26, column 54)

  No type declaration was provided for the top-level declaration of test1.
  It is good practice to provide type declarations as a form of documentation.
  The inferred type of test1 was:

    Proxy Id

in value declaration test1

All tests are now green (except for breaking changes to externs)! There’s quite a few rough spots (errors still haven’t been fixed), but it can probably be tested in earnest now. You can do some pretty wild stuff. This cases on the kind of a type variable:

import Prelude

data Proxy a = Proxy

class NArgs t where
  nargs :: Proxy t -> Int

instance nargsFn :: NArgs b => NArgs (a -> b) where
  nargs _ = 1 + nargs (Proxy :: Proxy b)
else instance nargsVal :: NArgs a where
  nargs _ = 0

nargsKind :: forall k (a :: k). NArgs k => Proxy a -> Int
nargsKind _ = nargs (Proxy :: Proxy k)

test :: Int
test = nargsKind (Proxy :: Proxy Proxy)

What would help you at this moment in its development?


There isn’t a lot to help with at the moment, just a lot of cleanup.