search

goldfirere / singletons

Fake dependent types in Haskell using singletons
287 stars 36 forks source link

Promote GADTs #150

Open int-index opened 8 years ago

int-index commented 8 years ago

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 commented 7 years ago

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 commented 7 years ago

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:

All of this seems far off, but worthwhile.

RyanGlScott commented 7 years ago

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 https://github.com/goldfirere/singletons/issues/150#issuecomment-305148738?

int-index commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 https://github.com/goldfirere/singletons/issues/150#issuecomment-305499354?

@int-index suggests in https://github.com/goldfirere/singletons/issues/150#issuecomment-305521844 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 commented 7 years ago

@RyanGlScott Check out my changeset here: https://github.com/int-index/singletons/commit/e39178bfbf9255177aad38baf2e5642196807835

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 commented 7 years ago

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 commented 7 years ago

@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 commented 7 years ago

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 commented 7 years ago

@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 https://github.com/goldfirere/singletons/issues/150#issuecomment-305909199. I've reported this as GHC Trac #13782.

goldfirere commented 7 years ago

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 commented 7 years ago

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? :)

goldfirere commented 7 years ago

DemoteX and PromoteX (yes, we'll need that too, I suppose) should be fully recursive everywhere. This means not using the "stubbed out" instances Ryan has proposed, but instead to recur on all arguments of data constructors.

I think.

RyanGlScott commented 7 years ago

Interesting! Using this approach, I was able to create singletons for every GADT discussed in this thread (see this gist).

...well, almost. I cheated when I got to Fin and Vec, since the type parameters of kind N gave me trouble. Here's the code I have for Fin, for instance:

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

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

type instance Demote (Fin n) = Fin n -- Fin (DemoteX n)
type instance Promote (Fin n) = Fin n -- Fin (PromoteX n)

instance SingKind (Fin n) where
  fromSing SFZ = FZ
  fromSing (SFS sfn) = FS (fromSing sfn)

  toSing FZ = SomeSing SFZ
  toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')

$(return [])
type instance DemoteX FZ = FZ
type instance DemoteX (FS n) = FS (DemoteX n)
type instance PromoteX FZ = FZ
type instance PromoteX (FS n) = FS (PromoteX n)

instance SingI FZ where
  sing = SFZ

instance SingI fn => SingI (FS fn) where
  sing = SFS sing

Notice that the definitions that the algorithm would have came up with for Demote and Promote are commented out, because if you use them, you get some perplexing errors:

GADTSingletons.hs:324:10: error:
    • Couldn't match type ‘PromoteX (DemoteX n)’ with ‘n’
        arising from the superclasses of an instance declaration
    • In the instance declaration for ‘SingKind (Fin n)’
    |
324 | instance SingKind (Fin n) where
    |          ^^^^^^^^^^^^^^^^

GADTSingletons.hs:328:15: error:
    • Could not deduce: n ~ 'S n0
      from the context: DemoteX n ~ 'S n2
        bound by a pattern with constructor:
                   FZ :: forall (n :: N). Fin ('S n),
                 in an equation for ‘toSing’
        at GADTSingletons.hs:328:10-11
      ‘n’ is a rigid type variable bound by
        the instance declaration at GADTSingletons.hs:324:10-25
      Expected type: SomeSing (Fin n)
        Actual type: SomeSing (Fin ('S n0))
    • In the expression: SomeSing SFZ
      In an equation for ‘toSing’: toSing FZ = SomeSing SFZ
      In the instance declaration for ‘SingKind (Fin n)’
    • Relevant bindings include
        toSing :: Demote (Fin n) -> SomeSing (Fin n)
          (bound at GADTSingletons.hs:328:3)
    |
328 |   toSing FZ = SomeSing SFZ
    |               ^^^^^^^^^^^^

GADTSingletons.hs:329:33: error:
    • Could not deduce: DemoteX n1 ~ n2
      from the context: DemoteX n ~ 'S n2
        bound by a pattern with constructor:
                   FS :: forall (n :: N). Fin n -> Fin ('S n),
                 in an equation for ‘toSing’
        at GADTSingletons.hs:329:11-15
      Expected type: Demote (Fin n1)
        Actual type: Fin n2
      The type variable ‘n1’ is ambiguous
    • In the first argument of ‘withSomeSing’, namely ‘fn’
      In the expression: withSomeSing fn (\ fn' -> SomeSing $ SFS fn')
      In an equation for ‘toSing’:
          toSing (FS fn) = withSomeSing fn (\ fn' -> SomeSing $ SFS fn')
    • Relevant bindings include
        fn :: Fin n2 (bound at GADTSingletons.hs:329:14)
    |
329 |   toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')
    |                                 ^^

GADTSingletons.hs:329:45: error:
    • Could not deduce: n ~ 'S n1
      from the context: DemoteX n ~ 'S n2
        bound by a pattern with constructor:
                   FS :: forall (n :: N). Fin n -> Fin ('S n),
                 in an equation for ‘toSing’
        at GADTSingletons.hs:329:11-15
      ‘n’ is a rigid type variable bound by
        the instance declaration at GADTSingletons.hs:324:10-25
      Expected type: SomeSing (Fin n)
        Actual type: SomeSing (Fin ('S n1))
    • In the expression: SomeSing $ SFS fn'
      In the second argument of ‘withSomeSing’, namely
        ‘(\ fn' -> SomeSing $ SFS fn')’
      In the expression: withSomeSing fn (\ fn' -> SomeSing $ SFS fn')
    • Relevant bindings include
        fn' :: Sing a (bound at GADTSingletons.hs:329:38)
        toSing :: Demote (Fin n) -> SomeSing (Fin n)
          (bound at GADTSingletons.hs:328:3)
    |
329 |   toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')
    |                                             ^^^^^^^^^^^^^^^^^^

Any ideas what this means?

goldfirere commented 7 years ago

This just needs more types.

type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)  -- hetero is important; otherwise, GHC can't be sure that the kinds respect the Promote/Demote property
instance SingKindX n => SingKind (Fin n) where ...

worked for me.

My whole file is below:

data N = Z | S N

data instance Sing (a :: N) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)

data family Sing (a :: k)

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

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

withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing x k
  = case toSing x of
      SomeSing sx -> k sx

type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k

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

type instance PromoteX (k :: Type) = Promote k
type instance DemoteX (k :: Type) = Demote k

type instance Demote Type = Type
type instance Promote Type = Type

class SingKindX k => SingKind k where
  fromSing :: Sing (a :: k) -> Demote k

  toSing :: Demote k -> SomeSing k

type instance Promote N = N
type instance Demote N = N

type instance PromoteX Z = Z
type instance PromoteX (S n) = S (PromoteX n)

type instance DemoteX Z = Z
type instance DemoteX (S n) = S (DemoteX n)

instance SingKind N where
  fromSing SZ = Z
  fromSing (SS n) = S (fromSing n)

  toSing Z = SomeSing SZ
  toSing (S n) = withSomeSing n $ \sn -> SomeSing (SS sn)

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

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

type instance Promote (Fin n) = Fin (PromoteX n)
type instance Demote (Fin n) = Fin (DemoteX n)

type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)

instance SingKindX n => SingKind (Fin n) where

  fromSing SFZ = FZ
  fromSing (SFS sfn) = FS (fromSing sfn)

  toSing FZ = SomeSing SFZ
  toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')

$(return [])
type instance DemoteX FZ = FZ
type instance DemoteX (FS n) = FS (DemoteX n)
type instance PromoteX FZ = FZ
type instance PromoteX (FS n) = FS (PromoteX n)

instance SingI FZ where
  sing = SFZ

instance SingI fn => SingI (FS fn) where
  sing = SFS sing
RyanGlScott commented 7 years ago

@goldfirere, thanks! I've updated the gist accordingly. This technique even works for poly-kinded things such as @int-index's Prox in https://github.com/goldfirere/singletons/issues/150#issuecomment-305148738.

This. Is. Awesome.

The only thing I couldn't figure out how to do was function kinds like @int-index alluded to in https://github.com/goldfirere/singletons/issues/150#issuecomment-305523495. I figure that we'll probably need Demote and Promote instances like this:

type instance Demote (k1 ~> k2) = Demote k1 -> Demote k2
type instance Promote (k1 -> k2) = Promote k1 ~> Promote k2

I then tried coming up with suitable DemoteX and PromoteX instances for SLambda, but I quickly got stuck...

goldfirere commented 7 years ago

Note that the Demote instance above is already here.

I'm note sure what your last comment refers to.

RyanGlScott commented 7 years ago

I'm note sure what your last comment refers to.

How would you write a DemoteX instance for something of kind Demote k1 ~> Demote k2?

goldfirere commented 7 years ago

Ah -- now I understand. You wouldn't. :)

Maybe once #82 is done a way forward will present itself. But perhaps not.

Even without promoting/demoting SLambda, this is still quite useful, no?

RyanGlScott commented 7 years ago

Even without promoting/demoting SLambda, this is still quite useful, no?

Certainly! I was just wondering if it was possible to cleanly singletonize arrow-kinded things like in https://github.com/goldfirere/singletons/issues/150#issuecomment-305523495 (I have a use case for this involving GHC.Generics, which has a lot of datatypes with parameters of kind * -> *), but as you say, it would probably require fixing #82 to accomplish that.

Icelandjack commented 7 years ago

I haven't read the discussion

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.

We have https://ghc.haskell.org/trac/ghc/ticket/12369 now, edit I don't think this is relevant, nvm

RyanGlScott commented 6 years ago

Ah, blast. The poly-kinded example in https://github.com/goldfirere/singletons/issues/150#issuecomment-305148738 no longer works in GHC 8.4 due to Trac #14441.

EDIT: And now it's fixed in GHC 8.6! Never mind.

RyanGlScott commented 6 years ago

If you want to try out the design in https://github.com/goldfirere/singletons/issues/150#issuecomment-306539091 more, I have a singleton-gadts package (not yet released on Hackage) with Template Haskell functionality to quickly generate the boilerplatey parts. (I wouldn't advocate merging this into singletons proper yet due to the unsightly workarounds one has to employ to avoid Trac #12088.)

RyanGlScott commented 5 years ago

One thing that I realized recently is that, AFAICT, the only thing blocking singletons from being able to handle GADTs at the moment is SingKind. Perhaps we don't have to let this SingKind issue block us from being able to other useful things with GADTs. I'm envisioning some sort of option (in the style of #204) that makes singletons/genSingletons/etc. generate all of the code it normally does except for SingKind instances.

goldfirere commented 5 years ago

Unless there's a crying need, I would personally hold off. Things seem to be getting closer and closer to fixing GHC's dreaded #12088, so perhaps the extra work needed to suppress the instances will be wasted.

RyanGlScott commented 5 years ago

Even if we possessed the ability to define and use SingKind as described in this issue, I'm still skeptical that singletons' TH machinery will generate the desired instances 100% of the time. As one data point in support of this claim, someone filed an issue because the generated instance put a SingKind constraint on a phantom type, which is questionable. (There are other various corner cases that I could cite, although I'll leave it at that for now.)

At the end of the day, I think it would be nice to give power users the ability to tweak this. It would certainly save me from having to write a lot of code, at least, and #348 suggests that others would save as well.

goldfirere commented 5 years ago

OK. Don't let me stand in your way. :)

RyanGlScott commented 4 years ago

427 implements the workaround described in https://github.com/goldfirere/singletons/issues/150#issuecomment-549048888.

RyanGlScott commented 4 years ago

448 poses an interesting challenge: how should SingKind handle Data.Functor.Product? I started out with a simple attempt at defining Promote/Demote instances for it:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Functor.Product
import Data.Kind

type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k

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

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type instance Promote Type = Type
type instance Demote  Type = Type

type instance Promote (a -> b) = PromoteX a ~> PromoteX b
type instance Demote  (a ~> b) = DemoteX  a -> DemoteX  b

type instance PromoteX (k :: Type) = Promote k
type instance DemoteX  (k :: Type) = Demote  k

$(pure [])
type instance Promote (Product f g a) = Product (PromoteX f) (PromoteX g) (PromoteX a)
type instance Demote  (Product f g a) = Demote  (DemoteX  f) (DemoteX  g) (DemoteX  a)

However, that doesn't work:

$ /opt/ghc/8.10.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o, Foo.dyn_o )

Foo.hs:32:76: error:
    • Expected kind ‘TyFun (Promote k0) *’,
        but ‘PromoteX a’ has kind ‘Promote k0’
    • In the third argument of ‘Product’, namely ‘(PromoteX a)’
      In the type ‘Product (PromoteX f) (PromoteX g) (PromoteX a)’
      In the type instance declaration for ‘Promote’
   |
32 | type instance Promote (Product f g a) = Product (PromoteX f) (PromoteX g) (PromoteX a)
   |                                                                            ^^^^^^^^^^

Foo.hs:33:41: error:
    • Expected kind ‘* -> Demote k0 -> *’,
        but ‘Demote (DemoteX f)’ has kind ‘*’
    • In the type ‘Demote (DemoteX f) (DemoteX g) (DemoteX a)’
      In the type instance declaration for ‘Demote’
   |
33 | type instance Demote  (Product f g a) = Demote  (DemoteX  f) (DemoteX  g) (DemoteX  a)
   |                                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Can you think of a way to make these instances typecheck?

goldfirere commented 4 years ago

For Promote, this works:

type instance Promote (Product f g a) = Product (PromoteX f) (PromoteX g) @@ (PromoteX a)

At least, it type checks. Something tells me something is wrong here. But, really, this is just #82 I think.

RyanGlScott commented 4 years ago

But, really, this is just #82 I think.

Interesting. Are you suggesting that in order for this to work, Product needs to be able to switch between (~>) and (->) depending on whether it's promoted or not? Following that idea, I was able to write instances of Promote and Demote successfully:

```hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Foo where import Data.Kind import Data.Type.Equality type Sing :: k -> Type type family Sing type SomeSing :: Type -> Type data SomeSing k where SomeSing :: Sing (a :: k) -> SomeSing k type Promote :: Type -> Type type family Promote k type PromoteX :: k -> Promote k type family PromoteX a type Demote :: Type -> Type type family Demote k type DemoteX :: k -> Demote k type family DemoteX a type SingKindX :: k -> Constraint type SingKindX a = PromoteX (DemoteX a) ~~ a type SingKind :: Type -> Constraint class SingKindX k => SingKind k where fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k withSomeSing :: forall k r . SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r withSomeSing x f = case toSing x of SomeSing x' -> f x' type TyFun :: Type -> Type -> Type data TyFun a b type (~>) :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type Apply :: (a ~> b) -> a -> b type family Apply f x type (@@) :: (a ~> b) -> a -> b type f @@ x = Apply f x infixl 9 @@ type instance Promote Type = Type type instance Demote Type = Type type instance Promote (a -> b) = PromoteX a ~> PromoteX b type instance Demote (a ~> b) = DemoteX a -> DemoteX b type instance PromoteX (k :: Type) = Promote k type instance DemoteX (k :: Type) = Demote k data TyCon1 :: (a -> b) -> (a ~> b) type instance Apply (TyCon1 f) x = f x data TyCon2 :: (a -> b -> c) -> (a ~> b ~> c) type instance Apply (TyCon2 f) x = TyCon1 (f x) type TyConApp :: (a -> b) -> a -> b type family TyConApp f where TyConApp f = f type TyConAppSym0 :: (a -> b) ~> a ~> b data TyConAppSym0 f type instance Apply TyConAppSym0 f = TyConAppSym1 f type TyConAppSym1 :: (a -> b) -> a ~> b data TyConAppSym1 f x type instance Apply (TyConAppSym1 f) x = TyConApp f x type (~>@#@$) :: Type ~> Type ~> Type data (~>@#@$) a type instance Apply (~>@#@$) a = (~>@#@$$) a type (~>@#@$$) :: Type -> Type ~> Type data (~>@#@$$) a b type instance Apply ((~>@#@$$) a) b = a ~> b type ApplySym0 :: (a ~> b) ~> a ~> b data ApplySym0 f type instance Apply ApplySym0 f = ApplySym1 f type ApplySym1 :: (a ~> b) -> a ~> b data ApplySym1 f x type instance Apply (ApplySym1 f) x = Apply f x type Product' :: forall k. forall (arr :: Type ~> Type ~> Type) (app :: arr @@ k @@ Type ~> k ~> Type) -> arr @@ k @@ Type -> arr @@ k @@ Type -> k -> Type data Product' arr app f g a = Pair (app @@ f @@ a) (app @@ g @@ a) type Product = Product' (TyCon2 (->)) TyConAppSym0 type PProduct = Product' (~>@#@$) ApplySym0 type SProduct :: PProduct f g a -> Type data SProduct p where SPair :: Sing fa -> Sing ga -> SProduct (Pair fa ga) type instance Sing = SProduct $(pure []) type instance Promote (Product f g a) = PProduct (PromoteX f) (PromoteX g) (PromoteX a) type instance Demote (PProduct f g a) = Product (DemoteX f) (DemoteX g) (DemoteX a) ```

However, I get stuck when trying to define the SingKind instance:

instance (SingKindX f, SingKindX g, SingKindX a) => SingKind (PProduct f g a) where
  fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
$ /opt/ghc/8.10.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o, Foo.dyn_o )

Foo.hs:125:36: error:
    • Could not deduce: Demote (Apply f a) ~ DemoteX f (DemoteX a)
      from the context: (SingKindX f, SingKindX g, SingKindX a)
        bound by the instance declaration at Foo.hs:124:10-77
      or from: a1 ~ 'Pair fa ga
        bound by a pattern with constructor:
                   SPair :: forall k (f :: k ~> *) (a :: k) (g :: k ~> *)
                                   (fa :: Apply f a) (ga :: Apply g a).
                            Sing fa -> Sing ga -> SProduct ('Pair fa ga),
                 in an equation for ‘fromSing’
        at Foo.hs:125:13-25
      Expected type: (TyConAppSym0 @@ DemoteX f) @@ DemoteX a
        Actual type: Demote (Apply f a)
    • In the first argument of ‘Pair’, namely ‘(fromSing sfa)’
      In the expression: Pair (fromSing sfa) (fromSing sga)
      In an equation for ‘fromSing’:
          fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
    • Relevant bindings include
        sga :: Sing ga (bound at Foo.hs:125:23)
        sfa :: Sing fa (bound at Foo.hs:125:19)
        fromSing :: Sing a1 -> Demote (PProduct f g a)
          (bound at Foo.hs:125:3)
    |
125 |   fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
    |                                    ^^^^^^^^^^^^

Foo.hs:125:51: error:
    • Could not deduce: Demote (Apply g a) ~ DemoteX g (DemoteX a)
      from the context: (SingKindX f, SingKindX g, SingKindX a)
        bound by the instance declaration at Foo.hs:124:10-77
      or from: a1 ~ 'Pair fa ga
        bound by a pattern with constructor:
                   SPair :: forall k (f :: k ~> *) (a :: k) (g :: k ~> *)
                                   (fa :: Apply f a) (ga :: Apply g a).
                            Sing fa -> Sing ga -> SProduct ('Pair fa ga),
                 in an equation for ‘fromSing’
        at Foo.hs:125:13-25
      Expected type: (TyConAppSym0 @@ DemoteX g) @@ DemoteX a
        Actual type: Demote (Apply g a)
    • In the second argument of ‘Pair’, namely ‘(fromSing sga)’
      In the expression: Pair (fromSing sfa) (fromSing sga)
      In an equation for ‘fromSing’:
          fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
    • Relevant bindings include
        sga :: Sing ga (bound at Foo.hs:125:23)
        sfa :: Sing fa (bound at Foo.hs:125:19)
        fromSing :: Sing a1 -> Demote (PProduct f g a)
          (bound at Foo.hs:125:3)
    |
125 |   fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
    |                                                   ^^^^^^^^^^^^

Any ideas?

RyanGlScott commented 4 years ago

Please disregard https://github.com/goldfirere/singletons/issues/150#issuecomment-612855762. It is based on the false premise that we need separate Product (term-level) and PProduct (type-level) types. In reality, we don't need to vary the arrows, but rather whether the fields are demoted or not. Here is a version of Product that can be given a SingKind instance:

```hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Foo where import Data.Kind import Data.Type.Equality type family Sing :: k -> Type data SomeSing :: Type -> Type where SomeSing :: Sing (a :: k) -> SomeSing k type family Promote (k :: Type) :: Type type family PromoteX (a :: k) :: Promote k type family Demote (k :: Type) :: Type type family DemoteX (a :: k) :: Demote k type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a) class SingKindX k => SingKind k where fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r withSomeSing x k = case toSing x of SomeSing sx -> k sx data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type instance Demote Type = Type type instance Promote Type = Type type instance Demote (a ~> b) = DemoteX a -> DemoteX b type instance Promote (a -> b) = PromoteX a ~> PromoteX b type instance DemoteX (k :: Type) = Demote k type instance PromoteX (k :: Type) = Promote k data Product f g a = Pair (f a) (g a) data DemotedProduct f g a = DemotedPair (Demote (f a)) (Demote (g a)) data SProduct :: forall f g a. Product f g a -> Type where SPair :: Sing fa -> Sing ga -> SProduct (Pair fa ga) type instance Sing = SProduct type instance Demote (Product f g a) = DemotedProduct f g a type instance Promote (DemotedProduct f g a) = Product f g a instance (SingKind (f a), SingKind (g a)) => SingKind (Product f g a) where fromSing (SPair sfa sga) = DemotedPair (fromSing sfa) (fromSing sga) toSing (DemotedPair fa ga) = withSomeSing fa $ \sfa -> withSomeSing ga $ \sga -> SomeSing (SPair sfa sga) ```

Or, if you don't want Product and DemotedProduct to be separate data types, you can do this:

```hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Foo where import Data.Kind import Data.Type.Equality import Unsafe.Coerce type family Sing :: k -> Type data SomeSing :: Type -> Type where SomeSing :: Sing (a :: k) -> SomeSing k type family Promote (k :: Type) :: Type type family PromoteX (a :: k) :: Promote k type family Demote (k :: Type) :: Type type family DemoteX (a :: k) :: Demote k data DemoteSym0 :: Type ~> Type type instance Apply DemoteSym0 x = Demote x type SingKindX a = PromoteX (DemoteX a) ~~ a class SingKindX k => SingKind k where fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r withSomeSing x k = case toSing x of SomeSing sx -> k sx data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: a ~> b) (x :: a) :: b type f @@ x = Apply f x type instance Demote Type = Type type instance Promote Type = Type type instance Demote (a ~> b) = DemoteX a -> DemoteX b type instance Promote (a -> b) = PromoteX a ~> PromoteX b type instance DemoteX (k :: Type) = Demote k type instance PromoteX (k :: Type) = Promote k type family Id (x :: a) :: a where Id x = x data IdSym0 :: a ~> a type instance Apply IdSym0 x = Id x data Product' (p :: Type ~> Type) f g a = Pair (p @@ f a) (p @@ g a) type Product = Product' IdSym0 type DemotedProduct = Product' DemoteSym0 data SProduct :: forall f g a. Product f g a -> Type where SPair :: Sing fa -> Sing ga -> SProduct (Pair fa ga) type instance Sing = SProduct type instance Demote (Product f g a) = DemotedProduct f g a type instance Promote (DemotedProduct f g a) = Product f g a instance (SingKind (f a), SingKind (g a)) => SingKind (Product f g a) where fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga) toSing (Pair fa ga) = withSomeSing fa $ \sfa -> withSomeSing ga $ \sga -> SomeSing (SPair sfa sga) ```

Neither version is quite satisfying for two reasons:

  1. You can't define PromoteX or DemoteX instances for Pair. I'm starting to believe that this is a fundamental limitation of PromoteX and DemoteX, since you can't define instances of them for (n :: Nat), (s :: Symbol), or (f :: a ~> b) either.
  2. Neither version is able to simply use Product from Data.Functor.Product everywhere. In the former version, you have to define a separate DemotedProduct data type alongside Data.Functor.Product.Product in order to make the SingKind instance work, and in the latter version, you don't use Data.Functor.Product.Product at all. This means that this version of SingKind wouldn't be a solution for #448.

This is reaffirming my belief that SingKind is fundamentally limited in what in can express. This version of SingKind can define instances for more things than the current version, yes, but it's far from perfect.

goldfirere commented 4 years ago

A little experimentation revealed that a problem is the overlap between TyFun a b -> Type (that is, a ~> b) and a -> b. Maybe if there were an encoding of a ~> b that was apart from a -> b, we would be in better shape. But I'm not feeling particularly creative around that at the moment...

RyanGlScott commented 4 years ago

A little experimentation revealed that a problem is the overlap between TyFun a b -> Type (that is, a ~> b) and a -> b.

That sounds like an interesting experiment, although it's unclear to me what steps led to to that conclusion. Do you mind providing some more details on what you tried? I have also wondered if a different encoding of a ~> b would be worthwhile (since you cannot partially apply (~>) currently), and this seems to add another argument in favor of that.

goldfirere commented 4 years ago

I wanted to say Demote (a -> b) = Demote a -> Demote b. But that overlapped. So I wrote

type family DemoteArrow a b where
  DemoteArrow (TyFun a b) Type = Demote a -> Demote b
  DemoteArrow a           b    = Demote a -> Demote b
type instance Demote  (a -> b) = DemoteArrow a b

but then Demote (k0 -> Type) is stuck. :(

RyanGlScott commented 4 years ago

Ah, now I see. I guess this is yet another thing that UnsaturatedTypeFamilies would make easier, since (~>) would become a distinct entity from (->).