Promote GADTs

[int-index]

Given inductively defined naturals data N = Z | S N we can define finite sets as follows:

data Fin :: N -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

If I wrap the above definition in singletons [d| |] I get these errors:

R.hs:23:1: error:
    • Expected kind ‘N’, but ‘a0’ has kind ‘*’
    • In the first argument of ‘Fin’, namely ‘a_ap1v’
      In the first argument of ‘SingKind’, namely ‘Fin a_ap1v’
      In the instance declaration for ‘SingKind (Fin a_ap1v)’

R.hs:23:1: error:
    • Expected kind ‘Fin a0’, but ‘'FS n1’ has kind ‘Fin ('S n0)’
    • In the definition of data constructor ‘SFS’
      In the data instance declaration for ‘Sing’

Instead I'd expect these definitions to be generated:

data instance Sing (fn :: Fin n) where
  SFZ :: Sing FZ
  SFS :: Sing fn -> Sing (FS fn)

instance SingKind (Fin n) where
  type DemoteRep (Fin n) = Fin n
  toSing = \case
    FZ -> SomeSing SFZ
    FS fn -> case toSing fn of
      SomeSing sfn -> SomeSing (SFS sfn)
  fromSing = \case
    SFZ -> FZ
    SFS sfn -> FS (fromSing sfn)

[goldfirere]

This would be nice, I agree. I think it's possible, too. If you describe your use cases (and what you have to write by hand to work around), that would motivate me. Thanks!

[int-index]

I've tackled this issue and there's a blocker: Demote. Parameters to GADTs are often of kinds other than *, or even kind-polymorphic, so that's what we've got to solve first.

Consider a simpler example: singletonizing kind-polymorphic Proxy. Say I write this:

$(singletons [d|
  data Prox (a :: k) = P
  |])

Right now (with minor modifications I introduced to preserve the kind annotation) this results in the following splice:

    data Prox_a2mSb (a_a2mSe :: k_a2mSd) = P_a2mSc
    type PSym0 = P_a2mSc
    data instance Sing (z_a2mSg :: Prox_a2mSb (a_a2mSe :: k_a2mSd))
      = z_a2mSg ~ P_a2mSc => SP
    type SProx = (Sing :: Prox_a2mSb (a_a2mSe :: k_a2mSd) -> Type)
    instance SingKind (a_a2mSe :: k_a2mSd) =>
             SingKind (Prox_a2mSb (a_a2mSe :: k_a2mSd)) where
      type Demote (Prox_a2mSb (a_a2mSe :: k_a2mSd)) = Prox_a2mSb (Demote (a_a2mSe :: k_a2mSd))
      fromSing SP = P_a2mSc
      toSing P_a2mSc = SomeSing SP
    instance SingI P_a2mSc where
      sing = SP

This almost works. The error GHC gives me is this:

poly.hs:8:3: error:
    • Expected a type, but ‘a0’ has kind ‘k0’
    • In the first argument of ‘SingKind’, namely
        ‘(a_a2mTX :: k_a2mTW)’
      In the instance declaration for
        ‘SingKind (Prox (a_a2mTX :: k_a2mTW))’

Indeed, we apply SingKind and Demote to the parameter of Prox, but this parameter is kind-polymorphic, whereas SingKind and Demote expect something of kind *. If I was to write this code by hand, I'd simply remove those:

data Prox (a :: k) = P

type PSym0 = 'P

data instance Sing (z :: Prox (a :: k)) =
  z ~ 'P => SP

type SProx = (Sing :: Prox (a :: k) -> Type)

instance SingKind (Prox (a :: k)) where
  fromSing SP = P
  toSing P = SomeSing SP

instance SingI 'P where
  sing = SP

I started to ponder when it's fine to omit SingKind and Demote but haven't come to a conclusion. At first glance this is possible when type parameter is phantom.

However, if we have Prox Integer, its singletonization will be SProx (p :: Prox Integer) instead of SProx (p :: Prox Nat). I can't grasp all of the consequences of this choice when it comes to nominal equality. Will it prevent singletonization of code that uses Proxy to specify a type parameter (instead of TypeApplications?).

And if the type variable is not phantom but nominal, this means a type family could've been applied to it, so depending on our choice to apply Demote or not, this type family could give different results:

type family F (a :: k) :: * where
  F Nat     = Void
  F Integer = ()

data T (a :: k) = C (F a)

The only simple and consistent solution I see is to get rid of Demote entirely and make singletonization more parametric. That is, fromSing :: Sing (a :: k) -> k and toSing :: k -> SomeSing k shall not apply any transformations to the kind k. This would require the following steps:

• make Type inhabited at term-level by TypeRep to support TypeableT as singletons.
• make Nat and Symbol inhabited at term-level by Natural and String respectively to support singletons for type-lits.
• implement Partially applied type families ghc-proposals/ghc-proposals#52 to support singletons for functions

All of this seems far off, but worthwhile.

[RyanGlScott]

Thanks for looking into this, @int-index.

Here's another question for you: if you restrict yourself to GADTs which have monomorphic kinds, does the problem become easier? That is, would it be possible to single/promote a GADT like:

data Foo (a :: Type) where
  MkFoo :: Foo Bool

Without some of the pain points you described in #150 (comment)?

[int-index]

if you restrict yourself to GADTs which have monomorphic kinds, does the problem become easier?

Yes, then we could figure out when to apply Demote and when not to. We could apply Demote to all parts of the type that have kind *:

type Demote (Foo a) = Foo (Demote a) -- because `a` has kind `*`
type Demote (Fin n) = Fin n -- because `n` has kind `Nat`

[int-index]

For a length-indexed vector:

type Demote (Vec n a) = Vec n (Demote a)

For higher-order kinds I don't know what to do. If we have Foo :: (* -> X) -> *, we might want to do something like this:

type Demote (Foo f) = Foo (f . Demote)

where . denotes function composition on type level. But this would be a partial application of Demote — not possible.

[goldfirere]

Really, the problem here is that we don't do type inference. The SingKind constraints are necessary for every type used as a data constructor argument. I've cheated by just making constraints for all type parameters, but this isn't really right. So perhaps an improvement is to do just that: walk through all the constructors to get all the SingKind constraints.

Demote can be fixed by making it kind-polymorphic. This would have to remove it from the SingKind class, but that's OK. I actually think all of this shouldn't be too bad. But I've spent out my time budget on singletons for now...

[RyanGlScott]

To help me understand better what changes would be needed here, can you help me hand-write the singled version of the Foo datatype in #150 (comment)?

@int-index suggests in #150 (comment) that the Demote instance we'd need for Foo is type Demote (Foo a) = Foo (Demote a). That's great, because that's what singletons already tries out of the box:

    singletons
      [d| data Foo_a3Eb (a_a3Ed :: Type)
            where MkFoo_a3Ec :: Foo_a3Eb Bool |]
  ======>
    data Foo_a6nX (a_a6nZ :: Type) where MkFoo_a6nY :: Foo_a6nX Bool
    type MkFooSym0 = MkFoo_a6nY
    data instance Sing (z_a6o1 :: Foo_a6nX a_a6nZ)
      = z_a6o1 ~ MkFoo_a6nY => SMkFoo
    type SFoo = (Sing :: Foo_a6nX a_a6nZ -> Type)
    instance SingKind a_a6nZ => SingKind (Foo_a6nX a_a6nZ) where
      type Demote (Foo_a6nX a_a6nZ) = Foo_a6nX (Demote a_a6nZ)
      fromSing SMkFoo = MkFoo_a6nY
      toSing MkFoo_a6nY = SomeSing SMkFoo
    instance SingI MkFoo_a6nY where
      sing = SMkFoo

But obviously it couldn't be that easy. Here's the error that the above splice gives you:

    • Expected kind ‘Foo a0’, but ‘'MkFoo’ has kind ‘Foo Bool’
    • In the definition of data constructor ‘SMkFoo’
      In the data instance declaration for ‘Sing’

This makes sense: we're trying to claim that z_a6o1 ~ MkFoo_a6nY, but those two things have different kinds. We should be able to patch this up with heterogeneous equality:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind
import Data.Singletons.Prelude
import Data.Type.Equality

