Better support for kinds in Template Haskell

[guest]

Type checking the attached code produces a legitimate type error, and also the following message:

Tip.hs:107:14:ghc: panic! (the 'impossible' happened)
  (GHC version 7.0.3 for i386-unknown-linux):
	Exotic form of kind ghc-prim:GHC.Prim.?{(w) tc 34g}

[guest]

Code

[guest]

More code (load this module)

[dreixel]

Could you perhaps say which libraries are necessary to build this (like QuickCheck), and their versions? Or, even better, minimize the test so that it doesn't rely on external libraries? That makes it easier to test with the current development branch.

[lunaris]

I can reproduce what appears to be the same bug with the following:

First.hs:

{-# LANGUAGE PolyKinds #-}

module First where

data Proxy (as :: [*])
  = Proxy

f :: Proxy as -> ()
f _
  = ()

Second.hs:

module Second where

import First

import Language.Haskell.TH

GHCI session:

% ghci -XTemplateHaskell Second.hs
GHCi, version 7.3.20111204: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 2] Compiling First            ( First.hs, interpreted )
[2 of 2] Compiling Second           ( Second.hs, interpreted )
Ok, modules loaded: Second, First.
*Second> $(reify 'f >>= stringE . show)
Loading package array-0.3.0.3 ... linking ... done.
Loading package deepseq-1.2.0.1 ... linking ... done.
Loading package containers-0.4.2.0 ... linking ... done.
Loading package pretty-1.1.0.0 ... linking ... done.
Loading package template-haskell ... linking ... done.

<interactive>:2:3:
    Exception when trying to run compile-time code:
      <interactive>: panic! (the 'impossible' happened)
  (GHC version 7.3.20111204 for x86_64-unknown-linux):
	Exotic form of kind [ghc-prim:GHC.Prim.*{(w) tc 34d}]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

      Code: (>>=) reify 'f (.) stringE show
    In the expression: $(reify 'f >>= stringE . show)
    In an equation for `it': it = $(reify 'f >>= stringE . show)

As far as I can tell, there aren't any TH constructors for promoted kinds yet, so reifyKind in TcSplice? can't do anything better.

[dreixel]

Replying to lunaris:

I can reproduce what appears to be the same bug with the following:

I think they are different things, as the original report wasn't using promoted kinds at all.

(Though we should certainly do something about reification of promoted kinds too; thanks for reporting.)

[dreixel]

I cannot reproduce the original error in ghc-7.2.1 (even after fixing a probably unintended type error in the source).

So I'm leaving this to track only lunaris's report with -XPolyKinds.

[lunaris]

If there's some sort of design in place for how kinds might be handled in TH.Kind, then I'm all up for implementing it, but there doesn't appear to be one yet.

[dreixel]

 http://hackage.haskell.org/trac/ghc/changeset/e328942561be162dd5f42b4ef630249ed34f1ef9 gives a more civilized error. Also for kinds like Constraint, which TH doesn't handle either.

I guess this will do for 7.4, and we should indeed come up with a design for handling the new kinds in TH.

[goldfire]

Check out TemplateHaskellRichKinds for implementation plan.

[goldfire]

Implementation complete and straightforward. Check out the attached patches.

[goldfire]

patch tarball

[igloo]

thanks, we'll take a look

[simonpj]

Thank you for doing this, goldfire. I'm sorry I've been playing dead. I'm surfacing slowly.

As you say, the implementation is straightforward, but there are design choices to make.

• The existing Type data type uses TupleT 3 plus AppTs for 3-tuples, and it would really be inconsistent not to continue to do this. Even arrows work like this! So I think I strongly prefer your "simpler types" alternative. Indeed that was the way you went for kinds!

• If I have data Foo = Foo, then I can use both Foo and 'Foo as a type constructor, and they will have different Names. Yet I think it is useful to be able to distinguish the two. So I'm inclined to suggest

  data Type = ...
            | VarT Name       -- Type variable
            | ConT Name       -- Ordinary type constructor 
            | PromotedT Name  -- Promoted data constructor
            ...
  

• In GHC we combine Type and Kind into one data type (called Type). In TH up to now it's been separate, but as you have found you have to add most of the machinery of Type to Kind, so the two are almost duplicates! (Indeed I think you have left Forall out of kinds, but it's needed too.) So I wonder about collapsing the two into one in TH as well.

  type Kind = Type
  

  I don't have a firm view, but it looks attractive.

• I think you will need ForallT in kinds.

Does this make sense?

[lunaris]

I'm having a go at implementing simonpj's changes on top of goldfire's patch in HEAD. I'm not too fond on the proposed:

type Kind = Type

But given that there is now a massive overlap between the types it may well be the sane option.

[goldfire]

Thanks for taking a look at this, lunaris. I've been meaning to get back to it, but time has been short with a paper deadline looming tomorrow.

I, too, was worried about Kind = Type, though my biggest fear was disrupting code that already uses Kind. In any case, setting Kind = Type now may be a sign of what's to come, so it may not be a bad idea.

As for ForallK, it's not clear to me how to implement it. For example, consider this:

data Foo (a :: k -> *) (b :: k) where
  Bar :: a b -> Foo a b

The TH rendition of Foo will have two KindedTVs. Where should the ForallK be? If we want to explicitly quantify over kind variables, it looks like one route would be to make a KindV constructor for TyVarBndr. Then, the above declaration would be something like (letting Names be strings):

DataD [] "Foo" [KindV "k",
                KindedTV "a" ((VarK "k") `ArrowK` StarK),
                KindedTV (VarK "k")] [...] []

There is also the question of what to do with explicit quantification when converting back from TH constructs into GHC's internal constructs, which don't have explicit kind variable quantification at that stage of the pipeline. Simply ignore the quantification? Error-check?

In any case, the implementation contained in the patches avoids the problem by doing what surface Haskell does: it just uses implicit kind variable quantification.

I'll be back above water by the middle of next week and would be happy to contribute again. Lunaris, let me know if there is a way I can help.

[simonpj]

In the source language (as it stands) there is no way to explicitly quantify over a kind variable; you cannot say forall k. forall (a::k). blah. Instead, kind quantification is always implicit. (This is really a missing feature, but that's another story.)

Currently TH is just concrete syntax for Haskell source syntax. So I think it's proably ok not to have KindV, but instead simply not to bind kind variables explicitly.

All of this is bound to affect TH users using Kind; there's really no alternative I think.

[lunaris]

Ok, so the functionality described above seems to be working (patches once validation has completed). As it stands, I made the following changes:

• Type and Kind are one and the same:

      data Type = ...
                | PromotedT Name
                | PromotedTupleT Int
                | PromotedNilT
                | PromotedConsT
                | StarT
                | ConstraintT
  
      type Kind = Type
  

I'm not sure if this is what was envisaged, but to "compensate" I've also provided functions such as varK, conK, arrowK, listK, starK, constraintK etc.

• PromotedT applications are produced by checking an HsTyVar's name to see if it falls in the Data namespace (isDataOcc). This appears to work but I'm not sure if it's guaranteed to be correct.

• Since Type and Kind are now the same type, arrows at the kind level have changed. It may be worth adding functions to TH.Lib that encapsulate the "obvious" folds -- I find myself using foldr (appT . appT promotedConsT) promotedNilT and others quite a bit.

• Reifying a type such as:

  data Dict c where
    Dict :: c => Dict c
  

won't work because irreducible constraints aren't in TH. Is this simply a case of adding something like:

data Pred = ...
          | VarP Name

(modulo the name VarP since Pat has taken it already) or are we going to end up in trouble if we do this? Similarly, is there ever a case where we'll hit TuplePred during a call to reify?

I think that's it; other than that it seems all right.

[goldfire]

I, for one, like the idea of fold and unfold operations in the TH library.

How would one refer to the kind Nat? Is it PromotedT (mkName "Nat") or ConT (mkName "Nat") (both used in a context expecting a kind)? Does the algorithm in Convert.lhs check for consistent usage of ConT vs PromotedT?

[lunaris]

I'm currently working on the Nat stuff, because I'm pretty sure reify can't deal with it yet. There's also the issue that the interface in GHC.TypeLits doesn't appear to be finalised yet (at least not to my mind).

I think the folds should be added, though perhaps as a separate ticket/patch. I think many of the use-cases for arrowK/arrowT and promotedConsT/promotedNilT etc. entail the same two or three functions.

[lunaris]

Updated patches, incorporating simonpj's/goldfire's comments.

[lunaris]

Forgot to regenerate patches after bugfix.

[lunaris]

Ok, I think the updated patches should work. I've ported over most of goldfire's test cases, except the last set, which I'll hopefully get around to tomorrow.

In addressing this ticket, I've also fleshed out TH support for type-level literals, which was somewhat incomplete. I felt it was necessary to cope with the introduction of type Kind = Type. These changes have been kept in separate patches however, and have not received additional test suite coverage.

Let me know what you think!

[simonpj]

See also #6066

[lunaris]

Regarding the above, the attached patches should fix #6066. I can re-roll if they've become too out-of-date to apply.

[simonpj]

Many thanks to lunaris and Richard Eisenberg. I've just pushed patches to HEAD to add promoted types and kind polymorphism to Template Haskell.

commit 0fe0c58ee9758f1606ccd12fd04121a08488fb9a
Author: Richard Eisenberg <eir@seas.upenn.edu>
Date:   Tue May 15 13:42:46 2012 -0400

    Applied lunaris's patch to allow promoted types and rich kinds in Template Haskell

 compiler/deSugar/DsMeta.hs      |  552 ++++++++++++++++++++++++---------------
 compiler/hsSyn/Convert.lhs      |  179 ++++++++------
 compiler/prelude/TysWiredIn.lhs |    2 +-
 compiler/typecheck/TcSplice.lhs |   46 +++-
 compiler/types/TyCon.lhs        |   11 +
 5 files changed, 497 insertions(+), 293 deletions(-)

commit 869044056c54dfe95017c19bef5274b748cfe724
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri May 18 10:10:28 2012 +0100

    Wibbles to lunaris's patch for promoted kinds

 compiler/deSugar/DsMeta.hs |   18 +++++++-----------
 compiler/hsSyn/Convert.lhs |    9 ++++++---
 2 files changed, 13 insertions(+), 14 deletions(-)

There are corresponding patches in libraries/template-haskell of course:

commit 5d36a74d115cb7c4c12a6c3bcc369e320fe1d1b3
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri May 18 10:06:17 2012 +0100

    Change TH syntax to allow promoted kinds and kind polymorphism
    
    The big change here is that Kind is no longer a distinct type,
    it's just a type synonym for Type.  This reflects exactly what
    happens in the HsSyn world, and avoids a great deal of duplication
    between types and kinds.   But it is a breaking for (the few)
    TH users who were using the constructors for Kind.
    
    Thanks to lunaris and Richard Eisenberg for doing the work.

 Language/Haskell/TH.hs        |   20 +++++++++-----
 Language/Haskell/TH/Lib.hs    |   40 ++++++++++++++++++++++++---
 Language/Haskell/TH/Ppr.hs    |   38 +++++++++++++++------------
 Language/Haskell/TH/Syntax.hs |   58 ++++++++++++++++++++++++++++++++++++-----
 4 files changed, 120 insertions(+), 36 deletions(-)

Richard and/or lunaris also provided some tests in tests/th.

Thanks all!

Simon

[goldfire]

The current implementation of this feature has a constructor PromotedT used to denote a promoted data constructor used as a type. However, if the Name passed to this constructor is created with mkName and is ambiguous (because both a native type and data constructor exist with the same name), the PromotedT behaves just like a ConT.

The one-line patch I will post shortly fixes this problem, defaulting PromotedT to use the promoted data constructor. The behavior of unambiguous PromotedTs is unaffected.

[goldfire]

fix the default behavior of PromotedT

[simonpj]

Done:

commit d69f5e46a6d421e17ccf49d5517d009733de3dd5
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Tue Jun 5 11:43:31 2012 +0100

    Use a *constructor* name when promoting a type
    
    This is when converting from TH -> HsSyn
    Thanks to Richard Eisenberg