Hi Simon, Thanks for the clarification, I attached the code to that ticket. Does this mean improvements in this area are supposed to land in 7.10?
Semi-relatedly, before attempting the current code (which at least compiles), I had a few other attempts and I was hoping you (or other readers) might be able to shed some light on this baffling error (full code at the end): Could not deduce (Readable sock) arising from a use of ‘f’ from the context (Readable sock) bound by the type signature for readSocket :: (Readable sock) => Socket sock -> IO Message at test-old.hs:52:15-70 Relevant bindings include f :: forall (op :: SocketOperation). (Foo op sock) => SockOp sock op -> Operation op (bound at test-old.hs:53:22) readSocket :: Socket sock -> IO Message (bound at test-old.hs:53:1) In the expression: f (SRead :: SockOp sock Read) In an equation for ‘readSocket’: readSocket (Socket _ f) = f (SRead :: SockOp sock Read) It seems to me that “Readable sock” should be trivially deducible from itself? Cheers, Merijn {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Test 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) On 02 Sep 2014, at 23:21 , Simon Peyton Jones <simo...@microsoft.com> wrote: > I believe this is probably an instance of > https://ghc.haskell.org/trac/ghc/ticket/3927 > > There are numerous other similar tickets, about GHC's inadequate/misleading > warnings for non-exhaustive patterns. A selection is > #595, #5728, #3927, #5724, #5762, #4139, #6124, #7669, #322, #8016, #8494, > #8853, #8970, #9113. > > Tom Schrijvers and colleagues are working on this right now, I'm glad to say. > > Please do add your example to #3927, so that we can be sure to use it as a > regression test when testing Tom's shiny new version. > > Simon > > | -----Original Message----- > | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- > | boun...@haskell.org] On Behalf Of Merijn Verstraaten > | Sent: 03 September 2014 06:59 > | To: GHC Users List > | Subject: GHC not able to detect impossible GADT pattern > | > | I've been trying to stretch GHC's type system again and somehow managed > | to get myself into a position where GHC warns about a non-exhaustive > | pattern where adding the (according to GHC) missing pattern results in a > | type error (as intended by me). It seems that even with closed type > | families GHC can't infer some patterns can never occur? Complete code to > | reproduce the issue is including below, the non-exhaustive pattern > | happens in the local definitions 'f' of push and pull. > | > | I'm open to suggestions for other approaches. > | > | Kind regards, > | Merijn > | > | {-# LANGUAGE ConstraintKinds #-} > | {-# LANGUAGE DataKinds #-} > | {-# LANGUAGE GADTs #-} > | {-# LANGUAGE RankNTypes #-} > | {-# LANGUAGE ScopedTypeVariables #-} > | {-# LANGUAGE TypeFamilies #-} > | {-# LANGUAGE TypeOperators #-} > | {-# LANGUAGE UndecidableInstances #-} > | module Test where > | > | import Data.Proxy > | import GHC.Exts > | > | data Message > | > | data SocketType = Dealer | Push | Pull > | > | data SocketOperation = Read | Write > | > | type family Restrict (a :: SocketOperation) (as :: [SocketOperation]) :: > | Constraint where > | Restrict a (a ': as) = () > | Restrict x (a ': as) = Restrict x as > | Restrict x '[] = ("Error!" ~ "Tried to apply a restricted type!") > | > | type family Implements (t :: SocketType) :: [SocketOperation] where > | Implements Dealer = ['Read, Write] > | Implements Push = '[Write] > | Implements Pull = '[ 'Read] > | > | data SockOp :: SocketType -> SocketOperation -> * where > | SRead :: SockOp sock 'Read > | SWrite :: SockOp sock Write > | > | data Socket :: SocketType -> * where > | Socket :: proxy sock > | -> (forall op . Restrict op (Implements sock) => SockOp sock > | op -> Operation op) > | -> Socket sock > | > | type family Operation (op :: SocketOperation) :: * where > | Operation 'Read = IO Message > | Operation Write = Message -> IO () > | > | class Restrict 'Read (Implements t) => Readable t where > | readSocket :: Socket t -> Operation 'Read > | readSocket (Socket _ f) = f (SRead :: SockOp t 'Read) > | > | instance Readable Dealer > | > | type family Writable (t :: SocketType) :: Constraint where > | Writable Dealer = () > | Writable Push = () > | > | dealer :: Socket Dealer > | dealer = Socket (Proxy :: Proxy Dealer) f > | where > | f :: Restrict op (Implements Dealer) => SockOp Dealer op -> Operation > | op > | f SRead = undefined > | f SWrite = undefined > | > | push :: Socket Push > | push = Socket (Proxy :: Proxy Push) f > | where > | f :: Restrict op (Implements Push) => SockOp Push op -> Operation op > | f SWrite = undefined > | > | pull :: Socket Pull > | pull = Socket (Proxy :: Proxy Pull) f > | where > | f :: Restrict op (Implements Pull) => SockOp Pull op -> Operation op > | f SRead = undefined > | > | foo :: IO Message > | foo = readSocket dealer
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users