Coverage condition should take functional dependencies in constraints into account

Motivation

The following instance is rejected by GHC (without UndecidableInstances) because the coverage condition fails:

{-# LANGUAGE FunctionalDependencies #-}

import Data.Functor.Identity

class Dep a b | a -> b where
  dep :: a -> b

instance (Dep a a') => Dep (Identity a) (Identity a') where
  dep = fmap dep

    • Illegal instance declaration for ‘Dep (Identity a) (Identity a')’
        The coverage condition fails in class ‘Dep’
          for functional dependency: ‘a -> b’
        Reason: lhs type ‘Identity a’
          does not determine rhs type ‘Identity a'’

Identity a does in fact determine Identity a', because a determines a', due to the instance's constraint, so I think the code should be accepted by GHC (without UndecidableInstances).

Proposal

I think that the functional dependencies in the constraints of instances should be taken into account, and the instance should be considered valid.

The coverage condition could be extended¹ to:

• Let S be the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.
• For each functional dependency tvs_left -> tvs_right, of the class, every type variable t_dest in S(tvs_right) must either appear in S(tvs_left), or there must exist a t_source in S(tvs_left) such that the functional dependencies of the instance's constraints contains a path from t_source -> t₁ -> ... -> t_n -> t_dest

---

1. Original definition taken from https://downloads.haskell.org/~ghc/7.0.1/docs/html/users_guide/type-class-extensions.html ↩