Make TH always reify data types with explicit return kinds

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?

Trac metadata

Trac field	Value
Version	8.6.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Template Haskell
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request TemplateHaskell Trac import labels

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.

As further evidence for how //ad hoc// the restriction in ticket:16300#comment:168510 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!

Ah, but the program in ticket:16300#comment:168516 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 ticket:16300#comment:168510 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.

1. ..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?

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 ticket:16300#comment:168516, as it would be rejected in Haskell.

Replying to [ticket:16300#comment:168531 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.

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.

Replying to [ticket:16300#comment:168533 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.

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.

added StandaloneKindSignatures label

added UnliftedNewtypes label

added Pnormal label

mentioned in merge request !1438 (merged)

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.

!1476 (closed) implements this idea.

Now that we have reifyType, do we want reify to return the type/kind for backwards compatibility?

That is, do we want to change

  | VarI
       Name
       Type
       (Maybe Dec)
...

  | DataD Cxt Name [TyVarBndr]
          (Maybe Kind)            -- Kind signature (allowed only for GADTs)
          [Con] [DerivClause]

to

  | VarI
       Name
       (Maybe Dec)
...

  | DataD Cxt Name [TyVarBndr]
          [Con] [DerivClause]

?

!1476 (closed) implements this idea.

Indeed. I think reifyType is a satisfactory solution to my original problem, so I would be content with closing this issue.

In response to #16300 (comment 215556) (which was spun off from the discussion starting at !1438 (comment 213924)), I do think that there may be some room in the Template Haskell API for further simplification, although it might be best to discuss this in a separate issue, as it is somewhat orthogonal to this one.

One point of clarification is that I don't think we should change any of Decs constructors, as these are intended to reflect the surface syntax of Haskell. For instance, without the Maybe Kind field of DataD, it would be impossible to faithfully quote [d| data F a b :: Type -> Type |]. The Info type, on the other hand, is only used for reification purposes, so we can be more flexible with its design.

changed milestone to %8.10.1

Closing, since this was fixed with #16976 (closed)/!1476 (closed).

closed