GHC not able to detect impossible GADT pattern

[Merijn Verstraaten]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 801 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140903/ea80f616/attachment.sig>