Opened 8 years ago

Last modified 4 years ago

#6024 infoneeded feature request

Allow defining kinds alone, without a datatype

Reported by: dreixel Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.5
Keywords: Cc: ross@…, bgamari@…, diatchki@…, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


Sometimes we want to define a kind alone, and we are not interested in the datatype. In principle having an extra datatype around is not a big problem, but the constructor names will be taken, so they cannot be used somewhere else. A contrived example:

data Code = Unit | Prod Code Code

data family Interprt (c :: Code) :: *
data instance Interprt Unit       = Unit1
data instance Interprt (Prod a b) = Prod1 (Interprt a) (Interprt b)

We're only interested in the constructors of the data family Interprt, but we cannot use the names Unit and Prod because they are constructors of Code.

The suggestion is to allow defining:

data kind Code = Unit | Prod Code Code

Such that Code is a kind, and not a type, and Unit and Prod are types, and not constructors.

Note that using "data kind" instead of just "kind" means the word "kind" does not have to be a reserved keyword.

You could also think you would want to have datatypes that should not be promoted:

data K

data type T = K

But I don't see a need for this, as the fact that the K constructor is promoted to a type does not prevent you from having a datatype named K.

Change History (13)

comment:1 Changed 7 years ago by dreixel

comment:2 Changed 7 years ago by igloo

difficulty: Unknown
Milestone: 7.8.1

Is it clear that being able to use the same names for different things won't cause too much confusion?

I guess that we manage fine with constructors and types sharing names, so perhaps there is no problem with types and kinds.

Are there any plans to have support for "sorts" and above in GHC? If so, would each level have its own namespace?

comment:3 Changed 7 years ago by dreixel

I don't think the language of sorts will be extended; if anything, types and kinds might be collapsed into a single level. That would also destroy the possibility of doing what is asked in this ticket, though.

comment:4 Changed 7 years ago by ross

Cc: ross@… added

I'm particularly interested in using * in a kind definition, which should be possible with a distinct syntax for kind definitions.

comment:5 Changed 6 years ago by bgamari

Cc: bgamari@… added

comment:6 Changed 5 years ago by thoughtpolice


Moving to 7.10.1.

comment:7 Changed 5 years ago by dreixel

Cc: diatchki@… added

Iavor, you worked on this for a while, didn't you? What's the status?

comment:8 Changed 5 years ago by thomie

Status: newinfoneeded

comment:9 Changed 5 years ago by thoughtpolice


Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:10 Changed 4 years ago by thoughtpolice


Milestone renamed

comment:11 in reply to:  3 Changed 4 years ago by thomie

Cc: goldfire added

Is this feature request still possible to implement, now that "kinds and types are the same" (6746549772c5cc0ac66c0fce562f297f4d4b80a2). See also comment:3.

comment:12 Changed 4 years ago by goldfire

Yes, though it's a shade less useful. Types and kinds are indeed the same now, but terms are not. I see this ticket as a request for an ability to define a datatype whose constructors are defined only in types, never in terms. From a user standpoint, this ticket is largely unaffected by type=kind.

It's a shade less useful because you can now say

data Foo = MkFoo1 Type   -- Type is a.k.a. *
         | MkFoo2 Int

so some of the motivation for kind-only has gone away. A kind-only definition would still prevent clients from constructing the object at runtime, though.

comment:13 Changed 4 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.