Re: GHC not able to detect impossible GADT pattern

3 Sep 2014

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