Type-level literals as a separate language extension (under review)

[RossPaterson]

This is a proposal to introduce a language extension TypeLevelLiterals (implied by DataKinds) to turn on the features in the Type-Level Literals section of the User's Guide without necessarily turning on datatype promotion.

Rendered

[simonpj]

Seems entirely plausible and uncontroversial to me.

[phadej]

With GHC-9.2.4 just

import GHC.TypeLits (Nat)
import Data.Kind (Type)

data Vector :: Nat -> Type -> Type where

requires DataKinds, because Nat is data.

For some reason GHC-9.4.1/9.4.2 doesn't, which seems to be a bug to me (I cannot find anything in https://downloads.haskell.org/~ghc/9.4.1/docs/users_guide/9.4.1-notes.html justifying why this is now accepted with just -XHaskell2010 -XGADTSyntax -XKindSignatures).

---

Especially if above is not an intended change and indeed a bug, it doesn't look you can write much programs with just TypeLevelLiterals, as about anything else than literals requires DataKinds anyway. A sub-extension of DataKinds which allows just Natural, Symbol and Char promotion would probably be a more generally usable, i.e. forbidding promotion of "user defined" types.

[RossPaterson]

I guess that now that kinds are types, promotion doesn't do anything to the type -- it's just data constructors being promoted to type constructors. That's certainly how it looks in the code, though the User's Guide still talks about kinds in places.

[phadej]

But if kinds are types, why would

data Vector :: Natural -> Type -> Type where
  Nil :: Vector 0 a
  Cons :: a -> Vector n a -> Vector (n+1) a

be ok with just TypeLevelLiterals but

data Foo :: Bool -> Type where
  Foo :: Foo True
  NotFoo :: Foo False

will require "more powerful" DataKinds?

Does DataKinds do much else then allowing to write "terms" (incl. literals) in types anymore (i.e. making GHC look in term namespace for things too)?

#106 doesn't specify whether TypeData extension will enable such lookup on its own (for just type data defined types!), or just enable DataKinds implicitly.

[RossPaterson]

#106 specifies that the constructors introduced by a type data definition become type constructors, not data constructors. That's all -- it does not affect the lookup of other constructors, either within the type data definition or elsewhere. The intent is finegrained namespace control, whereas with TypeData each constructor in a data definition is potentially a data constructor and a type constructor (if the definition obeys certain restrictions).

As for the first question, that is indeed what is proposed here. It would be useful, because then one could use literals at the type level without giving up namespace control.

[phadej]

@RossPaterson I see, thanks for the explanations.

To me it seems that implementing this proposal would be much more valuable when #106 is implemented.

[RossPaterson]

Indeed. I have an implementation of #106 that just needs a bit of finishing, and that was the motivation for this proposal.

[konsumlamm]

Suggested change

	Cons :: a -> Vector n a -> Vector (n+1) a
	Cons :: a -> Vector n a -> Vector (n + 1) a

Just a style change, but usually operators have spaces around them.

[Ericson2314]

I still don't understand the semantics of this even with #106. Are we going to use type data in conjunction with Natural, Symbol, and Char?

Morally, I think literals desugar to some "secret" data constructors. This is especially true if/when for Dependent Haskell we make type level literals use the same overloading as regular ones.

So while I do think it's fine to enable the syntax without enabling the data kind semantics, I feel like every use of that new syntax (except for maybe Symbol) ought to be an error. That's not "practical", yes, but as proposed this feels like an ad-hoc treatment of some data types but not others.

[Ericson2314]

If there was a way to do something like import Data.Char (Char (..)) as type to selectively "promote" just the data constructors (explicit or implicit via literals) we want, that would feel to me far less ad-hoc and also in better accordance with the Dependent Haskell plans.

[RossPaterson]

I think the technical effect of this proposal is quite clear, and already described in detail in the "Type-Level Literals" section of the User's Guide. (As for #106, type data can only be used for new definitions, and so would not affect Natural, Symbol or Char.)

I believe this is the same philosophical objection to allowing literals like 23, 'c' and "abc" in both expressions and types, but not constructors like False and Just. It is different, but the idea is to allow one to be selective about what is promoted. This feature won't be useful for people using DataKinds or DependentHaskell, but will be useful for those that don't.

[int-index]

This proposal appears to be entirely about namespaces, just like #106.

