Commit 29b43fc7 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Austin Seipp
Browse files

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 7c07cf16)
parent a6ef59cd
...@@ -399,10 +399,15 @@ checkInstCoverage be_liberal clas theta inst_taus ...@@ -399,10 +399,15 @@ checkInstCoverage be_liberal clas theta inst_taus
rs_tvs = tyVarsOfTypes rs rs_tvs = tyVarsOfTypes rs
conservative_ok = rs_tvs `subVarSet` closeOverKinds ls_tvs conservative_ok = rs_tvs `subVarSet` closeOverKinds ls_tvs
liberal_ok = rs_tvs `subVarSet` closeOverKinds (oclose theta ls_tvs) liberal_ok = rs_tvs `subVarSet` oclose theta (closeOverKinds ls_tvs)
-- closeOverKinds: see Note [Closing over kinds in coverage] -- closeOverKinds: see Note [Closing over kinds in coverage]
msg = vcat [ sep [ ptext (sLit "The") 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")) <+> ppWhen be_liberal (ptext (sLit "liberal"))
<+> ptext (sLit "coverage condition fails in class") <+> ptext (sLit "coverage condition fails in class")
<+> quotes (ppr clas) <+> quotes (ppr clas)
...@@ -418,22 +423,70 @@ checkInstCoverage be_liberal clas theta inst_taus ...@@ -418,22 +423,70 @@ checkInstCoverage be_liberal clas theta inst_taus
, ppWhen (not be_liberal && liberal_ok) $ , ppWhen (not be_liberal && liberal_ok) $
ptext (sLit "Using UndecidableInstances might help") ] 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 Suppose we have a fundep (a::k) -> b
Then if 'a' is instantiated to (x y), where x:k2->*, y:k2, 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 then fixing x really fixes k2 as well, and so k2 should be added to
the lhs tyvars in the fundep check. the lhs tyvars in the fundep check.
Example (Trac #8391), using liberal coverage 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 We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
class Bar a b | a -> b Now use the fundep to extend to {a,k1,b,k2,ab}. But we need to
instance Bar a (Foo a) 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 Bottom line:
that (a:k) fixes k. Trac #10109 is another example. * closeOverKinds on initial seeds (in checkInstCoverage)
* and closeOverKinds whenever extending those seeds (in oclose)
Note [The liberal coverage condition] Note [The liberal coverage condition]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
...@@ -466,13 +519,14 @@ oclose preds fixed_tvs ...@@ -466,13 +519,14 @@ oclose preds fixed_tvs
where new_fixed_tvs = foldl extend fixed_tvs tv_fds where new_fixed_tvs = foldl extend fixed_tvs tv_fds
extend fixed_tvs (ls,rs) 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 | otherwise = fixed_tvs
-- closeOverKinds: see Note [Closing over kinds in coverage]
tv_fds :: [(TyVarSet,TyVarSet)] tv_fds :: [(TyVarSet,TyVarSet)]
tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys) tv_fds = [ (tyVarsOfTypes ls, tyVarsOfTypes rs)
| (xs, ys) <- concatMap determined preds | pred <- preds
] , (ls, rs) <- determined pred ]
determined :: PredType -> [([Type],[Type])] determined :: PredType -> [([Type],[Type])]
determined pred determined pred
......
{-# 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
...@@ -445,3 +445,4 @@ test('T10195', normal, compile, ['']) ...@@ -445,3 +445,4 @@ test('T10195', normal, compile, [''])
test('T10109', normal, compile, ['']) test('T10109', normal, compile, [''])
test('T10335', normal, compile, ['']) test('T10335', normal, compile, [''])
test('T10489', normal, compile, ['']) test('T10489', normal, compile, [''])
test('T10564', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment