Support promoting symbolic types

[goldfirere]

GHC 8 can, so we should too. But see the comment in singInfixDecl before proceeding too far, as I don't know how to handle that function if we can promote symbolic types.

[RyanGlScott]

Silly question: what exactly constitutes a "symbolic type"? And why weren't they usable before GHC 8?

[goldfirere]

Something like data a + b = Left a | Right b. It's just about naming.

GHC 7.x couldn't deal with symbolic kinds because it couldn't parse both them and *. With quite a bit of effort, the parsing around * is "fixed" in GHC 8, allowing symbolic kinds.

[RyanGlScott]

Ah! Your original comment had me confused, since it implies this was new in GHC 8, but this feature has actually been around since GHC 7.6!

$ /opt/ghc/7.4.2/bin/ghci -XTypeOperators
GHCi, version 7.4.2: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
λ> data a + b = Left a | Right b

<interactive>:2:6:
    Malformed head of type or class declaration: a + b
λ> :q
Leaving GHCi.
$ /opt/ghc/7.6.3/bin/ghci -XTypeOperators
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
λ> data a + b = Left a | Right b
λ> 

So I suppose my next question is: what does the comment in singInfixDecl hinting at? It claims that "symbolic tycons can't be promoted", but that's surely not true?

$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :set -XTypeInType -XTypeOperators 
λ> data a + b = Left a | Right b
λ> :kind (+)
(+) :: * -> * -> *

[RyanGlScott]

Perhaps it's referring to this business?

λ> ; $(singletons [d| data a + b = L a | R b |])

<interactive>:6:5: error:
    Illegal type constructor or class name: ‘S+’
    When splicing a TH declaration:
      type S+ = (Data.Singletons.Internal.Sing :: +_0 a_1 b_2 -> *)

[RyanGlScott]

Indeed, I suppose there's been an assumption that all infix datatype names have a colon at the beginning. This assumption is encoded into the naming conventions as well:

2. original datatype: :/\:
   promoted kind: :/\:
   singleton type: :%/\:

So if you give singletons a datatype name which doesn't begin with a colon, it'll get flummoxed and produce garbage like S+.

Perhaps the rule should actually be %:/\: instead of :%/\:? That way, it would work consistently with all infix datatype names.

[RyanGlScott]

Since this is currently burning a hole in my skull, I think singletons needs an overhaul with respect to how it deals with colons. There's too many icky corner cases where inserting leading colons (#200) or leaving out colons from certain types (#226) causes problems. My proposed solution? Leave colons be. More precisely, I propose these new naming conventions for infix names:

2. original datatype: /\

   promoted kind: /\

   singleton type: %/\

3. original constructor: :+:

   promoted type: ':+:

   singleton constructor: :%+:

   symbols: :+:@#@$, :+:@#@$$, :+:@#@$$$

4. original value: +

   promoted type: +

   singleton value: %+

   symbols: +@#@$, +@#@$$, +@#@$$$

5. original class: ~>

   promoted class: #~>

   singleton class: %~>

Notice that the only case where we care about colons is the constructor case (since we have to put the % after the colon), but that's only because Haskell's syntax demands it. For other cases, we simply prepend/append the appropriate symbols, regardless of whether colons are used or not. Much simpler, and in addition to fixing this issue, it would also fix #200, as we would be able to unambiguously create kind-inference constructors by just prepending : and appending ###.

There are two downsides to this proposal:

1. There'd be quite a bit of API churn. But we've already broken the API in the upcoming release with Eliminate the dollar sign hack #203, so this doesn't bother me so much. (Plus, we'd go back from :$ to $ for type-level application, so we'd partially un-break the API!)
2. Some of the type families from GHC.TypeLits (+, -, *, etc.) would now clash with their counterparts in Data.Singletons.Prelude.Num. I suppose we could simply add a disclaimer to the top of Data.Singletons.Prelude.Num indicating the danger of importing it alongside GHC.TypeLits.

[goldfirere]

If it's really a simplification, go for it. A highly experimental library like singletons can get away with this kind of (actually, rather easy to fix) breakage.

It is interesting that a + function gets promoted to a + type family. This is different than what happens for identifiers, where the function and type family have different names. This is OK, of course.

As for drawback (2), that's not so bad, because the Num exports subsume the TypeLits ones, anyway -- right?