[GHC] #14237: -Wredundant-constraints incorrectly warns about required type equality constraints in default signatures

[GHC]

#14237: -Wredundant-constraints incorrectly warns about required type equality
constraints in default signatures
-------------------------------------+-------------------------------------
           Reporter:  lexi.lambda    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           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:
-------------------------------------+-------------------------------------
 GHC emits a warning about the following function:

 {{{#!hs
 f :: (Integer ~ a) => a -> Integer
 f = (+ 1)
 }}}
 {{{
 /private/tmp/redundant-default-
 constraint/src/RedundantDefaultConstraints.hs:14:1: warning: [-Wredundant-
 constraints]
     • Redundant constraint: Integer ~ a
     • In the type signature for:
            f :: forall a. Integer ~ a => a -> Integer
    |
 14 | f :: Integer ~ a => a -> Integer
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 This is understandable (though the error message could perhaps be better)
 because the equality is pointless. It would be better to just rewrite the
 type signature as `Integer -> Integer`.

 However, this becomes problematic when combined with `DefaultSignatures`.
 GHC ''also'' emits a warning for the following program:

 {{{#!hs
 class Monad m => MonadFoo m where
   foo :: m ()

   default foo :: (MonadFoo m', MonadTrans t, m ~ t m') => m ()
   foo = lift foo
 }}}
 {{{
 /private/tmp/redundant-default-
 constraint/src/RedundantDefaultConstraints.hs:8:18: warning: [-Wredundant-
 constraints]
     • Redundant constraint: m ~ t m'
     • In the type signature for:
            foo :: forall (m' :: * -> *) (t :: (* -> *) -> * -> *).
                   (MonadFoo m', MonadTrans t, m ~ t m') =>
                   m ()
   |
 8 |   default foo :: (MonadFoo m', MonadTrans t, m ~ t m') => m ()
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 This is wrong, because the constraint here is necessary. The type equality
 cannot be “inlined” into the type, since #12918 made that illegal. The
 constraint cannot be removed entirely, since then the program would fail
 to typecheck. Therefore, GHC should not produce an error in this case.

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