[commit: ghc] master: Another test for type function saturation (3034dd4)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/3034dd40a9c397ab4e5c596c15de83eefd834341/ghc

>---------------------------------------------------------------

commit 3034dd40a9c397ab4e5c596c15de83eefd834341
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Sep 3 21:44:40 2014 +0100

    Another test for type function saturation
    
    Came up on GHC users list


>---------------------------------------------------------------

3034dd40a9c397ab4e5c596c15de83eefd834341
 .../tests/indexed-types/should_compile/Sock.hs     | 55 +++++++++++++++++++++
 testsuite/tests/indexed-types/should_compile/all.T |  1 +
 .../tests/indexed-types/should_fail/BadSock.hs     | 57 ++++++++++++++++++++++
 .../should_fail/{T9097.stderr => BadSock.stderr}   |  4 +-
 testsuite/tests/indexed-types/should_fail/all.T    |  1 +
 5 files changed, 116 insertions(+), 2 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 0000000..7b89e9a
--- /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 be0099c..ff45df2 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 0000000..3e72817
--- /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/T9097.stderr b/testsuite/tests/indexed-types/should_fail/BadSock.stderr
similarity index 52%
copy from testsuite/tests/indexed-types/should_fail/T9097.stderr
copy to testsuite/tests/indexed-types/should_fail/BadSock.stderr
index 02dfc33..fc3fb54 100644
--- a/testsuite/tests/indexed-types/should_fail/T9097.stderr
+++ b/testsuite/tests/indexed-types/should_fail/BadSock.stderr
@@ -1,5 +1,5 @@
 
-T9097.hs:10:3:
-    Illegal type synonym family application in instance: Any
+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 50eec86..2862f1e 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, [''])