Opened 4 years ago

Last modified 16 months ago

#10778 new bug

GHC doesn't infer all constrains

Reported by: danilo2 Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: Cc: dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by danilo2)

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.

Change History (11)

comment:1 Changed 4 years ago by danilo2

Description: modified (diff)

comment:2 Changed 4 years ago by danilo2

Description: modified (diff)

comment:3 Changed 4 years ago by goldfire

I don't see a functional dependency on your Container class. Is there supposed to be one?

comment:4 Changed 4 years ago by danilo2

No, But there are the GADTs constraints:

IndexOf a cont ~ idx, ElementByIdx idx cont ~ a

So idx is always result of IndexOf a cont. Is this information not enough for GHC?

Last edited 4 years ago by danilo2 (previous) (diff)

comment:5 Changed 4 years ago by goldfire

Ah -- I see now. Yes, this might be reasonable. Curious to see what Simon thinks, after he returns from holiday.

comment:6 Changed 4 years ago by danilo2

@Simon have a nice holiday! :D

comment:7 Changed 3 years ago 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).

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?

comment:8 Changed 16 months ago by George

Type of failure: None/UnknownGHC rejects valid program

comment:9 Changed 16 months ago by dfeuer

Cc: dfeuer added

Is this just waiting on a test case?

comment:10 Changed 16 months ago by simonpj

Is this just waiting on a test case?

I think so, yes.

comment:11 Changed 16 months ago 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?

Note: See TracTickets for help on using tickets.