[GHC] #10778: GHC doesn't infer all constrains
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Hello! Let's consider following signatures: {{{ class (IndexOf a cont ~ idx, ElementByIdx idx cont ~ a, Measurable cont) => Container cont idx a class Container cont idx a => Appendable cont idx a class HasContainer a cont | a -> cont class Monad m => RefBuilder3 a m ref | a m -> ref where mkRef3 :: a -> m (ref a) }}} Now when I define following instance: {{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 = undefined }}} I get an error: {{{ Illegal instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ The liberal coverage condition fails in class ‘RefBuilder3’ for functional dependency: ‘a m -> ref’ Reason: lhs types ‘a’, ‘GraphBuilderT g m’ do not jointly determine rhs type ‘Ptr i’ In the instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ }}} But when I add the constraint to the instance head: {{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m, IndexOf a cont ~ idx) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 a = fmap ptrFrom . withGraph . append $ a }}} It compiles fine. What's interesting, the constraint should be inferred by GHC, because we've got following funds here: {{{ g -> cont -- from HasContainer cont a -> idx -- from Appendable -> Container }}} Is this a GHC bug or am I missing something? If thats a bug, I will try to clean the code and make a minimal example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by danilo2: Old description:
Hello! Let's consider following signatures: {{{ class (IndexOf a cont ~ idx, ElementByIdx idx cont ~ a, Measurable cont) => Container cont idx a class Container cont idx a => Appendable cont idx a class HasContainer a cont | a -> cont class Monad m => RefBuilder3 a m ref | a m -> ref where mkRef3 :: a -> m (ref a)
}}}
Now when I define following instance:
{{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 = undefined }}}
I get an error:
{{{ Illegal instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ The liberal coverage condition fails in class ‘RefBuilder3’ for functional dependency: ‘a m -> ref’ Reason: lhs types ‘a’, ‘GraphBuilderT g m’ do not jointly determine rhs type ‘Ptr i’ In the instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ }}}
But when I add the constraint to the instance head:
{{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m, IndexOf a cont ~ idx) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 a = fmap ptrFrom . withGraph . append $ a }}}
It compiles fine. What's interesting, the constraint should be inferred by GHC, because we've got following funds here: {{{ g -> cont -- from HasContainer cont a -> idx -- from Appendable -> Container }}}
Is this a GHC bug or am I missing something? If thats a bug, I will try to clean the code and make a minimal example.
New description: Hello! Let's consider following signatures: {{{ class (IndexOf a cont ~ idx, ElementByIdx idx cont ~ a, Measurable cont) => Container cont idx a class Container cont idx a => Appendable cont idx a class HasContainer a cont | a -> cont class PtrFrom p i | p -> i class Monad m => RefBuilder3 a m ref | a m -> ref where mkRef3 :: a -> m (ref a) }}} Now when I define following instance: {{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 = undefined }}} I get an error: {{{ Illegal instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ The liberal coverage condition fails in class ‘RefBuilder3’ for functional dependency: ‘a m -> ref’ Reason: lhs types ‘a’, ‘GraphBuilderT g m’ do not jointly determine rhs type ‘Ptr i’ In the instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ }}} But when I add the constraint to the instance head: {{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m, IndexOf a cont ~ idx) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 a = fmap ptrFrom . withGraph . append $ a }}} It compiles fine. What's interesting, the constraint should be inferred by GHC, because we've got following funds here: {{{ g -> cont -- from HasContainer cont a -> idx -- from Appendable -> Container idx -> i -- from PtrFrom }}} Is this a GHC bug or am I missing something? If thats a bug, I will try to clean the code and make a minimal example. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by danilo2: Old description:
Hello! Let's consider following signatures: {{{ class (IndexOf a cont ~ idx, ElementByIdx idx cont ~ a, Measurable cont) => Container cont idx a class Container cont idx a => Appendable cont idx a class HasContainer a cont | a -> cont class PtrFrom p i | p -> i class Monad m => RefBuilder3 a m ref | a m -> ref where mkRef3 :: a -> m (ref a)
}}}
Now when I define following instance:
{{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 = undefined }}}
I get an error:
{{{ Illegal instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ The liberal coverage condition fails in class ‘RefBuilder3’ for functional dependency: ‘a m -> ref’ Reason: lhs types ‘a’, ‘GraphBuilderT g m’ do not jointly determine rhs type ‘Ptr i’ In the instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ }}}
But when I add the constraint to the instance head:
{{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m, IndexOf a cont ~ idx) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 a = fmap ptrFrom . withGraph . append $ a }}}
It compiles fine. What's interesting, the constraint should be inferred by GHC, because we've got following funds here: {{{ g -> cont -- from HasContainer cont a -> idx -- from Appendable -> Container idx -> i -- from PtrFrom }}}
Is this a GHC bug or am I missing something? If thats a bug, I will try to clean the code and make a minimal example.
New description: Hello! Let's consider following signatures: {{{ class (IndexOf a cont ~ idx, ElementByIdx idx cont ~ a, Measurable cont) => Container cont idx a class Container cont idx a => Appendable cont idx a class HasContainer a cont | a -> cont class PtrFrom p i | p -> i class Monad m => RefBuilder3 a m ref | a m -> ref where mkRef3 :: a -> m (ref a) }}} Now when I define following instance: {{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 = undefined }}} I get an error: {{{ Illegal instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ The liberal coverage condition fails in class ‘RefBuilder3’ for functional dependency: ‘a m -> ref’ Reason: lhs types ‘a’, ‘GraphBuilderT g m’ do not jointly determine rhs type ‘Ptr i’ In the instance declaration for ‘RefBuilder3 a (GraphBuilderT g m) (Ptr i)’ }}} But when I add the constraint to the instance head: {{{ instance (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m, IndexOf a cont ~ idx) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) where mkRef3 a = fmap ptrFrom . withGraph . append $ a }}} It compiles fine. What's interesting, the constraint should be inferred by GHC, because we've got following fundeps here: {{{ g -> cont -- from HasContainer cont a -> idx -- from Appendable -> Container idx -> i -- from PtrFrom }}} Is this a GHC bug or am I missing something? If thats a bug, I will try to clean the code and make a minimal example. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): I don't see a functional dependency on your `Container` class. Is there supposed to be one? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by danilo2): No, But there are the GADTs constraints: {{{ IndexOf a cont ~ idx, ElementByIdx idx cont ~ a, Measurable cont }}} So {{{idx}}} is always result of {{{IndexOf a cont}}}. Is this information not enough for Haskell? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Ah -- I see now. Yes, this might be reasonable. Curious to see what Simon thinks, after he returns from holiday. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by danilo2): @Simon have a nice holiday! :D -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'd missed this. Actually it turns out that it's already fixed in 8.0. What happens is this: * `(t1 ~ t2)` is actually a class constraint (homogeneous equality), with superclass `(t1 ~~ t2)` (heterogeneous equality). * `(t1 ~~ t2)` is actuall a class constraint with superclass `(t1 ~# t2)` (true nominal type equality). * The `oclose` function in `FunDeps` already takes account of true nominal equality. Iavor appears to have put this in as part of fe61599ffebb27924c4beef47b6237542644f3f4. To the code above I added {{{ data IndexOf a b data ElementByIdx a b class Measurable a data GraphBuilderT g (m :: * -> *) a data Ptr a b }}} And then your example compiles fine. More precisely, in addition to incorrectly reporting the coverate error, GHC 7.10 correctly says {{{ T10778.hs:18:10: Couldn't match type ‘a’ with ‘ElementByIdx (IndexOf a cont) cont’ ‘a’ is a rigid type variable bound by an instance declaration: (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) at T10778.hs:18:10 Inaccessible code in an instance declaration: (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) In the ambiguity check for an instance declaration: forall a g (m :: * -> *) i idx cont. (PtrFrom idx i, Appendable cont idx a, HasContainer g cont, Monad m) => RefBuilder3 a (GraphBuilderT g m) (Ptr i) }}} But because of #12466, it now says (much more confusingly) {{{ T10778.hs:20:5: warning: [-Woverlapping-patterns] Pattern match is redundant In an equation for ‘mkRef3’: mkRef3 = ... }}} The pattern match checker sees that the entire instance is inaccessible, and so reports that the (only) equation for `mkRef3` is redundant. See #12694 for a simpler case. Do you agree that the instance is in fact inaccessible? Want to change the example to something more sensible to add as a regression test? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by George): * failure: None/Unknown => GHC rejects valid program -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) Comment: Is this just waiting on a test case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Is this just waiting on a test case?
I think so, yes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10778: GHC doesn't infer all constrains -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Simon, I see pretty much the same error unless I enable `UndecidableInstances`. Should I enable that for the test, or do we still have a problem? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10778#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC