Commit 3034dd40 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Another test for type function saturation

Came up on GHC users list
parent b5a57767
-- 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)
......@@ -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, [''])
-- 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
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’
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment