How to export type constructors when using DataKinds extension?

Question

Playing with advanced type-system stuff. I want to have named kind and a couple of type constructors that produce types of that kind:

{-# LANGUAGE DataKinds #-}

data Subject = New | Existing

Here, as I understand, we have named kind Subject and type constructors New and Existing that are :: Subject. These type constructors do not take arguments (I plan to use them as phantom types), it should be roughly equivalent to:

{-# LANGUAGE EmptyDataDecls #-}

data New
data Existing

With the difference that now I can write:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}

-- …

data MyConfig :: Subject -> * -> * where
  MyConfig
    { mcOneThing :: Path t File
    } :: MyConfig k t

This even compiles. What is confusing is that declaration of data kinds is indistinguishable from data type declarations, so this code seems to produce data type Subject as well as named kind Subject (?) It would be clearer for me it we could specify on which level do we declare things (kinds, and then New and Existing are type constructors; or types, and then New and Existing are value constructors for things of Subject type). I don't get this design decision with “promote everything that seems to work”.

Now, my problem is that I cannot export New and Existing as type-constructors to use in other module, e.g. to declare things like:

foo :: MyConfig New Dir -> …

where at the same time

foo :: MyConfig Int Dir -> …

should be ill-kinded and it should not compile.

Here is how I'm trying to export them:

module MyModule
  ( New
  , Existing
  -- …
  )
where

What I get:

Not in scope type constructor or class ‘New’

Not in scope type constructor or class ‘Existing’

GHC manual in section 7.9.3 says that to distinguish between “types and constructors” one can use single quote ', so I tried:

module MyModule
  ( 'New
  , 'Existing
  -- …
  )
where

…but now it's a parse error.

---

How do I export New and Existing type constructors, and most importantly, is there anything wrong with my current understanding?

Answer 1

Use the usual syntax for exporting constructors:

module MyModule (Subject(..)) where

data Subject = New | Existing

Currently, lifted and unlifted constructors are tied together, so we can only export/import them together.

Also, you don't need to have DataKinds in MyModule, only in the module where you intend to use lifted constructors.