GHC not able to detect impossible GADT pattern

[Merijn Verstraaten]

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/20140902/3e2bffc5/attachment.sig>