[commit: ghc] master: closeOverKinds *before* oclose in coverage check (7c07cf1)
git at git.haskell.org
git at git.haskell.org
Fri Jun 26 16:53:19 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/7c07cf16ab5d5bdfb64efb1d4fc5f20cf7437437/ghc
>---------------------------------------------------------------
commit 7c07cf16ab5d5bdfb64efb1d4fc5f20cf7437437
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Jun 26 14:28:45 2015 +0100
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
>---------------------------------------------------------------
7c07cf16ab5d5bdfb64efb1d4fc5f20cf7437437
compiler/typecheck/FunDeps.hs | 85 ++++++++++++++++++----
testsuite/tests/typecheck/should_compile/T10564.hs | 20 +++++
testsuite/tests/typecheck/should_compile/all.T | 1 +
3 files changed, 91 insertions(+), 15 deletions(-)
diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs
index 830873c..3b44caa 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
diff --git a/testsuite/tests/typecheck/should_compile/T10564.hs b/testsuite/tests/typecheck/should_compile/T10564.hs
new file mode 100644
index 0000000..7b19f00
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10564.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
+ DataKinds, TypeFamilies, KindSignatures, PolyKinds, FunctionalDependencies #-}
+
+module T10564 where
+
+class HasFieldM (l :: k) r (v :: Maybe *)
+ | l r -> v
+
+class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
+ | b l r -> v
+
+class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
+ | e1 l -> r
+
+data Label a
+type family LabelsOf (a :: [*]) :: [*]
+
+instance (HMemberM (Label (l::k)) (LabelsOf xs) b,
+ HasFieldM1 b l (r xs) v)
+ => HasFieldM l (r xs) v where
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 89227c6..178f9f3 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -464,3 +464,4 @@ test('T10493', normal, compile, [''])
test('T10428', normal, compile, [''])
test('RepArrow', normal, compile, [''])
test('T10562', normal, compile, [''])
+test('T10564', normal, compile, [''])
More information about the ghc-commits
mailing list