From 29b43fc7714e888ab5a2f5ebda18c0ceb48dfc2b Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 26 Jun 2015 14:28:45 +0100
Subject: [PATCH] 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
(cherry picked from commit 7c07cf16ab5d5bdfb64efb1d4fc5f20cf7437437)
---
compiler/typecheck/FunDeps.hs | 86 +++++++++++++++----
.../tests/typecheck/should_compile/T10564.hs | 20 +++++
.../tests/typecheck/should_compile/all.T | 1 +
3 files changed, 91 insertions(+), 16 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_compile/T10564.hs
diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs
index a6e5552b849f..dc2549b0d753 100644
--- a/compiler/typecheck/FunDeps.hs
+++ b/compiler/typecheck/FunDeps.hs
@@ -399,10 +399,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)
@@ -418,22 +423,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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -466,13 +519,14 @@ oclose preds fixed_tvs
where new_fixed_tvs = foldl extend fixed_tvs tv_fds
extend 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 000000000000..7b19f0092d96
--- /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 7bb37b47d5bb..bf0e0a0ecac2 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -445,3 +445,4 @@ test('T10195', normal, compile, [''])
test('T10109', normal, compile, [''])
test('T10335', normal, compile, [''])
test('T10489', normal, compile, [''])
+test('T10564', normal, compile, [''])
--
GitLab