Why is this instance not meeting the coverage condition?
Why UndecidableInstances
does declaring the next instance complete the coverage condition in the absence ? It seems that if a functional dependency is executed in the context, then it is executed in a new instance.
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
class Foo a b | a -> b where
instance (Foo a b, Foo a' b') => Foo (a, a') (b, b') where
If I try to reproduce the same thing with a family type, no problem.
{-# LANGUAGE TypeFamilies #-}
type family Bar a
type instance Bar (a, b) = (Bar a, Bar b)
source to share
I believe that instance limits are actually not considered when selecting an instance. They become additional restrictions that must be proven on each site of use, and do not limit the applicability of the instance.
So your instance declaration is equivalent to a value instance Foo (a, b) (c, d)
, which is rather not a coverage condition.
Adding (Foo a b, Foo a' b')
only causes some of the instance usage examples to result in "no such instance" errors, they won't actually change the types for which your instance will be selected.
source to share
From the GHC docs :
Coating condition. For every functional dependency tvsleft → tvsright, class, every type variable in S (tvsright) must appear in S (tvsleft), where S is a wildcard mapping of every type variable in the class declaration to the corresponding type in the instance declaration.
In your class, you have a -> b
, therefore, tvsleft = a
and tvsright = b
. The substitution S
maps a
to S(a)=(a,a')
and b
to S(b)=(b,b')
.
So, we find variables of type in S(tvsright)=S(b)=(b,b')
(both b
and b'
) that will not appear in S(tvsleft)=S(a)=(a,a')
. Hence, the coverage condition does not work.
As @Ben said, the coverage condition is context-insensitive: only the head of the instance matters.
source to share