-Wredundant-constraints incorrectly treats all type equality constraints as redundant

GHC emits a warning about the following function:

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:

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 (closed) 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.

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture