[GHC] #11342: Character kind

[GHC]

#11342: Character kind
-------------------------------------+-------------------------------------
        Reporter:  alexvieth         |                Owner:  alexvieth
            Type:  feature request   |               Status:  patch
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:  DataKinds
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #10776, #12162    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Before looking at implementation, let's think about design: Is there any
 reason the kind shouldn't be `Char`? `Symbol` is actually different from
 `String` (the former is monolithic while the latter is a list) and `Nat`,
 when it was invented, was different from any term-level type. But neither
 of these arguments apply to `Char`.

 I'm also trying to be forward thinking about naming. In my thoughts about
 DependentHaskell, I've envisioned using the `'` promotion operator (which
 already exists for data constructors) to promote term-level variables. In
 this way, instead of `ToUpper`, we would have `'toUpper`. Unlike with data
 constructors, the quote would be mandatory, because otherwise `toUpper`
 would look like a type variable.

 Of course, we don't have DependentHaskell and I wouldn't want this rather
 independent work to become dependent on DependentHaskell. But a small
 tweak now could make things line up nicely later.

 '''Proposal:'''
 * In a type, parse `'`''varid'' as a ''conid''.

 That means that a use of, say, `'foo` in a type would be in the same
 syntactic category as `Foo`. In particular, you would be able to say

 {{{
 type family 'toUpper (c :: Char) :: Char
 }}}

 Before we have DependentHaskell, all of the `Data.Char` operations would
 indeed have to be re-implemented one level up. But if we name them
 according to this scheme, then when we do have DependentHaskell, we don't
 have to break all the code that uses promoted characters. My expectation
 would be that the type family declaration above would no longer work --
 the type-level definition would be promoted from the term-level definition
 -- but clients don't need to change. Thoughts?

 As for the implementation, I'm sorry to be annoying, but could you post
 the patch to Phab? It's just so much easier to read there and comment on.
 Thanks.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11342#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler