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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users