Q: How is promoting 42 :: Natural different from promoting True :: Bool?
A: Promoting 42 does not require using term-level names at the type level, whereas promoting True does, leading to a potential name conflict with type True = ... and requiring namespace disambiguation syntax 'True.

Both #106 and this proposal attempt to carve out a language subset where type-level programming is possible but terms and types are kept separate. Personally, I would find this subset too limiting and keep reaching for the full power of DataKinds, but I see no problem with factoring out TypeLevelLiterals into its own extension.

[RossPaterson]

Summary: the only objection was a philosophical one to allowing literals like 23, 'c' and "abc" in both expressions and types, but not constructors like False and Just. As pointed out by Vladislav, the difference is that promoting constructors raises the possibility of name conflicts and the need for disambiguating quote marks.

@nomeata - I believe this proposal is ready for review.

[int-index]

I've made a recommendation: https://mail.haskell.org/pipermail/ghc-steering-committee/2023-March/003165.html

The proposal is now under committee review.

[goldfirere]

This proposal strikes me as an attempt to have GHC offer support for a particular stylistic choice. (It's like #270 in this regard.) As our language grows -- and we programmers become increasingly conditioned to rely on our tools -- this kind of feature request makes a lot of sense. However, I don't see the need for it to lead to a language extension. Instead, if GHC had a warning for a constructor used in a type, users could choose to set that to Werror and achieve the goals of this proposal, no?

And actually, GHC already has such a warning! It's called -Wunticked-promoted-constructors. That's a mouthful, and I (as its author) regret the name and the way it was originally presented. But actually I think it exactly fits the need here. As a bonus, using this warning allows a programmer to use a constructor in a type if necessary: I'm imagining a 2,000-line file where the author wants to avoid constructors in types.... but then they need one just on line 1,673. It would be frustrating to lose the no-constructors-in-types check in the rest of the file just for that one usage. But with -Wunticked-promoted-constructors, just put the ' in and away you go!

Question for the crowd: Does my -Wunticked-promoted-constructors plan fit in with #378? That is, I have a niggling feeling that we wanted to remove the ' at some point, due to the conflict with Template Haskell. If that's the case, the "use a warning" idea is still a good one; it just means we need a slightly different mechanism than the existing one.

A little background: I believe that each language extension imposes a tax on our ecosystem, in that each extension doubles the number of languages we call Haskell. Haskellers have to learn how to read all of these languages, even if they write in only some of them. I claim (without evidence) that each language extension thus increases the cognitive burden of using Haskell (even if only slightly), and thus we should be parsimonious about them. (If anyone is tracking, this stance of mine has evolved over time; I was more sanguine about extensions in the past.)

[RossPaterson]

It's a choice to use a subset of an extension, like GADTSyntax vs GADTs. Would a warning be a workable alternative in that case?

In this case the type-level literals subset does not interact with the data constructor promotion provided by the rest (though they have similar purposes). I assume it is for this reason that they are already documented in separate sections of the User's Guide.

The warning approach may be logical when starting from DataKinds, but it seems conceptually complicated when coming from the other direction. To understand a module with TypeLevelLiterals, one would need only to consult the type-level literals section of the User's Guide. There is no need to consult the data constructor promotion section to learn about a feature one didn't intend to use, and how to turn accidental uses of it into warnings.

[AntC2]

@goldfirere I claim (without evidence) that each language extension thus increases the cognitive burden of using Haskell (even if only slightly), and thus we should be parsimonious about them.

If I someone from the crowd may provide a sliver of evidence from personal experience ...

What makes the cognitive burden is the extra syntax and semantics -- whether that's two pieces of syntax under a single extension, or under two extensions, it's the same burden.

What's particularly burdensome is different semantics with no syntactic clue: ScopedTypeVariables should be deprecated (then taken out the back and shot) in favour of some syntactic explicit binding from sig to decl. And I fear datatype promotion without the explicit ' is in the same bucket. I'm in favour of the type/data heralds for that reason. By all means also require code using punning (unpromoted) to say so.

There's further burden because not all extensions are simply orthogonal or simply a widening of an existing extension. Example: FunDeps interact very badly with Overlapping instances. It's great to have the per-instance OVERLAPPABLE etc pragmas; if the class also has FunDeps, I have to remember to hold my jaw funny.

So for this particular proposal, it would help me reading code to know whether it's using only TypeLevelLiterals or also using datatype promotion. And having only one extension that might introduce one or the other or both is more burdensome.

[goldfirere]

@RossPaterson

It's a choice to use a subset of an extension, like GADTSyntax vs GADTs. Would a warning be a workable alternative in that case?

In that particular case: no, because GADTs implies MonoLocalBinds which alters the type inference algorithm. But in general, yes.

The warning approach may be logical when starting from DataKinds, but it seems conceptually complicated when coming from the other direction. To understand a module with TypeLevelLiterals, one would need only to consult the type-level literals section of the User's Guide. There is no need to consult the data constructor promotion section to learn about a feature one didn't intend to use, and how to turn accidental uses of it into warnings.

A fair point. My stance is also informed by my general opinion that we've gotten language growth and evolution a little bit wrong. I think all extensions that just enable new syntax (without changing the meaning of any existing programs) should be warnings. (This can be made fully backward compatible by having the existing extensions just twiddle warning flags.) The "extension" idea makes sense if we think about some common core of Haskell shared across compilers and defined in a standard. But that's not the world we're in. Instead, we have a compiler capable of dealing with quite a large language, where users restrict themselves to subsets of the large language by turning off language extensions. GHC uses all of its power to accept user programs, stopping only late-ish in the process when it discovers that a language extension is disabled.

So I'd be happy for all of DataKinds to be a warning -- or indeed two warnings, one for uses of a constructor in a type, and the other for uses of a literal in a type. These warnings can be errors by default, and we can clarify in the user's guide that a certain section applies only when a warning is off.

My end goal here is to try to reduce complexity by stating we have one Haskell. Users are free to restrict themselves to a subset of that language -- and GHC should actively support such subsetting. But it's still one language.

[simonpj]

I think *all* extensions that just enable new syntax (without changing the meaning of any existing programs) should be warnings.

Yes, I think that is a perfectly defensible position. But if we do it, let's be consistent about it. A proposal, perhaps? Simon

…

On Sun, 19 Mar 2023 at 20:58, Richard Eisenberg ***@***.***> wrote: @RossPaterson <https://github.com/RossPaterson> It's a choice to use a subset of an extension, like GADTSyntax vs GADTs. Would a warning be a workable alternative in that case? In that particular case: no, because GADTs implies MonoLocalBinds which alters the type inference algorithm. But in general, yes. The warning approach may be logical when starting from DataKinds, but it seems conceptually complicated when coming from the other direction. To understand a module with TypeLevelLiterals, one would need only to consult the type-level literals section of the *User's Guide*. There is no need to consult the data constructor promotion section to learn about a feature one didn't intend to use, and how to turn accidental uses of it into warnings. A fair point. My stance is also informed by my general opinion that we've gotten language growth and evolution a little bit wrong. I think *all* extensions that just enable new syntax (without changing the meaning of any existing programs) should be warnings. (This can be made fully backward compatible by having the existing extensions just twiddle warning flags.) The "extension" idea makes sense if we think about some common core of Haskell shared across compilers and defined in a standard. But that's not the world we're in. Instead, we have a compiler capable of dealing with quite a large language, where users restrict themselves to subsets of the large language by turning off language extensions. GHC uses all of its power to accept user programs, stopping only late-ish in the process when it discovers that a language extension is disabled. So I'd be happy for all of DataKinds to be a warning -- or indeed two warnings, one for uses of a constructor in a type, and the other for uses of a literal in a type. These warnings can be errors by default, and we can clarify in the user's guide that a certain section applies only when a warning is off. My end goal here is to try to reduce complexity by stating we have one Haskell. Users are free to restrict themselves to a subset of that language -- and GHC should actively support such subsetting. But it's still one language. — Reply to this email directly, view it on GitHub <#536 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAEOY63MOBTLVLXA74DLAH3W45XQFANCNFSM6AAAAAAQD4SQPI> . You are receiving this because you commented.Message ID: ***@***.***>

[goldfirere]

A proposal, perhaps?

In due course -- I'm essentially arguing my point of view in the parallel conversation about understanding what an extension means. I don't think a proposal pushing this one point will be all that useful until the committee can come to some agreement about why we have an extension system and how it should evolve.

[simonpj]

In due course -- I'm essentially arguing my point of view in the parallel conversation about understanding what an extension means. I don't think a proposal pushing this one point will be all that useful until the committee can come to some agreement about why we have an extension system and how it should evolve.

Yes but are you suggesting that we simply park this proposal until that larger conversation converges?

[AntC2]

@goldfirere My end goal here is to try to reduce complexity by stating we have one Haskell.

[I appreciate we're still holding our breath for Richard to adumbrate some approach.]

Reduce complexity for the compiler maintainers? Or for 'the crowd' wanting to write programs in Haskell?

Yes the compiler has to cope with the interactions of any/all extensions. Even if I restrict the code I write to a narrow dialect, I won't necessarily know/understand what extensions are used in modules I import -- indeed they might deliberately hide their implementation.

Using GHC is already problematic for those learning Haskell. Most of the educational materials introduce an unrealistically out-of-date version of Haskell; then explain extensions (via the Language pragmas) incrementally. If instead learners are to be faced with "one Haskell" everythingallatonce -- unless they actively switch off (or switch Warnings to Errors) for stuff they can't possibly understand yet -- it's going to be an even more off-putting experience. (Can the Haskell20xx setting be made to switch Warnings to Errors for the sake of learners?)

Do those outside the circle of GHC maintainers think we have "one Haskell"? For myself, I think FunDeps are a different Haskell vs Type Families; I think I might find TypeData [**] a different Haskell vs DataKinds. I think DependentHaskell breaks so many of my intuitions, it's not Haskell at all.

[**] The TypeData proposal got accepted in 2018. It's only just arrived in 9.6 last month. If it's the complexity of GHC's extension management that's slowing feature development, I guess we should just bite the bullet and give up on an extension mechanism.

[RossPaterson]

I want to defend the Haskell introduced by most educational materials. Yes, it's a long way behind GHC, but it is a subset that is fairly precisely specified, mostly stable, usable for lots of applications, and an achievable base camp for learning the newer features. Without it, GHC Haskell would be too daunting.

Once you've reached this base, it's helpful to be able to turn on features incrementally as you explore. Different users will be interested in different extensions. Addition seems more workable than subtraction here.

I don't think the delay in implementing TypeData was due to extension management. Rather, it was waiting for someone who was (a) sufficiently interested in the feature to invest the effort, and (b) sufficiently foolish to think it wouldn't be too hard. I found it quite difficult, because GHC is huge and this involved several parts of it (though only touching the edges of the type system, where the biggest dragons live), and a lot of what DataKinds is doing is somewhat obscure. The extension machinery was the least of it. The proposal process was useful in producing a fairly precise design to implement and to evaluate the implementation against before merging.

[tbidne]

@AntC2

If instead learners are to be faced with "one Haskell" everythingallatonce -- unless they actively switch off (or switch Warnings to Errors) for stuff they can't possibly understand yet -- it's going to be an even more off-putting experience. (Can the Haskell20xx setting be made to switch Warnings to Errors for the sake of learners?)

I do not believe this is necessarily true. A hypothetical GHC that does not have language pragmas would be in the same boat as every other language wrt "advanced" features: either you use a feature, or you do not. Having to preface your file (or default-extensions) with -XFeature is unnecessary noise, and imo makes the interface more complicated.

For instance, typescript has some pretty advanced type features, especially by web standards. I do not believe anyone, including beginners, would be helped by requiring users to write -XIntersectionTypes at the top of their .ts files. Indeed this type of interface imposes significant costs of its own. Not only is this one more thing users have to understand, but so too do tools (e.g. formatters, linters), and then their users have to understand the resultant idiosyncrasies. Case in point, extensions have to be passed somehow to tools like doctest and ormolu (there are multiple ways to do this), and the latter's behavior wrt the cabal file's default-extensions has changed across versions (for the better, to be clear). This sort of faff does not exist in languages where version(lang) >= N implies features X,Y,Z are available.

Of course, having new features unconditionally available can degrade the user experience when they worsen error messages or change the semantics of an existing program. Certainly the latter should be guarded behind a flag, and probably the former too (though the real solution is to fix the error messages). Thus I agree that the extension mechanism makes sense in some circumstances, but it also imposes a cost, and I think it is perfectly reasonable to consider a world where new feature do not necessarily have to be guarded behind an extension.

[AntC2]

@tbidne (those are important points for Richard's 'proposal perhaps' -- when we get to it. I'll try not to clutter this TypeLevelLiterals topic with more generic discussion, but briefly ...)

either you use a feature, or you do not

Sadly, there are some features of Haskell that come without distinctive syntax. The only way the compiler can tell whether this is an intended "advanced" piece of code vs a newbie's error is from the flag setting. (AllowAmbiguousTypes, ScopedTypeVariables -- which potentially changes the typing of a program with no clue at the usage site; OverlappingInstances/the various OVERLAP* pragmas; and I have a q following re how TypeData interacts with DataKinds in the absence of this extension.)

in the same boat as every other language

I don't see 'every other language' as trying to be all of a flagship for learning a still fairly rare programming paradigm (Functional Programming), an experimental testbed for advanced type theory, an industrial-strength compiler for high-assurance computing. (Could a newbie reasonably just jump into typescript? Or would they be expected to cut their teeth first on javascript?)

On the "experimental testbed", an extension documented as not-yet-stable means the design might change in future releases, in ways that make previously-accepted code invalid. In theory the whole feature might get withdrawn (although this has never happened in practice). So your version(lang) >= N implies ... doesn't necessarily hold.

Addit: hehe you might be hoist by your own petard with that example. Typescript docs tell me 'Intersection types' are no longer a thing/"This page has been deprecated". Looks like the switch statement on the deprecated page got withdrawn in favour of using only typeof for discriminating unions by type.

[AntC2]

Looking at the motivating example in #106,

• There's type data Character | Number | Boolean in the type namespace;
• GADT data constructors Character | Number | Boolean in the data namespace.
• Those data constructors are the promotable variety.

So with DataKinds, do I get two of each same-named types in the type namespace? That's what :info is telling me. How to distinguish between them?

It seems (to be precise, I'm at GHC 8.10, and using an EmptyDataDecl to mimic type data Number):

• Bare Number gets interpreted as the type data Number.
• I need to tick-prefix 'Number to get at the promoted GADT.
• If I have some other data constructor whose name doesn't clash with a type, I don't need to use the ' prefix.

@goldfirere Mar 10 I have a niggling feeling that we wanted to remove the ' at some point, due to the conflict with Template Haskell.

Yes, I thought there was a strong move (somewhere) towards that. And that DependentHaskell wants us to not mentally distinguish a constructor appearing in a term vs in a type (hence some pushback on the type/data heralds). BTW what does (type Number) in an expression select when there's both a type data and a promoted data constructor? Do I need ticked (type 'Number)?

-Wunticked-promoted-constructors. ... I[@goldfirere] think it exactly fits the need here.

I think what Ross is proposing here is that it's legitimate to insist promoted data constructors not be in scope at all -- not even if ticked. And having just reminded myself with this exercise/my poor monkey brain that they're rather fiddly, I agree they're something to be kept away from newbies.

[tbidne]

Addit: hehe you might be hoist by your own petard with that example. Typescript docs tell me 'Intersection types' are no longer a thing/"This page has been deprecated". Looks like the switch statement on the deprecated page got withdrawn in favour of using only typeof for discriminating unions by type.

The intersection concept still exists, though your point regarding deprecation / experimentation is well-taken.

[simonpj]

Reflecting a bit on this, and re-reading the whole thread

• Adding a language extension does have a cost, albeit a small one.
• Why should we pay that cost? Because there is a definite reason that someone might want type-level literals, but not data type promotion. I'm unconvinced by this motivation and the proposal does not really attempt to make the case.
• Even if we did want to divide up DataKinds in this way, I'd prefer to say "DataKinds implies TypeLevelLiterals and DataTypePromotion". Then you could switch on type-level literals or data type promotion, or both, independently. That seems more uniform.

On balance I now think that the (modest) pain isn't worth the (extremely modest) gain. I have seen no one saying "this change would really make my life better".

[yav]

@simonpj as I've said before I would really find this change useful, because when combined with #106, it gives me a subset of the type language that can express all the things that I need (i.e., explicitly defined kinds from #106, and type level literals from this proposal).

Personally, I have never found the design of DataKinds to match my way of thinking, and while I've used it, it is because it was the only available way of doing things, despite the difficulties it introduces. For example, I find that when defining a new kind, I rarely (never?) need to use the same type both as a value and as a type---most of the time the value level constructors are just noise that we have to work around. We also have to resort to comments to note which data declarations define kinds and which ones define actual types. A fairly common pattern in our code base are declarations like this:

data T = MyInt | MyBool

type MyInt = 'MyInt
type MyBool = 'ByBool

data TRepr :: T -> Type where
  MyIntRepr :: TRepr MyInt
  MyBoolRepr :: TRepr MyBool

Note that the type synonyms and the Repr in the constructors of TRepr are only there to work around the DataKinds.
If we were writing the code today, I'd much rather write:

type data T = MyInt | MyBool                                                     
                                                                                 
data TRepr :: T -> Type where                                                    
  MyInt  :: TRepr MyInt                                                          
  MyBool :: TRepr MyBool

For an actual example from our code base, have a look here: https://github.com/GaloisInc/crucible/blob/master/crucible/src/Lang/Crucible/Types.hs

Now, of course, thanks to Ross we have #106 implemented, so I could just write the code in the nicer form above and I am really happy about it! It just seems quite unfortunate, that if I want to index my types with type level literals, I have to turn on DataKinds again and deal with all the issues outlined above, and that's for no reason whatsoever!

[simonpj]

Thanks @yav that's really helpful. We have one person at least who positively wants this.

Can you help me a bit more: Since we now have type data, why don't you just use that plus DataKinds? Is it a significant problem (in practice) that data constructors can appear in types; you don't use that facility, to be sure, but it doesn't harm you sigificantly, does it?

[RossPaterson]

The cost of enabling a feature one isn't using is a loss from the error space. My coding mistake, e.g. getting names mixed up and using a data constructor where I meant to use a type name, is no longer a simple compiler error; now it is reported as an erroneous use of a feature I haven't learnt yet, or perhaps accepted as an accidental and unintended correct use of that feature.

[int-index]

@yav I can hardly see the point of the extra declarations in your example

data T = MyInt | MyBool

type MyInt = 'MyInt
type MyBool = 'ByBool

data TRepr :: T -> Type where
  MyIntRepr :: TRepr MyInt
  MyBoolRepr :: TRepr MyBool

Why write MyInt = 'MyInt instead of simply using the data constructor MyInt unticked? Then the example becomes

data T = MyInt | MyBool

data TRepr :: T -> Type where
  MyIntRepr :: TRepr MyInt
  MyBoolRepr :: TRepr MyBool

Now it's the same size as your example that uses type data

type data T = MyInt | MyBool                                                     
                                                                                 
data TRepr :: T -> Type where                                                    
  MyInt  :: TRepr MyInt                                                          
  MyBool :: TRepr MyBool

With the only difference being that the distinction between MyInt and MyIntRepr is reflected in the name instead of using punning to resolve it.

As far as I'm concerned, using a distinct name for MyIntRepr is actually an improvement, eliminating any potential confusion between MyInt :: T and MyInt :: TRepr MyInt. Even the declaration itself looks cyclical. MyInt :: TRepr MyInt appears self-referential until you realize that there are two distinct MyInt at play here.

But suppose you are unwilling to use a separate name for MyIntRepr because your preferred code style heavily relies on punning. That's still possible with DataKinds, right? Except that error messages are sometimes not what you want, as @RossPaterson mentions.

In other words, the motivation behind this proposal is to improve error messages in code that heavily relies on punning. Is that a correct summary? If so, could it be incorporated into the "Motivation" section of the proposal, with examples of unwanted error messages and desired error messages? Also, the "Alternatives" section should mention that a pun-free naming convention is, in fact, an alternative (it doesn't imply it's a good one, but it's there)

[RossPaterson]

I don't think punning is the issue. Suppose I'm using a type like

newtype Component a = Part a

and I get the names mixed up and use the data constructor where I meant to use the type name:

type Parts a = [Part a]

type Chapter = Part Int

Without DataKinds, both are reported as type constructor Part not in scope. With it, the first complains about kinds, while the second is accepted (until I try to use the type later).

[int-index]

Thanks for clarifying. Yes, I can see how error messages are different with DataKinds on and off regardless of punning, although I wouldn't describe either variant as "better" — this largely depends on the expectations.

In any case, the Motivation section should be very clear on the benefits of splitting off TypeLevelLiterals. Currently it simply says that not all users want the full power of DataKinds, but it doesn't show how this full power affects error messages and why it's undesirable.

Furthermore, is it about error messages only or are there other benefits? And would it be possible to improve error messages without reorganizing extension flags?