Opened 7 months ago

Last modified 7 months ago

#16300 new feature request

Make TH always reify data types with explicit return kinds

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Template Haskell Version: 8.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Currently, whenever you reify a data type with Template Haskell, it will return a DataD/NewtypeD where the return kind information has been set to Nothing:

λ> putStrLn $(reify ''Bool >>= stringE . show)
TyConI (DataD [] GHC.Types.Bool [] Nothing [NormalC GHC.Types.False [],NormalC GHC.Types.True []] [])

One could argue that this isn't a problem since data types always have return kind Type anyway. For 99% of data types, this is true. There are a handful of exceptions, such as unboxed tuples (with return kind TYPE (TupleRep [...]), but those could be dismissed as unusual special cases.

With the advent of unlifted newtypes, however, things become murkier. UnliftedNewtypes let you define newtypes like this one:

newtype Foo :: TYPE IntRep where MkFoo :: Int# -> Foo

Notice how the return kind is not Type, but instead TYPE IntRep. However, TH reification doesn't clue you in to this fact:

λ> putStrLn $(reify ''Foo >>= stringE . show)
TyConI (NewtypeD [] Ghci8.Foo [] Nothing (GadtC [Ghci8.MkFoo] [(Bang NoSourceUnpackedness NoSourceStrictness,ConT GHC.Prim.Int#)] (ConT Ghci8.Foo)) [])

Still Nothing. There's no easy way in general to determine what the return kind of an unlifted newtype is using TH reification, which is unfortunate.

Luckily, I think there's a very simple fix that we could apply here: just have TH reification return Just (<kind>) instead of Nothing! There's no technical reason why TH couldn't do this; the only reason it currently returns Nothing is due to historical convention. Moreover, I doubt that this would even break any code in the wild, since Nothing doesn't convey any useful information in the context of TH reification anyway.

Does this sound reasonable?

Change History (8)

comment:1 Changed 7 months ago by RyanGlScott

A different (but closely related) issue is that currently, this is rejected:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where

import Language.Haskell.TH

$(pure [DataD [] (mkName "D") [] (Just StarT)
              [NormalC (mkName "MkD") []] []])
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:7:3: error:
    Kind signatures are only allowed on GADTs
    When splicing a TH declaration: data D :: * = MkD
  |
7 | $(pure [DataD [] (mkName "D") [] (Just StarT)
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

This restriction feels somewhat artificial, given that GHC can't even parse Haskell98-style declarations with explicit kind signatures in the first place (ignore the bit about data D :: * = MkD, as that's just a pretty-printing mistake). Indeed, the Maybe Kind field of DataD/NewtypeD only makes sense if the data type happens to be a GADT. If it's not a GADT, surely it doesn't do any harm to just ignore the Maybe Kind, right?

I care about this since changing TH reification to always fill in the Maybe Kind field with Just <...> causes the TH_spliceDecl3 test case to start failing with the "Kind signatures are only allowed on GADTs" error. If you look at the implementation of the test, you'll see why:

-- test splicing of reified and renamed data declarations

module TH_spliceDecl3
where

import Language.Haskell.TH
import TH_spliceDecl3_Lib

data T = C

$(do { TyConI d <- reify ''T; rename' d})

It's reifying T (a Haskell98 data type) and then immediately splicing back in. Due to the aforementioned restriction about kinds, however, this fails. We could dig into the reified AST and change Just Type to Nothing before splicing it back it, but this feels like a lot of unnecessary work. I propose that we just drop this restriction as well.

comment:2 Changed 7 months ago by RyanGlScott

As further evidence for how ad hoc the restriction in comment:1 is, if I change the program to use NewtypeD instead:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where

import Language.Haskell.TH

$(pure [NewtypeD [] (mkName "D") [] (Just StarT)
                 (NormalC (mkName "MkD")
                          [(Bang NoSourceUnpackedness NoSourceStrictness, ConT ''Int)])
                 []])

Then GHC accepts it without issue!

comment:3 Changed 7 months ago by RyanGlScott

Ah, but the program in comment:2 is accepted for different reasons than what I expected. It's not being accepted due to the fact that Just StarT is ignored. In fact, GHC is checking the explicit return kind! This is demonstrated by this program, which tries to sneak in something bogus:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where

import Language.Haskell.TH

$(pure [NewtypeD [] (mkName "D") [] (Just (ArrowT `AppT` ConT ''Maybe `AppT` StarT))
                 (NormalC (mkName "MkD")
                          [(Bang NoSourceUnpackedness NoSourceStrictness, ConT ''Int)])
                 []])
GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:8:3: error:
    • Expecting one more argument to ‘Maybe’
      Expected a type, but ‘Maybe’ has kind ‘* -> *’
    • In the kind ‘Maybe -> GHC.Types.Type’
  |
8 | $(pure [NewtypeD [] (mkName "D") [] (Just (ArrowT `AppT` ConT ''Maybe `AppT` StarT))
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

I suppose this reveals another viable alternative. We could just treat the program in comment:1 as though we were trying to splice in a GADT (i.e., newtype D :: Type where MkD :: D). Granted, we'd then be splicing in a GADT using NormalC instead of the usual GadtC, but there's no reason why we couldn't reinterpret NormalC as though it were specifying a GADT constructor.

...except there's another weird thing that Convert does in which it rejects mixed uses of NormalC and GadtC:

        ; unless (isGadtDecl || isH98Decl)
                 (failWith (text "Cannot mix GADT constructors with Haskell 98"
                        <+> text "constructors"))

This suggests that if we want to pursue this direction, then we should further lift this mixed constructors restriction. Hm...

I'm not sure which route to go down. Do others have any thoughts?

comment:4 Changed 7 months ago by goldfire

I favor keeping the no-mixed-constructors and no-kind-sig-without-GADT-constructors restrictions: they keep TH closer to Haskell. I feel like every time TH diverges from Haskell, we regret it later.

So, returning to the original question: how about non-Type-kinded datatypes/newtypes always reify as GADTs? The choice of syntax in reification is immaterial, so let's just change it.

Also, we should reject the example in comment:2, as it would be rejected in Haskell.

comment:5 in reply to:  4 Changed 7 months ago by RyanGlScott

Replying to goldfire:

how about non-Type-kinded datatypes/newtypes always reify as GADTs? The choice of syntax in reification is immaterial, so let's just change it.

I can see the appeal behind this choice, but at the same time, I would be a little sad if we went in this direction. Generally speaking, I like keeping TH reification as honest as possible. Moreover, whether a data type is declared as a GADT or not has some consequences on its other properties. For instance, the derived Show instance for a data type with infix constructors changes depending on whether the type is a GADT, and unless consumers have a reliable way to reify whether or not a data type is a GADT, they wouldn't be able to replicate what deriving Show does with Template Haskell, which would be a bit sad.

I really wish that we had top-level kind signatures, since then we could just reify type Foo :: TYPE IntRep, regardless of whether Foo was defined using Haskell98 or GADT syntax. I suppose we could just park this ticket until that becomes a reality.

comment:6 Changed 7 months ago by goldfire

I suppose we could just park this ticket until that becomes a reality.

That sounds like as good an idea of any of these others.

Actually, maybe it would be better to have qTypeKind :: Type -> Q Kind and qExprType :: Exp -> Q Type. Then, we can avoid this whole kerfuffle for unlifted newtypes by requiring clients to just get the kind of the argument. Note that these two functions would not be particularly hard to write but would be very useful.

comment:7 in reply to:  6 Changed 7 months ago by RyanGlScott

Replying to goldfire:

Actually, maybe it would be better to have qTypeKind :: Type -> Q Kind and qExprType :: Exp -> Q Type. Then, we can avoid this whole kerfuffle for unlifted newtypes by requiring clients to just get the kind of the argument.

That's an intriguing idea.

Note that these two functions would not be particularly hard to write but would be very useful.

While I imagine one could implement these functions, I wonder what their specification should be. What should they do if their inputs are ill typed, for instance? Also, the answers that they return might change depending on whether certain language extensions are enabled.

comment:8 Changed 7 months ago by goldfire

Note that they are in the Q monad: there's no claim to purity here. This means it's reasonable for the behavior to depend on extensions, etc.

I suppose this could be a specification: they return the information that :t or :k would return. And that could also essentially be the implementation.

Note: See TracTickets for help on using tickets.