RE: GHC not able to detect impossible GADT pattern
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- | boun...@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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHC not able to detect impossible GADT pattern
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 simo...@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- | boun...@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 |-
RE: GHC not able to detect impossible GADT pattern
This is a bug in 7.8.3: https://ghc.haskell.org/trac/ghc/ticket/9433 You should get this error (and do in HEAD): Sock.hs:28:5: Type family 'Readable' should have 1 argument, but has been given none In the equations for closed type family 'Foo' So your program is indeed wrong, but the error message you are getting is entirely bogus. If you fix the above error you should be good to go. Indeed, if you change the defn of Foo thus, it compiles just fine type family Foo (op :: SocketOperation) (s :: SocketType) :: Constraint where Foo 'Read s = Readable s Foo Write s = Writable s Sorry about the egregious bug. Simon | -Original Message- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Merijn Verstraaten | Sent: 03 September 2014 09:22 | To: Simon Peyton Jones | Cc: Tom Schrijvers; GHC Users List | Subject: Re: GHC not able to detect impossible GADT pattern | | 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 simo...@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- | | boun...@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