DataKinds promotion of String -> Symbol and Natural -> Nat

Exactly what it says on the tin. It would be nice if the following would compile:

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

import GHC.TypeLits
import GHC.Natural

data X = X String Natural

data Y :: X -> * where
    Y :: Y ('X "hello" 4)

I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.

changed weight to 5

added Tfeature request Trac import typechecker labels

changed the description

Combining Natural and Nat seems straightforward. But Symbol and String are different: the former is not a list of characters. Symbol is much more like a promoted Text than a promoted String. And we might want the kind String to mean a type-level list of type-level characters someday.

Even better than making progress on these small issues is to step back and come up with a plan for type-level literals of all stripes (floating-point numbers, characters, a promoted Num class of some sort?). I'm worried that small forays into this space will dig us into a local minimum from which we can't escape.

A hearty amen on this one, especially unifying Natural with Nat.

Regarding the String objection perhaps it would be better to merely flesh out Symbol at the term level? With an IsString instance and so forth? Because as mentioned unifying it with String is problematic since String is a type synonym for a list of characters.

I also agree with Richard's comments regarding the desirability of type-level literals of all stripes (or at least other stripes). I'm not sure if floating-point numbers or characters specifically are useful, but integers and rationals most definitely are of use to the dimensional library. We have home-brewed ones, but it is a lot of machinery, isn't interoperable with the few other flavors of home-brewed ones on the market, and isn't the lifted version of Rational or Integer so you can't use the lifted kinds that go with the types of term-level structures that include rational or integers.

Trac metadata

Trac field	Value
CC	- → dmcclean

mentioned in issue #11342 (closed)

Trac metadata

Trac field	Value
Related	- → #11342 (closed)

added DataKinds label

added Pnormal label

mentioned in merge request !3583 (merged)

One half of this was completed in !3583 (merged)/8f4f5794.

mentioned in commit 8f4f5794