GHC not able to detect impossible GADT pattern

[Simon Peyton Jones]

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 at 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 <simonpj at 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-
| > | bounces at 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