Skip to content
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

Make the TH machinery handle PolyKinds more robustly #945

Merged
merged 1 commit into from
Dec 14, 2020
Merged

Conversation

RyanGlScott
Copy link
Collaborator

This is a collection of various Template Haskell–related fixes that, when all put together, fixes #917. This does the following:

  • Rather than use th-abstraction's datatypeType function, which strips off important kind information from type arguments, I defined a similar datatypeTypeKinded function that preserves kinds.
  • Control.Lens.Internal.{FieldTH,PrismTH} is now more careful to use freeVariablesWellScoped (from th-abstraction) instead of typeVars to ensure that the resulting types are well scoped. This is particularly important for poly-kinded types, as the kind variables must always appear before the type variables.
  • I deleted the close function from Control.Lens.Internal.PrismTH in favor of quantifyType and quantifyType', which I have moved to Control.Lens.Internal.TH so that they may be used by FieldTH and PrismTH alike. Moreover, I now use quantifyType' in the definition of PrismTH.makeClassyPrismClass so that any type variables bound by the class itself do not get requantified in any class methods. The previous code was not doing this at all, which was just plain wrong.

@RyanGlScott
Copy link
Collaborator Author

I have marked this as an WIP for now since I had to vendor in an unreleased version of th-abstraction. I do this because the datatypeTypeKinded refactor above caused me to run into glguy/th-abstraction#84. To work around this, I have temporarily vendored in a version of th-abstraction with a fix (glguy/th-abstraction#85), so once that fix makes it to Hackage, I can simply adjust the lower version bounds on th-abstraction accordingly.

@RyanGlScott
Copy link
Collaborator Author

For what it's worth, this is definitely a breaking change, since any code that uses makeLenses, makePrisms, etc. with a data type with one or more type parameters will now be required to enable KindSignatures. As one example, this will break the wreq library:

[ 9 of 15] Compiling Network.Wreq.Lens.TH ( Network/Wreq/Lens/TH.hs, interpreted )

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseVersion’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_a5Pi’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseVersion’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseStatus’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_a5Pi’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseStatus’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseHeaders’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_a5Pi’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseHeaders’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseCookieJar’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_a5Pi’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseCookieJar’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseClose'’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_a5Pi’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseClose'’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseBody’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘GHC.Types.Type’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseBody’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_a5Pi’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseBody’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Network/Wreq/Lens/TH.hs:84:1: error:
    Illegal kind signature: ‘body_akQ5’
      Perhaps you intended to use KindSignatures
    In the type signature for ‘responseBody’
   |
84 | makeLenses ''HTTP.Response
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

This isn't a huge breakage, since one can fix it by simply enabling a language extension. But I thought this worth mentioning nonetheless.

@arybczak
Copy link

arybczak commented Nov 7, 2020

FWIW when I fixed this in well-typed/optics#313 I only annotated types with kinds involving variables, not monomorphic ones, so that KindSignatures is not needed (unless you use PolyKinds, but then it's implied anyway).

@RyanGlScott
Copy link
Collaborator Author

I fear that the situation is slightly more complicated than just detecting kind variables. Consider this program:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Foo where

import Control.Lens
import Data.Kind
import Data.Proxy

