`[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.