Dear Committee,
Ross Paterson has proposed #536 "Type-level literals as a separate language extension". Read it here:
https://github.com/RossPaterson/ghc-proposals/blob/literals/proposals/0000-type-level-literals.rstCurrently the DataKinds extension allows us to use both type-level literals (such as "hello", 'x', and 42) and promoted algebraic data constructors (such as True, Just, and '[]). The proposal is to factor out promotion of literals into its own extension, TypeLevelLiterals.
Why would one want to enable TypeLevelLiterals but not DataKinds? Because the latter can create ambiguities when it comes to name resolution. If the user defines `data Just x = ...` and they have DataKinds enabled, then suddenly it's ambiguous whether `Just` refers to a data constructor or a type constructor, and GHC starts to guess from context. Type-level literals, on the other hand, are a more conservative subset of DataKinds that does not raise any questions with regards to name resolution.
While I, personally, would not use this conservative subset, I believe we shouldn't create obstacles for those who want to. I expect the maintenance costs to be minimal.
Does anyone have objections? If not, I will mark the proposal accepted in 2 weeks.
- Vlad