data family DF (a :: k)
data instance DF (a :: Type) = MkDF { _unDF :: Proxy a }
$(makeLenses 'MkDF)

If you generate this code without any kind signatures, you'll get the following:

/home/rgscott/Documents/Hacking/Haskell/Foo.hs:13:3-18: Splicing declarations
    makeLenses 'MkDF
  ======>
    unDF ::
      forall a_a44D a_a45f.
      Iso (DF a_a44D) (DF a_a45f) (Proxy a_a44D) (Proxy a_a45f)
    unDF = (iso (\ (MkDF x_a45g) -> x_a45g)) MkDF
    {-# INLINE unDF #-}

This won't typecheck:

/home/rgscott/Documents/Hacking/Haskell/Foo.hs:13:3: error:
    • Couldn't match type ‘k’ with ‘*’
      ‘k’ is a rigid type variable bound by
        the type signature for:
          unDF :: forall k k1 (a :: k) (a2 :: k1).
                  Iso (DF a) (DF a2) (Proxy a) (Proxy a2)
        at /home/rgscott/Documents/Hacking/Haskell/Foo.hs:13:3-18
      Expected type: p (Proxy a) (f (Proxy a2)) -> p (DF a) (f (DF a2))
        Actual type: p (Proxy a0) (f (Proxy a1)) -> p (DF a0) (f (DF a1))
    • In the expression: (iso (\ (MkDF x_a3YS) -> x_a3YS)) MkDF
      In an equation for ‘unDF’:
          unDF = (iso (\ (MkDF x_a3YS) -> x_a3YS)) MkDF
    • Relevant bindings include
        unDF :: p (Proxy a) (f (Proxy a2)) -> p (DF a) (f (DF a2))
          (bound at /home/rgscott/Documents/Hacking/Haskell/Foo.hs:13:3)
   |
13 | $(makeLenses 'MkDF)
   |   ^^^^^^^^^^^^^^^^

This is because DF a (i.e., DF (a :: k)) is too general for the data instance, which requires DF (a :: Type). You'd need to generate this code instead:

    unDF ::
      forall (a_a2sl :: Type) (a_a3YQ :: Type).
      Iso (DF (a_a2sl :: Type)) (DF (a_a3YQ :: Type)) (Proxy a_a2sl) (Proxy a_a3YQ)
    unDF = (iso (\ (MkDF x_a3YR) -> x_a3YR)) MkDF
    {-# INLINE unDF #-}

That being said, I do see your point about not needing KindSignatures everywhere, however. Perhaps it would suffice to strip off monomorphic kinds as long as we are dealing with non-data family instances. After all, if you are dealing with data families, then you almost assuredly have TypeFamilies enabled, and TypeFamilies implies KindSignatures. (This is the approach that libraries like deriving-compat take.)

@RyanGlScott
Copy link
Collaborator Author

I've pushed some changes that alter datatypeTypeKinded to only preserve kinds that contain kind variables (as long as it is not a data family instance), much in the spirit of well-typed/optics#313. Although this PR still contains breaking changes, they are now far less likely to occur in practice. (wreq will now compile with this version of lens, at the very least.)

This is a collection of various Template Haskell–related fixes that, when all
put together, fixes #917. This does the following:

* Rather than use `th-abstraction`'s `datatypeType` function, which strips off
  important kind information from type arguments, I defined a similar
  `datatypeTypeKinded` function that preserves kinds when reasonable.
* `Control.Lens.Internal.{FieldTH,PrismTH}` is now more careful to use
  `freeVariablesWellScoped` (from `th-abstraction`) instead of `typeVars`
  to ensure that the resulting types are well scoped. This is particularly
  important for poly-kinded types, as the kind variables must always appear
  before the type variables.
* I deleted the `close` function from `Control.Lens.Internal.PrismTH` in favor
  of `quantifyType` and `quantifyType'`, which I have moved to
  `Control.Lens.Internal.TH` so that they may be used by `FieldTH` and
  `PrismTH` alike. Moreover, I now use `quantifyType'` in the definition of
  `PrismTH.makeClassyPrismClass` so that any type variables bound by the class
  itself do not get requantified in any class methods. The previous code was
  not doing this at all, which was just plain wrong.
@RyanGlScott RyanGlScott changed the title WIP: Make the TH machinery handle PolyKinds more robustly Make the TH machinery handle PolyKinds more robustly Dec 10, 2020
@RyanGlScott
Copy link
Collaborator Author

Now that th-abstraction-0.4.1.0 has been released with a fix for glguy/th-abstraction#84, the last remaining obstacle in the way of this PR has been unblocked. If there are no further review comments, I'll likely land this some time in the coming week or so.

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.

Kind and type vars sometimes out of dependency order with makePrisms/makeLenses
2 participants