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
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- | bounces@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