Help getting PolyKinds over the line

language
#1

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

19 Likes
#2

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
13 Likes
#3

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)
11 Likes
#4

What would help you at this moment in its development?

#5

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

#6

There is now a PR up with remaining tasks: https://github.com/purescript/purescript/pull/3779

7 Likes
#7

Nate’s PR now builds. Among the core libraries, only prelude and typelevel-prelude had to be updated. I think all the error messages have been fixed now.

For those who aren’t watching that PR, I’ve created a cheatsheet of my understanding of some of the changes to the syntax. I’m sure Nate will provide a better and more accurate explanation when 0.14 is released, but I’m linking to it here in the meantime:

Lastly, I think the general consensus about how to update the ecosystem’s libraries is to make two breaking changes. The first breaking change will make the library compilable on the new PS release when it gets released, but won’t fully utilize all the new possibilities via PolyKinds. The second breaking change will utilize the PolyKinds feature to do new things.

3 Likes
#8

To be more specific, we are probably going to keep the zoo of proxy types (but deprecate them) to avoid churn and change function signatures to take proxy type variables instead

foo :: forall sym. SProxy sym -> ...
foo :: forall sproxy sym. sproxy sym -> ...

This will let you pass in any proxy type you want. So existing code that uses SProxy will work, but you can also use a polykinded Proxy as well.

1 Like
#9

As a way to validate/test Nate’s PR, I’m using a fork of the purescript language repo here that is using a recent version of the package set to compile most of the ecosystem: https://github.com/JordanMartinez/purescript/tree/useSpagoForSupport

As suggested by Nate, I’ll be using this thread to post error messages I get along the way, so that we don’t spam his PR. I apologize in advance if this ends up spamming this thread!

1 Like
#10

Latest output of stack test via d98c1a15:

~/Programming/Git Projects/purescript$ stack test
purescript> test (suite: tests)


###############################################################################
# Updating support code
###############################################################################

audited 110 packages in 0.824s

1 package is looking for funding
  run `npm fund` for details

found 0 vulnerabilities

[info] Installation complete.
tests: user error (Error 1 of 9:

  in module Data.Struct.Utils.Record
  at /home/jordan/Programming/Git Projects/purescript/tests/support/.spago/struct/v1.1.0/src/Utils/Record/Utils.purs:19:17 - 19:44 (line 19, column 17 - line 19, column 44)

    No type class instance was found for
                               
      Prim.Row.Lacks l4        
                     (() @Type)
                               

  while applying a function insert
    of type IsSymbol t0 => Lacks @Type t0 t1 => Cons @Type t0 t2 t1 t3 => SProxy t0 -> t2 -> Record t1 -> Record t3
    to argument SProxy
  while inferring the type of insert SProxy
  in value declaration singleton

  where l4 is a rigid type variable
          bound at (line 0, column 0 - line 0, column 0)
        t1 is an unknown type
        t3 is an unknown type
        t0 is an unknown type
        t2 is an unknown type

  See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
  or to contribute content related to this error.

Error 2 of 9:

  in module Formless.Internal.Transform
  at .:0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Unknown type Prim.Row.Cons$Dict

  while inferring the kind of Cons$Dict s t r r'
  while checking that type Cons$Dict s t r r'
    has kind Type
  while inferring the kind of Record () -> Cons$Dict s t r r'
  while inferring the kind of ( "Cons0" :: Record () -> Cons$Dict s t r r'
                              , "Lacks1" :: Record () -> Lacks$Dict s r   
                              )                                           
  while inferring the kind of { "Cons0" :: Record () -> Cons$Dict s t r r'
                              , "Lacks1" :: Record () -> Lacks$Dict s r   
                              }                                           
  in type synonym Row1Cons$Dict

  See https://github.com/purescript/documentation/blob/master/errors/UnknownName.md for more information,
  or to contribute content related to this error.

Error 3 of 9:

  in module Formless.Types.Component
  at /home/jordan/Programming/Git Projects/purescript/tests/support/.spago/halogen-formless/v1.0.0-rc.1/src/Formless/Types/Component.purs:81:1 - 86:44 (line 81, column 1 - line 86, column 44)

    Type synonym Formless.Types.Component.PublicAction is partially applied.
    Type synonyms must be applied to all of their type arguments.

  in data constructor AsQuery
  in type constructor QueryF

  See https://github.com/purescript/documentation/blob/master/errors/PartiallyAppliedSynonym.md for more information,
  or to contribute content related to this error.

Error 4 of 9:

  in module Freedom.VNode
  at .:0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      forall (f :: Type -> Type -> Type) (state :: Type). Ref (Ref ...) -> BridgeFoot f state

    where t52 is an unknown kind.
    where t55 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group VObject, Operations, BridgeFoot, VNode, VElement, VRender, VRenderEnv

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 5 of 9:

  in module Halogen.VDom.Driver
  at .:0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      RenderState @t42 @t45

    where t42 is an unknown kind.
    where t45 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group ChildRenderer, RenderState

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 6 of 9:

  in module Options.Applicative.Types
  at .:0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      forall (a :: Type). Option @t60 a -> Parser a

    where t60 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group ParserInfo, Parser, Option, OptReader, CReader, ReadM, ParseError, SomeParser, MultPE

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 7 of 9:

  in module Pathy.Phantom
  at /home/jordan/Programming/Git Projects/purescript/tests/support/.spago/pathy/v7.0.1/src/Pathy/Phantom.purs:21:8 - 25:9 (line 21, column 8 - line 25, column 9)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      forall (f :: RelOrAbs -> t31 -> Type) (b :: t31) (r :: Type). ((... -> ...) -> ... -> r) -> (... -> ...) -> ... -> r

    where t31 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in type synonym IsRelOrAbs$Dict

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 8 of 9:

  in module Polyform.Field.Generic
  at /home/jordan/Programming/Git Projects/purescript/tests/support/.spago/polyform/v0.8.0/src/Polyform/Field/Generic.purs:93:17 - 93:29 (line 93, column 17 - line 93, column 29)

    No type class instance was found for
                               
      Prim.Row.Lacks name4     
                     (() @Type)
                               

  while applying a function insert
    of type IsSymbol t0 => Lacks @Type t0 t1 => Cons @Type t0 t2 t1 t3 => SProxy t0 -> t2 -> Record t1 -> Record t3
    to argument _name
  while inferring the type of insert _name
  in value declaration multiChoiceConstructor

  where name4 is a rigid type variable
          bound at (line 0, column 0 - line 0, column 0)
        t1 is an unknown type
        t3 is an unknown type
        t0 is an unknown type
        t2 is an unknown type

  See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
  or to contribute content related to this error.

Error 9 of 9:

  in module Record.Extra
  at /home/jordan/Programming/Git Projects/purescript/tests/support/.spago/record-extra/v3.0.1/src/Record/Extra.purs:209:8 - 209:28 (line 209, column 8 - line 209, column 28)

    No type class instance was found for
                               
      Prim.Row.Lacks name6     
                     (() @Type)
                               

  while applying a function insert
    of type Cons @Type t2 t3 t4 t5 => Lacks @Type t2 t4 => IsSymbol t2 => SProxy t2 -> t3 -> Builder (Record t4) (Record t5)
    to argument namep
  while checking that expression insert namep
    has type t0 -> t1
  in value declaration sequenceRecordSingle

  where name6 is a rigid type variable
          bound at (line 0, column 0 - line 0, column 0)
        t0 is an unknown type
        t1 is an unknown type
        t2 is an unknown type
        t3 is an unknown type
        t4 is an unknown type
        t5 is an unknown type

  See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
  or to contribute content related to this error.

)

purescript> Test suite tests failed
Test suite failure for package purescript-0.13.6
    tests:  exited with: ExitFailure 1
Logs printed to console
#12

I think for many “Cannot unambiguously generalize” errors, we should look at the declarations of these types. Something like Option is very unlikely to be polykinded, however it probably has an opaque representation defined with an empty data decl, and uses unsafeCoerce which is not correct. These should be foreign import data and have a kind signature.

-- This will be polykinded, since it is phantom
data Option a

-- It should be
foreign import data Option :: Type -> Type

I think Halogen is one particular egregious offender of this for it’s existential encodings :laughing:

The Cons$Dict errors are because classes are declaring Cons to be a superclass, and the Prim classes do not have a dictionary type alias (they should).

The Lacks error is suspicious. It has a polykinded signature in the environment, but it’s very strange that it’s only really this class that is having issues. It seemed like it wasn’t getting kind-applied, so maybe there is just an error in the solver which isn’t propagating the kind application.

#13

Is there an intuitive way to think about what “Cannot unambiguously generalize kinds” means?

#14

Yes, but I’m willing to take suggestions. Kinds can only be unambiguously generalized in the type of a declaration.

data Proxy a = Proxy

someProxy :: forall a. Proxy a
someProxy = Proxy

It is always safe to automatically generalize this to

someProxy :: forall k (a :: k). Proxy a
someProxy = Proxy

Since this is the only possible way to do so. Note that this is only in top level declarations. Let-should-not-be-generalized still applies here. However with:

type SomeProxy = forall a. Proxy a

someProxy :: SomeProxy
someProxy = Proxy

It is not the case I can generalize the RHS of the type synonym. For one, it’s not the case that a forall is always involved, so it may not even be of kind Type. But also someone could easily use this synonym in a rank-n position, which would result in likely unintended consequences. One option is to add the forall k (a :: k)., but one might also actually want to do:

type SomeProxy k = forall (a :: k). Proxy a

someProxy :: forall k. SomeProxy k
someProxy = Proxy

This probably happens most commonly though in record synonyms with polymorphic fields. Unfortunately, since typeclass desugaring happens before kind-checking, class members might need kind signatures (this tripped up IxDiscard). I think it’s safe to generalize these unambiguously, but can’t due to the (unkinded) record synonym for dictionaries. Another example is in data types:

data SomeProxy = SomeProxy (forall a. Proxy a)

If you take a signature for this constructor:

SomeProxy :: (forall a. Proxy a) -> SomeProxy

It might be possible to say it could generalize to:

SomeProxy :: forall k. (forall (a :: k). Proxy a) -> SomeProxy

Which is equivalent to an existential, but we don’t support that. This is what GHC does, but I don’t really agree that this is an unambiguous generalization.

I mentioned this doesn’t always happen because of forall. It can happen due to polymorphic kind applications (this is much much more rare) that appear to be closed. This can happen with the empty row, but also with other polymorphic containers that have a polymorphic unit. GHC uses a magic Any :: forall a. a type family for situations like this (for now), hoping that this is unobservable, but this isn’t actually the case since kind applications in the symbolic type system are relevant and Any can show up in errors in a confusing way.

Please see this issue https://gitlab.haskell.org/ghc/ghc/issues/14198 for more details (it’s a really good read).

#15

I should also mention that it’s possible in the SomeProxy case to make it an ambiguous type variable:

type SomeProxy :: forall k. Type
type SomeProxy = forall (a :: k). Proxy a

But I don’t think it’s a good idea to generalize to something ambiguous.

#16

I believe I converted all of Halogen’s empty data declarations into the foreign import data type declaration in this commit: https://github.com/JordanMartinez/purescript/commit/feaaf3af8b6ecaa4a70aa1f64d9188b56c23dec0

I still get the same error message though. Also, the declaration for RenderState isn’t an empty data declaration, so perhaps I just need to add a kind signature specified to Type or Type -> Type, etc.? (https://github.com/JordanMartinez/purescript/blob/feaaf3af8b6ecaa4a70aa1f64d9188b56c23dec0/tests/support/.spago/halogen/v5.0.0-rc.7/src/Halogen/VDom/Driver.purs#L43):

Error 5 of 9:

  in module Halogen.VDom.Driver
  at .:0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      RenderState @t42 @t45

    where t42 is an unknown kind.
    where t45 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group ChildRenderer, RenderState

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.
#17

Also, are kind signatures available for foreign import data, too?

For example (see https://github.com/JordanMartinez/purescript/blob/feaaf3af8b6ecaa4a70aa1f64d9188b56c23dec0/tests/support/.spago/halogen/v5.0.0-rc.7/src/Halogen/Aff/Driver/State.purs#L77):

-- rather than
foreign import data DriverStateX :: (Type -> Type -> Type) -> (Type -> Type -> Row Type -> Type -> Type) -> (Type -> Type) -> Type -> Type

-- we have
foreign import data DriverStateX :: (Type -> Type -> Type) -> (Type -> Type -> Row Type -> Type -> Type) -> (Type -> Type) -> Type -> Type
foreign import data DriverStateX h r f o
#18

@JordanMartinez Those empty spans are really unfortunate. I’m not sure what’s happening with that. Seems to always happen in data binding groups.

#19

foreign import data is the same as foreign import. It’s only a type signature. For example, we don’t do

foreign import foo a b

when we have a function that takes two arguments.

#20

@natefaubion Turning on verbose errors doesn’t help much in this situation either…

Error 3 of 9:

  in module Formless.Types.Component
  at .spago/halogen-formless/v1.0.0-rc.1/src/Formless/Types/Component.purs:81:1 - 86:44 (line 81, column 1 - line 86, column 44)

    Type synonym Formless.Types.Component.PublicAction is partially applied.
    Type synonyms must be applied to all of their type arguments.

  in data constructor AsQuery
  in type constructor QueryF

  See https://github.com/purescript/documentation/blob/master/errors/PartiallyAppliedSynonym.md for more information,
  or to contribute content related to this error.

Error 4 of 9:

  in module Freedom.VNode
  at .spago/freedom/v1.4.1/src/Freedom/VNode.purs:61:1 - 61:84 (line 61, column 1 - line 61, column 84)
  at :0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      forall (k :: Type) (f :: k -> Type -> Type) (state :: k). Ref (Ref (Array (Array (VNode @t60 @t63 f state)))) -> BridgeFoot @k f state

    where t60 is an unknown kind.
    where t63 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group VObject, Operations, BridgeFoot, VNode, VElement, VRender, VRenderEnv

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 5 of 9:

  in module Halogen.VDom.Driver
  at .spago/halogen/v5.0.0-rc.7/src/Halogen/VDom/Driver.purs:40:1 - 41:80 (line 40, column 1 - line 41, column 80)
  at :0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      RenderState @t42 @t45

    where t42 is an unknown kind.
    where t45 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group ChildRenderer, RenderState

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 6 of 9:

  in module Options.Applicative.Types
  at .spago/optparse/v3.0.1/src/Options/Applicative/Types.purs:103:1 - 113:4 (line 103, column 1 - line 113, column 4)
  at :0:0 - 0:0 (line 0, column 0 - line 0, column 0)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      forall (a :: Type). Option @t60 a -> Parser a

    where t60 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in data binding group ParserInfo, Parser, Option, OptReader, CReader, ReadM, ParseError, SomeParser, MultPE

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.

Error 7 of 9:

  in module Pathy.Phantom
  at .spago/pathy/v7.0.1/src/Pathy/Phantom.purs:19:1 - 25:9 (line 19, column 1 - line 25, column 9)
  at .spago/pathy/v7.0.1/src/Pathy/Phantom.purs:21:8 - 25:9 (line 21, column 8 - line 25, column 9)

    Cannot unambiguously generalize kinds appearing in the elaborated type:

      forall (f :: RelOrAbs -> t31 -> Type) (b :: t31) (r :: Type). ((f Rel b -> f a b) -> f Rel b -> r) -> ((f Abs b -> f a b) -> f Abs b -> r) -> f a b -> r

    where t31 is an unknown kind.
    Try adding additional kind signatures or polymorphic kind variables.

  in type synonym IsRelOrAbs$Dict

  See https://github.com/purescript/documentation/blob/master/errors/QuantificationCheckFailureInType.md for more information,
  or to contribute content related to this error.
#21

That looks suspicious. It’s possible I’m missing a context application before generalization in data binding groups. We probably need a test case for polymorphic data binding groups. I do not expect some of those to take kind applications.