blob: 31da8f479179fa00ffbfca37dc9284220956f977 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
module SingletonsBug where
import Control.Applicative
import Data.Traversable (for)
import GHC.Exts( Constraint )
-----------------------------------
-- From 'constraints' library
-- import Data.Constraint (Dict(..))
data Dict :: Constraint -> * where
Dict :: a => Dict a
-----------------------------------
-- From 'singletons' library
-- import Data.Singletons hiding( withSomeSing )
class SingI (a :: k) where
-- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@
-- extension to use this method the way you want.
sing :: Sing a
data family Sing (a :: k)
data KProxy (a :: *) = KProxy
data SomeSing (kproxy :: KProxy k) where
SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
-- SingKind :: forall k. KProxy k -> Constraint
class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
-- | Get a base type from a proxy for the promoted kind. For example,
-- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.
type DemoteRep kparam :: *
-- | Convert a singleton to its unrefined version.
fromSing :: Sing (a :: k) -> DemoteRep kparam
-- | Convert an unrefined type to an existentially-quantified singleton type.
toSing :: DemoteRep kparam -> SomeSing kparam
withSomeSing :: SingKind ('KProxy :: KProxy k)
=> DemoteRep ('KProxy :: KProxy k)
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing = error "urk"
-----------------------------------
data SubscriptionChannel = BookingsChannel
type BookingsChannelSym0 = BookingsChannel
data instance Sing (z_a5I7 :: SubscriptionChannel) where
SBookingsChannel :: Sing BookingsChannel
instance SingKind ('KProxy :: KProxy SubscriptionChannel) where
type DemoteRep ('KProxy :: KProxy SubscriptionChannel) = SubscriptionChannel
fromSing SBookingsChannel = BookingsChannel
toSing BookingsChannel = SomeSing SBookingsChannel
instance SingI BookingsChannel where
sing = SBookingsChannel
type family T (c :: SubscriptionChannel) :: *
type instance T 'BookingsChannel = Bool
witnessC :: Sing channel -> Dict (Show (T channel), SingI channel)
witnessC SBookingsChannel = Dict
forAllSubscriptionChannels
:: forall m r. (Applicative m)
=> (forall channel. (SingI channel, Show (T channel)) => Sing channel -> m r)
-> m r
forAllSubscriptionChannels f =
withSomeSing BookingsChannel $ \(sChannel) ->
case witnessC sChannel of
Dict -> f sChannel
|
