Ticket #3927: test.hs

File test.hs, 2.0 KB (added by merijn, 5 years ago)

Test case exhibiting wrong exhaustiveness checks that SPJ asked me to attach.

Line 
1{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE GADTs #-}
4{-# LANGUAGE RankNTypes #-}
5{-# LANGUAGE ScopedTypeVariables #-}
6{-# LANGUAGE TypeFamilies #-}
7{-# LANGUAGE TypeOperators #-}
8{-# LANGUAGE UndecidableInstances #-}
9module Test where
10
11import Data.Proxy
12import GHC.Exts
13
14data Message
15
16data SocketType = Dealer | Push | Pull
17
18data SocketOperation = Read | Write
19
20type family Restrict (a :: SocketOperation) (as :: [SocketOperation]) :: Constraint where
21    Restrict a (a ': as) = ()
22    Restrict x (a ': as) = Restrict x as
23    Restrict x '[] = ("Error!" ~ "Tried to apply a restricted type!")
24
25type family Implements (t :: SocketType) :: [SocketOperation] where
26    Implements Dealer = ['Read, Write]
27    Implements Push = '[Write]
28    Implements Pull = '[ 'Read]
29
30data SockOp :: SocketType -> SocketOperation -> * where
31    SRead :: SockOp sock 'Read
32    SWrite :: SockOp sock Write
33
34data Socket :: SocketType -> * where
35    Socket :: proxy sock
36           -> (forall op . Restrict op (Implements sock) => SockOp sock op -> Operation op)
37           -> Socket sock
38
39type family Operation (op :: SocketOperation) :: * where
40    Operation 'Read = IO Message
41    Operation Write = Message -> IO ()
42
43class Restrict 'Read (Implements t) => Readable t where
44    readSocket :: Socket t -> Operation 'Read
45    readSocket (Socket _ f) = f (SRead :: SockOp t 'Read)
46
47instance Readable Dealer
48
49type family Writable (t :: SocketType) :: Constraint where
50    Writable Dealer = ()
51    Writable Push = ()
52
53dealer :: Socket Dealer
54dealer = Socket (Proxy :: Proxy Dealer) f
55  where
56    f :: Restrict op (Implements Dealer) => SockOp Dealer op -> Operation op
57    f SRead = undefined
58    f SWrite = undefined
59
60push :: Socket Push
61push = Socket (Proxy :: Proxy Push) f
62  where
63    f :: Restrict op (Implements Push) => SockOp Push op -> Operation op
64    f SWrite = undefined
65
66pull :: Socket Pull
67pull = Socket (Proxy :: Proxy Pull) f
68  where
69    f :: Restrict op (Implements Pull) => SockOp Pull op -> Operation op
70    f SRead = undefined
71
72foo :: IO Message
73foo = readSocket dealer