Commit 2cdd9bd5 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Take account of injectivity when doing fundeps

This fixes Trac #12803. Yikes!

See Note [Care with type functions].
parent 7b0ae417
...@@ -991,6 +991,11 @@ mk_sum arity = (tycon, sum_cons) ...@@ -991,6 +991,11 @@ mk_sum arity = (tycon, sum_cons)
-- See Note [The equality types story] in TysPrim -- See Note [The equality types story] in TysPrim
-- (:~~: :: forall k1 k2 (a :: k1) (b :: k2). a -> b -> Constraint) -- (:~~: :: forall k1 k2 (a :: k1) (b :: k2). a -> b -> Constraint)
--
-- It's tempting to put functional dependencies on (~~), but it's not
-- necessary because the functional-dependency coverage check looks
-- through superclasses, and (~#) is handled in that check.
heqTyCon, coercibleTyCon :: TyCon heqTyCon, coercibleTyCon :: TyCon
heqClass, coercibleClass :: Class heqClass, coercibleClass :: Class
heqDataCon, coercibleDataCon :: DataCon heqDataCon, coercibleDataCon :: DataCon
......
...@@ -10,7 +10,7 @@ module FamInst ( ...@@ -10,7 +10,7 @@ module FamInst (
newFamInst, newFamInst,
-- * Injectivity -- * Injectivity
makeInjectivityErrors makeInjectivityErrors, injTyVarsOfType, injTyVarsOfTypes
) where ) where
import HscTypes import HscTypes
...@@ -504,35 +504,39 @@ unusedInjTvsInRHS tycon injList lhs rhs = ...@@ -504,35 +504,39 @@ unusedInjTvsInRHS tycon injList lhs rhs =
-- set of type variables appearing in the RHS on an injective position. -- set of type variables appearing in the RHS on an injective position.
-- For all returned variables we assume their associated kind variables -- For all returned variables we assume their associated kind variables
-- also appear in the RHS. -- also appear in the RHS.
injRhsVars = collectInjVars rhs injRhsVars = injTyVarsOfType rhs
-- Collect all type variables that are either arguments to a type
-- constructor or to injective type families.
collectInjVars :: Type -> VarSet
collectInjVars (TyVarTy v)
= unitVarSet v `unionVarSet` collectInjVars (tyVarKind v)
collectInjVars (TyConApp tc tys)
| isTypeFamilyTyCon tc = collectInjTFVars tys
(familyTyConInjectivityInfo tc)
| otherwise = mapUnionVarSet collectInjVars tys
collectInjVars (LitTy {})
= emptyVarSet
collectInjVars (FunTy arg res)
= collectInjVars arg `unionVarSet` collectInjVars res
collectInjVars (AppTy fun arg)
= collectInjVars fun `unionVarSet` collectInjVars arg
-- no forall types in the RHS of a type family
collectInjVars (ForAllTy {}) =
panic "unusedInjTvsInRHS.collectInjVars"
collectInjVars (CastTy ty _) = collectInjVars ty
collectInjVars (CoercionTy {}) = emptyVarSet
collectInjTFVars :: [Type] -> Injectivity -> VarSet
collectInjTFVars _ NotInjective
= emptyVarSet
collectInjTFVars tys (Injective injList)
= mapUnionVarSet collectInjVars (filterByList injList tys)
injTyVarsOfType :: TcTauType -> TcTyVarSet
-- Collect all type variables that are either arguments to a type
-- constructor or to /injective/ type families.
-- Determining the overall type determines thes variables
--
-- E.g. Suppose F is injective in its second arg, but not its first
-- then injVarOfType (Either a (F [b] (a,c))) = {a,c}
-- Determining the overall type determines a,c but not b.
injTyVarsOfType (TyVarTy v)
= unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
injTyVarsOfType (TyConApp tc tys)
| isTypeFamilyTyCon tc
= case familyTyConInjectivityInfo tc of
NotInjective -> emptyVarSet
Injective inj -> injTyVarsOfTypes (filterByList inj tys)
| otherwise
= injTyVarsOfTypes tys
injTyVarsOfType (LitTy {})
= emptyVarSet
injTyVarsOfType (FunTy arg res)
= injTyVarsOfType arg `unionVarSet` injTyVarsOfType res
injTyVarsOfType (AppTy fun arg)
= injTyVarsOfType fun `unionVarSet` injTyVarsOfType arg
-- No forall types in the RHS of a type family
injTyVarsOfType (CastTy ty _) = injTyVarsOfType ty
injTyVarsOfType (CoercionTy {}) = emptyVarSet
injTyVarsOfType (ForAllTy {}) =
panic "unusedInjTvsInRHS.injTyVarsOfType"
injTyVarsOfTypes :: [Type] -> VarSet
injTyVarsOfTypes tys = mapUnionVarSet injTyVarsOfType tys
-- | Is type headed by a type family application? -- | Is type headed by a type family application?
isTFHeaded :: Type -> Bool isTFHeaded :: Type -> Bool
......
...@@ -25,6 +25,7 @@ import Class ...@@ -25,6 +25,7 @@ import Class
import Type import Type
import TcType( transSuperClasses ) import TcType( transSuperClasses )
import Unify import Unify
import FamInst( injTyVarsOfTypes )
import InstEnv import InstEnv
import VarSet import VarSet
import VarEnv import VarEnv
...@@ -491,6 +492,36 @@ also know `t2` and the other way. ...@@ -491,6 +492,36 @@ also know `t2` and the other way.
oclose is used (only) when checking the coverage condition for oclose is used (only) when checking the coverage condition for
an instance declaration an instance declaration
Note [Equality superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 Trac #10778.
Note [Care with type functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #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.
-} -}
oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
...@@ -507,7 +538,8 @@ oclose preds fixed_tvs ...@@ -507,7 +538,8 @@ oclose preds fixed_tvs
-- closeOverKinds: see Note [Closing over kinds in coverage] -- closeOverKinds: see Note [Closing over kinds in coverage]
tv_fds :: [(TyCoVarSet,TyCoVarSet)] tv_fds :: [(TyCoVarSet,TyCoVarSet)]
tv_fds = [ (tyCoVarsOfTypes ls, tyCoVarsOfTypes rs) tv_fds = [ (tyCoVarsOfTypes ls, injTyVarsOfTypes rs)
-- See Note [Care with type functions]
| pred <- preds | pred <- preds
, pred' <- pred : transSuperClasses pred , pred' <- pred : transSuperClasses pred
-- Look for fundeps in superclasses too -- Look for fundeps in superclasses too
...@@ -517,13 +549,14 @@ oclose preds fixed_tvs ...@@ -517,13 +549,14 @@ oclose preds fixed_tvs
determined pred determined pred
= case classifyPredType pred of = case classifyPredType pred of
EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])] EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
-- See Note [Equality superclasses]
ClassPred cls tys -> [ instFD fd cls_tvs tys ClassPred cls tys -> [ instFD fd cls_tvs tys
| let (cls_tvs, cls_fds) = classTvsFds cls | let (cls_tvs, cls_fds) = classTvsFds cls
, fd <- cls_fds ] , fd <- cls_fds ]
_ -> [] _ -> []
{-
************************************************************************ {- *********************************************************************
* * * *
Check that a new instance decl is OK wrt fundeps Check that a new instance decl is OK wrt fundeps
* * * *
......
...@@ -148,7 +148,7 @@ The SrcSpan is for the entire original declaration. ...@@ -148,7 +148,7 @@ The SrcSpan is for the entire original declaration.
-} -}
mkClass :: Name -> [TyVar] mkClass :: Name -> [TyVar]
-> [([TyVar], [TyVar])] -> [FunDep TyVar]
-> [PredType] -> [Id] -> [PredType] -> [Id]
-> [ClassATItem] -> [ClassATItem]
-> [ClassOpItem] -> [ClassOpItem]
......
{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
TypeFamilies, FunctionalDependencies #-}
module T10778 where
type family F a :: *
class C a b | a -> b
instance C p (F q) => C p [q]
-- This instance should fail the (liberal) coverage condition
T12803.hs:9:10: error:
• Illegal instance declaration for ‘C p [q]’
The liberal coverage condition fails in class ‘C’
for functional dependency: ‘a -> b’
Reason: lhs type ‘p’ does not determine rhs type ‘[q]’
Un-determined variable: q
• In the instance declaration for ‘C p [q]’
...@@ -430,3 +430,4 @@ test('T12124', normal, compile_fail, ['']) ...@@ -430,3 +430,4 @@ test('T12124', normal, compile_fail, [''])
test('T12589', normal, compile_fail, ['']) test('T12589', normal, compile_fail, [''])
test('T12529', normal, compile_fail, ['']) test('T12529', normal, compile_fail, [''])
test('T12729', normal, compile_fail, ['']) test('T12729', normal, compile_fail, [''])
test('T12803', normal, compile_fail, [''])
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