[GHC] #14633: -fwarn-redundant-constraints false positive

[GHC]

#14633: -fwarn-redundant-constraints false positive
-------------------------------------+-------------------------------------
        Reporter:  ghorn             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here is a much simpler example:
 {{{
 type family F a

 foo :: forall a b. (Eq a
                    , a ~ F b
                    ) => b -> Bool
 foo _ = (undefined :: a) == undefined
 }}}
 We compiling this we get
 {{{
 T14663.hs:35:1: error: [-Wredundant-constraints, -Werror=redundant-
 constraints]
     * Redundant constraint: a ~ F b
     * In the type signature for:
            foo :: forall a b. (Eq a, a ~ F b) => b -> Bool
    |
 35 | foo :: forall a b. (Eq a
    | ^^^^^^^^^^^^^^^^^^^^^^^^...
 }}}
 And indeed the equality constraint is redundant: the expression
 `undefined :: a == undefined` needs `Eq a` but we have that.

 But if we remove the equality constraint we get this complaint:
 {{{
 T14663.hs:35:8: error:
     * Could not deduce (Eq a0)
       from the context: Eq a
         bound by the type signature for:
                    foo :: forall a b. Eq a => b -> Bool
         at T14663.hs:(35,8)-(37,33)
       The type variable `a0' is ambiguous
     * In the ambiguity check for `foo'       <------ NB --------------
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature: foo :: forall a b. (Eq a) => b -> Bool
    |
 35 | foo :: forall a b. (Eq a
    |        ^^^^^^^^^^^^^^^^^...
 }}}
 Notice that this complaint comes from the '''ambiguity check''' for `foo`.
 Indeed `foo` really does have
 an ambiguous type.  For example, if have `foo :: Eq a => b -> Bool` and
 try
 {{{
 foo2 :: Eq c => d -> Bool
 foo2 = foo
 }}}
 we'd fail, because nothing forces the `a` from `foo` to be instantiated to
 `c` in `foo2`.  So the complaint is valid.

 The solution is to make the type unambiguous, perhaps by adding a proxy
 parameter:
 {{{
 foo :: forall a b. (Eq a) => Proxy a -> b -> Bool
 foo _ _ = (undefined :: a) == undefined
 }}}
 Now all is well: the type is unambiguous.

 I suppose you could also try `-XAllowAmbiguousTypes`, but the function
 really is ambiguous!

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14633#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler