Make Sing a type family

[RyanGlScott]

This fixes #318 by switching Sing from a data family to a type family. There are several knock-on changes as a result of this switch—refer to CHANGES.md for an overview.

[int-index]

I was initially opposed to the change, but then I realized: the important part of this encoding is that it says

type family Sing :: k -> Type

rather than

type family Sing (a :: k) :: Type    -- (and perhaps some injectivity annotations)

This means we can still partially apply Sing.

Would be good to see a mention of this in the docs (or a Note)

[int-index]

I wonder, would this injectivity annotation make any difference?

type family Sing = (r :: k -> Type) | r -> k

[RyanGlScott]

I've just added a Note [The kind of Sing] underneath the definition of Sing which explains why we don't pick something like type family Sing (a :: k).

I wonder, would this injectivity annotation make any difference?

It wouldn't. Since Sing is declared to have return kind k -> Type, it is automatically an injective type constructor as a consequence, so an injectivity declaration would be redundant. (I explain this in Note [The kind of Sing] as well.)

[RyanGlScott]

Since this is a nontrivial redesign of some of singletons' fundamentals, I'm currently doing some smoke-testing of other libraries that depend on singletons to see if there are other problems that I didn't anticipate. In this process, I did encounter one small wrinkle that I overlooked when I wrote this patch. Previously, singletons would generate this data family instance:

data instance Sing :: D a -> Type where

It now generated this equivalent data type:

data SD :: D a -> Type

At least, I had previously convinced myself that they were equivalent. But I now realize that there's actually a subtle difference between the two in that the latter type does not have a CUSK! Data family instances don't really have an equivalent of CUSKs, but since data families themselves always have CUSKs, it not too much of a stretch to say that former type does have a CUSK.

That being said, given that singletons doesn't really support singling GADTs at the moment, I can't think of any singletons code that you can successfully compile today where the lack of a CUSK would be an issue. On the other hand, I do have a singleton-gadts repo—which piggybacks off of singletons' Template Haskell machinery—that fails to compile with this patch. That's because singleton-gadts tries to generate (or rather, the underlying singletons machinery tries to generate) the following data type:

data (%:~:) :: a :~: b -> Type where
  SRefl :: (%:~:) Refl

Lacking a CUSK, (%:~:) fails to compile. Granted, I could take the singletons-generated Dec and manually insert the forall a b. into (%:~:)'s kind post facto, but it feels like it would be much more direct to do this in singletons itself. Unless someone feels strongly otherwise, I think I will go ahead and do so.

[goldfirere]

A very quick gander at the code makes this look quite a bit easier than I would have thought. Cool. I'm in full support of this change, unsurprisingly. :)

[RyanGlScott]

Hm, it turns out that @mstksg's decidable library doesn't compile with this patch either. Here is a boiled-down example:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind
import Data.Singletons
import Data.Singletons.Decide

type Predicate k = k ~> Type
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
type Evident = (TyPred Sing :: Predicate k)
type Decide p = forall a. Sing a -> Decision (p @@ a)

class Decidable p where
    decide :: Decide p
instance Decidable Evident where
    -- decide = Proved . prove @Evident

With Sing-as-a-type-family, this fails to compile with:

Foo.hs:20:10: error:
    • Illegal type synonym family application ‘Sing’ in instance:
        Decidable Evident
    • In the instance declaration for ‘Decidable Evident’
   |
20 | instance Decidable Evident where
   |          ^^^^^^^^^^^^^^^^^

(That error message isn't great, but there's a use of Sing buried underneath the Evident type synonym.)

This worries me a bit, since I'm not exactly sure how one would port over this code. Thoughts, @mstksg?

[mstksg]

i'll look into it and see. the main issue is using a type family as an instance, right? So instance Decidable (TyPred1 Sing) cannot be defined for all singletons, huh.

We may be able to get around the issue by using a newtype wrapper and writing the instance over that. I'll try to see if I can get something that works.

[RyanGlScott]

Yes, I suspect that recommending the use of a newtype wrapper around Sing may be the best path forward here. I was planning to introduce such a WrappedSing separately (as part of a fix for #366) as an optional goodie for power users, but it didn't occur to me until now that WrappedSing might be required for some use cases (such as decidable's).

[RyanGlScott]

@mstksg, I've just pushed a change which adds a WrappedSing newtype around Sing. With this, it may be possible to define things like type Evident = (TyPred WrappedSing :: Predicate k)—let me know if this is sufficient for your needs.

[RyanGlScott]

Ping @mstksg. Do note that I'm essentially holding back this PR until I receive some an indication of some kind from you that this will (or won't) work out for your needs, so if you'd like to see this feature land, your feedback would be appreciated :)

[mstksg]

Ah, I was going to look deeper into this last week, but things did come up. It's a bit difficult for me to test right now because I need to set up a pipeline to test with GHC head :) I think if a newtype wrapper or some other workaround is possible, decidable would be okay for it. Overall the ergonomics of general singletons usage is a higher priority for me at this moment! I can't promise a specific day I can get to this, so feel free to move past me if you want to move things along :)

[RyanGlScott]

No worries. I'm not in a huge hurry to merge this, especially since it there's still time before we even see a release candidate of GHC 8.8.1 (we're still in the alpha stage). Also, us folks at the #ghc IRC channel would be happy to help get you set up with a GHC HEAD configuration—it's much less painful than it used to be, I promise :)

[RyanGlScott]

FWIW, I've pushed a fork of decidable which shows one possible way of making it work with WrappedSing. (There are still some questions you would need to decide as far as which places should use Sing and which places should use WrappedSing, but each possible design is the same up to wrapping/unwrapping newtypes.)

[mstksg]

Thanks for this :) Looking over the changes, it all seems like a very reasonable interface. The only time someone would need to deal with wrapping is Evident, I think. And also with sing as a type family, we can get rid of SIndex' completely, right? and just use type Sing (Index as a) = SIndex as a, hopefully!

[RyanGlScott]

And also with sing as a type family, we can get rid of SIndex' completely, right?

Indeed. I've pushed a commit which demonstrates one way to do this.

[RyanGlScott]

Judging from recent comments (especially #393 (comment)) and from the general quiescence of the discussion on this PR, it looks like we have come to a consensus that this is the right approach. In light of this, I'm going to merge this. Please speak up if you feel otherwise!