GHC not able to detect impossible GADT pattern

[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 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