\begin{code}
module FunDeps (
- Equation, pprEquation, pprEquationDoc,
+ Equation, pprEquation,
oclose, grow, improve,
- checkInstFDs, checkFunDeps,
+ checkInstCoverage, checkFunDeps,
pprFundeps
) where
import Class ( Class, FunDep, classTvsFds )
import Unify ( tcUnifyTys, BindFlag(..) )
import Type ( substTys, notElemTvSubst )
-import TcType ( Type, ThetaType, PredType(..), tcEqType,
+import TcType ( Type, PredType(..), tcEqType,
predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
import InstEnv ( Instance(..), InstEnv, instanceHead, classInstances,
instanceCantMatch, roughMatchTcs )
-- We usually act on an equation by instantiating the quantified type varaibles
-- to fresh type variables, and then calling the standard unifier.
-pprEquationDoc (eqn, doc) = vcat [pprEquation eqn, nest 2 doc]
-
pprEquation (qtvs, pairs)
= vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])]
----------
-improve :: (Class -> [Instance]) -- Gives instances for given class
- -> [(PredType,SDoc)] -- Current constraints; doc says where they come from
- -> [(Equation,SDoc)] -- Derived equalities that must also hold
- -- (NB the above INVARIANT for type Equation)
- -- The SDoc explains why the equation holds (for error messages)
+type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
+
+improve :: (Class -> [Instance]) -- Gives instances for given class
+ -> [Pred_Loc] -- Current constraints;
+ -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
+ -- (NB the above INVARIANT for type Equation)
+ -- The Pred_Locs explain which two predicates were
+ -- combined (for error messages)
\end{code}
Given a bunch of predicates that must hold, such as
----------
checkGroup :: (Class -> [Instance])
- -> [(PredType,SDoc)]
- -> [(Equation, SDoc)]
+ -> [Pred_Loc]
+ -> [(Equation, Pred_Loc, Pred_Loc)]
-- The preds are all for the same class or implicit param
checkGroup inst_env (p1@(IParam _ ty, _) : ips)
= -- For implicit parameters, all the types must match
- [ ((emptyVarSet, [(ty,ty')]), mkEqnMsg p1 p2)
+ [ ((emptyVarSet, [(ty,ty')]), p1, p2)
| p2@(IParam _ ty', _) <- ips, not (ty `tcEqType` ty')]
checkGroup inst_env clss@((ClassP cls _, _) : _)
--
-- We need to do something very similar comparing each predicate
-- with relevant instance decls
- pairwise_eqns ++ instance_eqns
+
+ instance_eqns ++ pairwise_eqns
+ -- NB: we put the instance equations first. This biases the
+ -- order so that we first improve individual constraints against the
+ -- instances (which are perhaps in a library and less likely to be
+ -- wrong; and THEN perform the pairwise checks.
+ -- The other way round, it's possible for the pairwise check to succeed
+ -- and cause a subsequent, misleading failure of one of the pair with an
+ -- instance declaration. See tcfail143.hs for an exmample
where
(cls_tvs, cls_fds) = classTvsFds cls
-- NOTE that we iterate over the fds first; they are typically
-- empty, which aborts the rest of the loop.
- pairwise_eqns :: [(Equation,SDoc)]
+ pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
pairwise_eqns -- This group comes from pairwise comparison
- = [ (eqn, mkEqnMsg p1 p2)
+ = [ (eqn, p1, p2)
| fd <- cls_fds,
p1@(ClassP _ tys1, _) : rest <- tails clss,
p2@(ClassP _ tys2, _) <- rest,
eqn <- checkClsFD emptyVarSet fd cls_tvs tys1 tys2
]
- instance_eqns :: [(Equation,SDoc)]
+ instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
instance_eqns -- This group comes from comparing with instance decls
- = [ (eqn, mkEqnMsg p1 p2)
+ = [ (eqn, p1, p2)
| fd <- cls_fds, -- Iterate through the fundeps first,
-- because there often are none!
p2@(ClassP _ tys2, _) <- clss,
ptext SLIT("arising from the instance declaration at") <+>
ppr (getSrcLoc ispec))
]
-
-mkEqnMsg (pred1,from1) (pred2,from2)
- = vcat [ptext SLIT("When using functional dependencies to combine"),
- nest 2 (sep [ppr pred1 <> comma, nest 2 from1]),
- nest 2 (sep [ppr pred2 <> comma, nest 2 from2])]
-
----------
checkClsFD :: TyVarSet -- Quantified type variables; see note below
-> FunDep TyVar -> [TyVar] -- One functional dependency from the class
\end{code}
\begin{code}
-checkInstFDs :: ThetaType -> Class -> [Type] -> Bool
--- Check that functional dependencies are obeyed in an instance decl
+checkInstCoverage :: Class -> [Type] -> Bool
+-- Check that the Coverage Condition is obeyed in an instance decl
-- For example, if we have
-- class theta => C a b | a -> b
-- instance C t1 t2
--- Then we require fv(t2) `subset` oclose(fv(t1), theta)
+-- Then we require fv(t2) `subset` fv(t1)
+-- See Note [Coverage Condition] below
-checkInstFDs theta clas inst_taus
+checkInstCoverage clas inst_taus
= all fundep_ok fds
where
(tyvars, fds) = classTvsFds clas
- fundep_ok fd = tyVarsOfTypes rs `subVarSet` oclose theta (tyVarsOfTypes ls)
+ fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
where
(ls,rs) = instFD fd tyvars inst_taus
\end{code}
+Note [Coverage condition]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+For the coverage condition, we used to require only that
+ fv(t2) `subset` oclose(fv(t1), theta)
+
+Example:
+ class Mul a b c | a b -> c where
+ (.*.) :: a -> b -> c
+
+ instance Mul Int Int Int where (.*.) = (*)
+ instance Mul Int Float Float where x .*. y = fromIntegral x * y
+ instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
+
+In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
+But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
+
+But it is a mistake to accept the instance because then this defn:
+ f = \ b x y -> if b then x .*. [y] else y
+makes instance inference go into a loop, because it requires the constraint
+ Mul a [b] b
+
%************************************************************************
%* *
projects / ghc-hetmet.git / blobdiff