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
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
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
This is a bug in 7.8.3: https://ghc.haskell.org/trac/ghc/ticket/9433
You should get this error (and do in HEAD):
Sock.hs:28:5:
Type family 'Readable' should have 1 argument, but has been given none
In the equations for closed type family 'Foo'
So your program is indeed wrong, but the error message you are getting is entirely bogus. If you fix the above error you should be good to go. Indeed, if you change the defn of Foo thus, it compiles just fine
type family Foo (op :: SocketOperation) (s :: SocketType)
:: Constraint where
Foo 'Read s = Readable s
Foo Write s = Writable s
Sorry about the egregious bug.
Simon
| -----Original Message-----
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| bounces@haskell.org] On Behalf Of Merijn Verstraaten
| Sent: 03 September 2014 09:22
| To: Simon Peyton Jones
| Cc: Tom Schrijvers; GHC Users List
| Subject: Re: GHC not able to detect impossible GADT pattern
|
| 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
participants (2)
-
Merijn Verstraaten -
Simon Peyton Jones