diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-06-26 14:28:45 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-06-26 17:53:24 +0100 |
commit | 7c07cf16ab5d5bdfb64efb1d4fc5f20cf7437437 (patch) | |
tree | 8cf089ce73a842ca8095cc7f1a822095fc17d48c /compiler/typecheck/FunDeps.hs | |
parent | 0696fc6d4de28cb589f6c751b8491911a5baf774 (diff) | |
download | haskell-7c07cf16ab5d5bdfb64efb1d4fc5f20cf7437437.tar.gz |
closeOverKinds *before* oclose in coverage check
Combining functional dependencies with kind-polymorphism is
devilishly tricky! It's all documented in
Note [Closing over kinds in coverage]
Fixes Trac #10564
Diffstat (limited to 'compiler/typecheck/FunDeps.hs')
-rw-r--r-- | compiler/typecheck/FunDeps.hs | 85 |
1 files changed, 70 insertions, 15 deletions
diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs index 830873c1b9..3b44caae9d 100644 --- a/compiler/typecheck/FunDeps.hs +++ b/compiler/typecheck/FunDeps.hs @@ -387,10 +387,15 @@ checkInstCoverage be_liberal clas theta inst_taus rs_tvs = tyVarsOfTypes rs conservative_ok = rs_tvs `subVarSet` closeOverKinds ls_tvs - liberal_ok = rs_tvs `subVarSet` closeOverKinds (oclose theta ls_tvs) - -- closeOverKinds: see Note [Closing over kinds in coverage] - - msg = vcat [ sep [ ptext (sLit "The") + liberal_ok = rs_tvs `subVarSet` oclose theta (closeOverKinds ls_tvs) + -- closeOverKinds: see Note [Closing over kinds in coverage] + + msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs + -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs) + -- , text "theta" <+> ppr theta + -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs)) + -- , text "rs_tvs" <+> ppr rs_tvs + sep [ ptext (sLit "The") <+> ppWhen be_liberal (ptext (sLit "liberal")) <+> ptext (sLit "coverage condition fails in class") <+> quotes (ppr clas) @@ -406,22 +411,70 @@ checkInstCoverage be_liberal clas theta inst_taus , ppWhen (not be_liberal && liberal_ok) $ ptext (sLit "Using UndecidableInstances might help") ] -{- -Note [Closing over kinds in coverage] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Closing over kinds in coverage] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 (Trac #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. Trac #10109 is another example. + +Here is a more subtle example, from HList-0.4.0.0 (Trac #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 Trac #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}) - type Foo a = a -- Foo :: forall k. k -> k - class Bar a b | a -> b - instance Bar a (Foo a) +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). -In the instance decl, (a:k) does fix (Foo k a), but only if we notice -that (a:k) fixes k. Trac #10109 is another example. +Bottom line: + * closeOverKinds on initial seeds (in checkInstCoverage) + * and closeOverKinds whenever extending those seeds (in oclose) Note [The liberal coverage condition] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -451,12 +504,14 @@ oclose preds fixed_tvs extend fixed_tvs = foldl add fixed_tvs tv_fds where add fixed_tvs (ls,rs) - | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs + | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs | otherwise = fixed_tvs + -- closeOverKinds: see Note [Closing over kinds in coverage] tv_fds :: [(TyVarSet,TyVarSet)] - tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys) - | (xs, ys) <- concatMap determined preds ] + tv_fds = [ (tyVarsOfTypes ls, tyVarsOfTypes rs) + | pred <- preds + , (ls, rs) <- determined pred ] determined :: PredType -> [([Type],[Type])] determined pred |