[GHC] #10778: GHC doesn't infer all constrains

[GHC]

#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