Another test for type function saturation

Came up on GHC users list

5 files changed, 119 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/Sock.hs b/testsuite/tests/indexed-types/should_compile/Sock.hs
new file mode 100644
index 0000000000..7b89e9ac77
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Sock.hs
@@ -0,0 +1,55 @@
+-- From the GHC users mailing list, 3/9/14
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module Sock where
+
+import Data.Proxy
+import GHC.Exts
+
+data Message
+
+data SocketType = Dealer | Push | Pull
+
+data SocketOperation = Read | Write
+
+data SockOp :: SocketType -> SocketOperation -> * where
+    SRead :: Foo 'Read sock => SockOp sock 'Read
+    SWrite :: Foo Write sock => SockOp sock Write
+
+data Socket :: SocketType -> * where
+    Socket :: proxy sock
+           -> (forall op . Foo op sock => SockOp sock op -> Operation op)
+           -> Socket sock
+
+type family Foo (op :: SocketOperation) (s :: SocketType) :: Constraint where
+    Foo 'Read s = Readable s
+    Foo Write s = Writable s
+
+type family Operation (op :: SocketOperation) :: * where
+    Operation 'Read = IO Message
+    Operation Write = Message -> IO ()
+
+type family Readable (t :: SocketType) :: Constraint where
+    Readable Dealer = ()
+    Readable Pull = ()
+
+type family Writable (t :: SocketType) :: Constraint where
+    Writable Dealer = ()
+    Writable Push = ()
+
+dealer :: Socket Dealer
+dealer = undefined
+
+push :: Socket Push
+push = undefined
+
+pull :: Socket Pull
+pull = undefined
+
+readSocket :: forall sock . Readable sock => Socket sock -> IO Message
+readSocket (Socket _ f) = f (SRead :: SockOp sock 'Read)
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index be0099cb84..ff45df2c83 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -246,3 +246,4 @@ test('T8979', normal, compile, [''])
 test('T9085', normal, compile, [''])
 test('T9316', normal, compile, [''])
 test('red-black-delete', normal, compile, [''])
+test('Sock', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/BadSock.hs b/testsuite/tests/indexed-types/should_fail/BadSock.hs
new file mode 100644
index 0000000000..3e72817b8d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/BadSock.hs
@@ -0,0 +1,57 @@
+-- From the GHC users mailing list, 3/9/14
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module BadSock where
+
+import Data.Proxy
+import GHC.Exts
+
+data Message
+
+data SocketType = Dealer | Push | Pull
+
+data SocketOperation = Read | Write
+
+data SockOp :: SocketType -> SocketOperation -> * where
+    SRead :: Foo 'Read sock => SockOp sock 'Read
+    SWrite :: Foo Write sock => SockOp sock Write
+
+data Socket :: SocketType -> * where
+    Socket :: proxy sock
+           -> (forall op . Foo op sock => SockOp sock op -> Operation op)
+           -> Socket sock
+
+type family Foo (op :: SocketOperation) :: SocketType -> Constraint where
+    Foo 'Read = Readable 
+    Foo Write = Writable 
+
+type family Operation (op :: SocketOperation) :: * where
+    Operation 'Read = IO Message
+    Operation Write = Message -> IO ()
+
+type family Readable (t :: SocketType) :: Constraint where
+    Readable Dealer = ()
+    Readable Pull = ()
+
+type family Writable (t :: SocketType) :: Constraint where
+    Writable Dealer = ()
+    Writable Push = ()
+
+{-
+dealer :: Socket Dealer
+dealer = undefined
+
+push :: Socket Push
+push = undefined
+
+pull :: Socket Pull
+pull = undefined
+
+readSocket :: forall sock . Readable sock => Socket sock -> IO Message
+readSocket (Socket _ f) = f (SRead :: SockOp sock 'Read)
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/BadSock.stderr b/testsuite/tests/indexed-types/should_fail/BadSock.stderr
new file mode 100644
index 0000000000..fc3fb54d0c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/BadSock.stderr
@@ -0,0 +1,5 @@
+
+BadSock.hs:30:5:
+    Type family ‘Readable’ should have 1 argument, but has been given none
+    In the equations for closed type family ‘Foo’
+    In the type family declaration for ‘Foo’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 50eec868b1..2862f1e854 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -127,4 +127,5 @@ test('T9160', normal, compile_fail, [''])
 test('T9357', normal, compile_fail, [''])
 test('T9371', normal, compile_fail, [''])
 test('T9433', normal, compile_fail, [''])
+test('BadSock', normal, compile_fail, [''])