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 extended1 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 tvsleft -> tvsright, of the class, every type variable tdest in S(tvsright) must either appear in S(tvsleft), or there must exist a tsource in S(tvsleft) such that the functional dependencies of the instance's constraints contains a path from tsource -> t1 -> ... -> tn -> tdest
-
Original definition taken from https://downloads.haskell.org/~ghc/7.0.1/docs/html/users_guide/type-class-extensions.html
↩