data Foo (a :: Type) where MkFoo :: Foo Bool
type MkFooSym0 = MkFoo
data instance Sing (z :: Foo a)
  = (z ~~ MkFoo) => SMkFoo
type SFoo = (Sing :: Foo a -> Type)
instance SingKind a => SingKind (Foo a) where
  type Demote (Foo a) = Foo (Demote a)
  fromSing SMkFoo = MkFoo
  toSing MkFoo = SomeSing SMkFoo
instance SingI MkFoo where
  sing = SMkFoo

But this leads to another error:

[1 of 1] Compiling Foo              ( Foo.hs, interpreted )

Foo.hs:19:18: error:
    • Could not deduce: a ~ Bool
      from the context: Demote a ~ Bool
        bound by a pattern with constructor: MkFoo :: Foo Bool,
                 in an equation for ‘toSing’
        at Foo.hs:19:10-14
      ‘a’ is a rigid type variable bound by
        the instance declaration at Foo.hs:16:10-39
      Expected type: SomeSing (Foo a)
        Actual type: SomeSing (Foo Bool)
    • In the expression: SomeSing SMkFoo
      In an equation for ‘toSing’: toSing MkFoo = SomeSing SMkFoo
      In the instance declaration for ‘SingKind (Foo a)’
    • Relevant bindings include
        toSing :: Demote (Foo a) -> SomeSing (Foo a) (bound at Foo.hs:19:3)
   |
19 |   toSing MkFoo = SomeSing SMkFoo
   |                  ^^^^^^^^^^^^^^^

At this point, I'm stuck. Any suggestions?

[int-index]

@RyanGlScott Check out my changeset here: int-index@e39178b

With it in place, I managed to compile this code:

{-# OPTIONS -ddump-splices #-}

{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, GADTs, InstanceSigs, UndecidableInstances #-}

module Singletons.PolyKindsApp where

import Data.Singletons.TH hiding (Proxy(..))

$(singletons [d|
  data Proxy (a :: k) = Proxy

  pId :: Proxy (a :: k) -> Proxy (a :: k)
  pId p = p

  |])

However, changing the type signature of pId to pId :: Proxy (t :: k) -> Proxy (t :: k) (yep, just a renaming of a to t) exposes a GHC bug:

poly.hs:9:3: error:
    • GHC internal error: ‘t_a2mVi’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [a2mVh :-> Type variable ‘k_a2mVh’ = k_a2mVh]
    • In the first argument of ‘Proxy’, namely ‘(t_a2mVi :: k_a2mVh)’
      In the kind ‘Proxy (t_a2mVi :: k_a2mVh)’
      In the type signature:
        sPId :: forall (t_a2mVv :: Proxy (t_a2mVi :: k_a2mVh)).
                Sing t_a2mVv
                -> Sing (Apply PIdSym0 t_a2mVv :: Proxy (t_a2mVi :: k_a2mVh))

This is a TemplateHaskell issue: inserting the generated splice by hand works! If you could help me identify what causes the trouble, I suppose the promotion of GADTs is a matter of generating more Demote instances. By "more" I mean that now for each kind we have something like this:

type instance Demote (Nat :: Type) = Integer

but we'll also need this:

type instance Demote (n :: Nat) = n

[int-index]

Oh, I see, you're dealing with a different problem now. Sorry, the comment above talks about poly-kinded Demote (what @goldfirere suggested).

[int-index]

@RyanGlScott Your handwritten Sing instance for Foo looks correct to me. My first instinct would be to add a ~ Demote a to the instance context of SingKind to satisfy the compiler:

instance (a ~ Demote a, SingKind a) => SingKind (Foo a) where

And indeed, this works for your definition of Foo. However, consider singletonization of a GADT like this:

data Quux (a :: Type) where
  MkFoo :: Quux Integer
  MkBar :: Quux Nat

If you add the same constraint, MkBar won't be accessible. Maybe Demote is a blocker after all :(

[int-index]

One could think that it would be fine to remove the application of Demote to the parameter of Quux altogether:

{-# OPTIONS -ddump-splices #-}

{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, GADTs, InstanceSigs, UndecidableInstances #-}

module Singletons.Foo where

import Data.Kind
import Data.Singletons.TypeLits
import Data.Singletons.Prelude
import Data.Singletons.TH

data Quux (a :: Type) where
  MkFoo :: Quux Integer
  MkBar :: Quux Nat

data instance Sing (z :: Quux a) where
  SMkFoo :: Sing (MkFoo :: Quux Integer)
  SMkBar :: Sing (MkBar :: Quux Nat)

type SQuux = (Sing :: Quux a -> Type)

type instance Demote (Quux a) = Quux a

instance (SingKind a) => SingKind (Quux a) where
  fromSing = \case
    SMkFoo -> MkFoo
    SMkBar -> MkBar
  toSing = \case
    MkFoo -> SomeSing (SMkFoo :: Sing (MkFoo :: Quux Integer))
    MkBar -> SomeSing (SMkBar :: Sing (MkBar :: Quux Nat))

instance SingI MkFoo where
  sing = SMkFoo

instance SingI MkBar where
  sing = SMkBar

and yeah, it compiles. However, consider a use of Foo like this:

data QSigma (a :: Type) where
  QSigma :: Quux a -> a -> QSigma a

if you singletonize QSigma, you get this definition:

data instance Sing (z :: QSigma a) where
  SQSigma :: Sing (t :: Quux a) -> Sing (p :: a) -> Sing (z :: QSigma a)

and SomeSing (QSigma a) is not isomorphic to QSigma a! Notice that Sing (p :: a) is inhabited for a ~ Nat, whereas Nat itself isn't. QSigma MkBar can have only bottom as its second field, but SQSigma SMkBar can have any integer (e.g. sing :: Sing 42).

[RyanGlScott]

@int-index, thanks for the advice! The Demote a ~ a trick is interesting, I'll have to give that more thought.

Also, great job at finding the bug in #150 (comment). I've reported this as GHC Trac #13782.

[goldfirere]

It looks like we need an inverse of Demote:

type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where ...

Also, to flesh out my polykinded Demote idea:

type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a

type instance Promote Type = Type
instance SingKind Type where
  type Demote Type = Type
  fromSing = error "fromSing Type"
  toSing = error "toSing Type"

I tested my ideas in the following, and it compiles (did not import Data.Singletons):

data family Sing (a :: k)
class SingI (a :: k) where
  sing :: Sing a

data SomeSing (k :: Type) where
  SomeSing :: Sing (a :: k) -> SomeSing k

type family Promote k :: Type

class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
  type Demote k :: Type
  fromSing :: Sing (a :: k) -> Demote k
  toSing :: Demote k -> SomeSing k

data instance Sing (b :: Bool) where
  SFalse :: Sing False
  STrue  :: Sing True

instance SingI True where
  sing = STrue
instance SingI False where
  sing = SFalse

type instance Promote Bool = Bool

instance SingKind Bool where
  type Demote Bool = Bool

  fromSing STrue = True
  fromSing SFalse = False

  toSing True = SomeSing STrue
  toSing False = SomeSing SFalse

type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a

type instance Promote Type = Type

instance SingKind Type where
  type Demote Type = Type
  fromSing = error "fromSing Type"
  toSing   = error "toSing Type"

data Foo (a :: Type) where MkFoo :: Foo Bool
type MkFooSym0 = MkFoo
data instance Sing (z :: Foo a)
  = (z ~~ MkFoo) => SMkFoo
type SFoo = (Sing :: Foo a -> Type)
type instance Promote (Foo a) = Foo (Promote a)
instance SingKind a => SingKind (Foo a) where
  type Demote (Foo a) = Foo (Demote a)
  fromSing SMkFoo = MkFoo
  toSing MkFoo = SomeSing SMkFoo
instance SingI MkFoo where
  sing = SMkFoo

[RyanGlScott]

Ooh, that looks really nice. Is the idea that the algorithm for coming up Demote instances would now become:

type Demote (T a1 ... an) = T (DemoteX a1) ... (DemoteX an)

And that for each data type, you'd also stub out an instance of the form:

type instance DemoteX (t :: T a1 ... an) = t

And would you need a kind-polymorphic PromoteX type family as well, with similarly stubbed out instances?

BTW, this design helped me find another GHC bug: Trac #13790. Isn't singletons great? :)