Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / pmcheck / should_compile / T3927b.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE TypeOperators #-}
8 {-# LANGUAGE UndecidableInstances #-}
9 {-# LANGUAGE UndecidableSuperClasses #-}
10 {-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
11
12 module T3927b where
13
14 import Data.Kind (Type, Constraint)
15 import Data.Proxy
16
17 data Message
18
19 data SocketType = Dealer | Push | Pull
20
21 data SocketOperation = Read | Write
22
23 type family Restrict (a :: SocketOperation) (as :: [SocketOperation]) :: Constraint where
24 Restrict a (a ': as) = ()
25 Restrict x (a ': as) = Restrict x as
26 Restrict x '[] = ("Error!" ~ "Tried to apply a restricted type!")
27
28 type family Implements (t :: SocketType) :: [SocketOperation] where
29 Implements Dealer = ['Read, Write]
30 Implements Push = '[Write]
31 Implements Pull = '[ 'Read]
32
33 data SockOp :: SocketType -> SocketOperation -> Type where
34 SRead :: SockOp sock 'Read
35 SWrite :: SockOp sock Write
36
37 data Socket :: SocketType -> Type where
38 Socket :: proxy sock
39 -> (forall op . Restrict op (Implements sock) => SockOp sock op -> Operation op)
40 -> Socket sock
41
42 type family Operation (op :: SocketOperation) :: Type where
43 Operation 'Read = IO Message
44 Operation Write = Message -> IO ()
45
46 class Restrict 'Read (Implements t) => Readable t where
47 readSocket :: Socket t -> Operation 'Read
48 readSocket (Socket _ f) = f (SRead :: SockOp t 'Read)
49
50 instance Readable Dealer
51
52 type family Writable (t :: SocketType) :: Constraint where
53 Writable Dealer = ()
54 Writable Push = ()
55
56 dealer :: Socket Dealer
57 dealer = Socket (Proxy :: Proxy Dealer) f
58 where
59 f :: Restrict op (Implements Dealer) => SockOp Dealer op -> Operation op
60 f SRead = undefined
61 f SWrite = undefined
62
63 push :: Socket Push
64 push = Socket (Proxy :: Proxy Push) f
65 where
66 f :: Restrict op (Implements Push) => SockOp Push op -> Operation op
67 f SWrite = undefined
68 -- Seeing that this pattern match is exhaustive
69 -- requires a reasonably vigorous effort on given
70 -- superclass expansion.
71
72 pull :: Socket Pull
73 pull = Socket (Proxy :: Proxy Pull) f
74 where
75 f :: Restrict op (Implements Pull) => SockOp Pull op -> Operation op
76 f SRead = undefined
77
78 foo :: IO Message
79 foo = readSocket dealer