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