[source]

compiler/typecheck/FunDeps.hs

Note [Coverage condition]

[note link]

Example

class C a b | a -> b instance theta => C t1 t2

For the coverage condition, we check

(normal) fv(t2) subset fv(t1) (liberal) fv(t2) subset oclose(fv(t1), theta)

The liberal version ensures the self-consistency of the instance, but it does not guarantee termination. Example:

class Mul a b c | a b -> c where
     (.*.) :: a -> b -> c

instance Mul Int Int Int where (.*.) = (*)
instance Mul Int Float Float where x .*. y = fromIntegral x * y
instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

In the third instance, it’s not the case that fv([c]) subset fv(a,[b]). But it is the case that fv([c]) subset oclose( theta, fv(a,[b]) )

But it is a mistake to accept the instance because then this defn:

f = b x y -> if b then x .*. [y] else y

makes instance inference go into a loop, because it requires the constraint

Mul a [b] b

Note [Closing over kinds in coverage]

[note link]

Suppose we have a fundep (a::k) -> b Then if ‘a’ is instantiated to (x y), where x:k2->*, y:k2, then fixing x really fixes k2 as well, and so k2 should be added to the lhs tyvars in the fundep check.

Example (#8391), using liberal coverage

data Foo a = … – Foo :: forall k. k -> * class Bar a b | a -> b instance Bar a (Foo a)

In the instance decl, (a:k) does fix (Foo k a), but only if we notice
that (a:k) fixes k.  #10109 is another example.

Here is a more subtle example, from HList-0.4.0.0 (#10564)

class HasFieldM (l :: k) r (v :: Maybe *)
      | l r -> v where ...
class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
      | b l r -> v where ...
class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
      | e1 l -> r

data Label :: k -> *
type family LabelsOf (a :: [*]) ::  *

instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
          HasFieldM1 b l (r xs) v)
       => HasFieldM l (r xs) v where

Is the instance OK? Does {l,r,xs} determine v? Well:

• From the instance constraint HMemberM (Label k l) (LabelsOf xs) b, plus the fundep “| el l -> r” in class HMameberM, we get {l,k,xs} -> b
• Note the ‘k’!! We must call closeOverKinds on the seed set ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b fundep won’t fire. This was the reason for #10564.
• So starting from seeds {l,r,xs,k} we do oclose to get first {l,r,xs,k,b}, via the HMemberM constraint, and then {l,r,xs,k,b,v}, via the HasFieldM1 constraint.
• And that fixes v.

However, we must closeOverKinds whenever augmenting the seed set in oclose! Consider #10109:

data Succ a – Succ :: forall k. k -> * class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab instance (Add a b ab) => Add (Succ {k1} (a :: k1))

b (Succ {k3} (ab :: k3})

We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}. Now use the fundep to extend to {a,k1,b,k2,ab}. But we need to closeOverKinds again now to {a,k1,b,k2,ab,k3}, so that we fix all the variables free in (Succ {k3} ab).

Bottom line:

• closeOverKinds on initial seeds (done automatically by tyCoVarsOfTypes in checkInstCoverage)
• and closeOverKinds whenever extending those seeds (in oclose)

Note [The liberal coverage condition]

[note link]

(oclose preds tvs) closes the set of type variables tvs, wrt functional dependencies in preds. The result is a superset of the argument set. For example, if we have

class C a b | a->b where …

then

oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}

because if we know x and y then that fixes z.

We also use equality predicates in the predicates; if we have an assumption t1 ~ t2, then we use the fact that if we know t1 we also know t2 and the other way.

eg oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}

oclose is used (only) when checking the coverage condition for an instance declaration

Note [Equality superclasses]

[note link]

Suppose we have

class (a ~ [b]) => C a b

Remember from Note [The equality types story] in TysPrim, that

• (a ~~ b) is a superclass of (a ~ b)
• (a ~# b) is a superclass of (a ~~ b)

So when oclose expands superclasses we’ll get a (a ~# [b]) superclass. But that’s an EqPred not a ClassPred, and we jolly well do want to account for the mutual functional dependencies implied by (t1 ~# t2). Hence the EqPred handling in oclose. See #10778.

Note [Care with type functions]

[note link]

Consider (#12803)

class C x y | x -> y type family F a b type family G c d = r | r -> d

Now consider

oclose (C (F a b) (G c d)) {a,b}

Knowing {a,b} fixes (F a b) regardless of the injectivity of F. But knowing (G c d) fixes only {d}, because G is only injective in its second parameter.

Hence the tyCoVarsOfTypes/injTyVarsOfTypes dance in tv_fds.