\begin{code}
module FunDeps (
+ Equation, pprEquation, pprEquationDoc,
oclose, grow, improve, checkInstFDs, checkClsFD, pprFundeps
) where
import Name ( getSrcLoc )
import Var ( Id, TyVar )
import Class ( Class, FunDep, classTvsFds )
-import Type ( Type, ThetaType, PredType(..), predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
import Subst ( mkSubst, emptyInScopeSet, substTy )
-import Unify ( unifyTyListsX, unifyExtendTysX )
+import TcType ( Type, ThetaType, PredType(..),
+ predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred,
+ unifyTyListsX, unifyExtendTysX, tcEqType
+ )
import VarSet
import VarEnv
import Outputable
\begin{code}
grow :: [PredType] -> TyVarSet -> TyVarSet
grow preds fixed_tvs
- | null pred_sets = fixed_tvs
- | otherwise = loop fixed_tvs
+ | null preds = fixed_tvs
+ | otherwise = loop fixed_tvs
where
loop fixed_tvs
| new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
----------
type Equation = (TyVarSet, Type, Type) -- These two types should be equal, for some
-- substitution of the tyvars in the tyvar set
+ -- To "execute" the equation, make fresh type variable for each tyvar in the set,
+ -- instantiate the two types with these fresh variables, and then unify.
+ --
-- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
-- We unify z with Int, but since a and b are quantified we do nothing to them
-- We usually act on an equation by instantiating the quantified type varaibles
--
+pprEquationDoc (eqn, doc) = vcat [pprEquation eqn, nest 2 doc]
+
+pprEquation (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
+ <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2
----------
improve :: InstEnv Id -- Gives instances for given class
type InstEnv a = Class -> [(TyVarSet, [Type], a)]
-- This is a bit clumsy, because InstEnv is really
-- defined in module InstEnv. However, we don't want
--- to define it (and ClsInstEnv) here because InstEnv
+-- to define it here because InstEnv
-- is their home. Nor do we want to make a recursive
-- module group (InstEnv imports stuff from FunDeps).
\end{code}
checkGroup inst_env (p1@(IParam _ ty, _) : ips)
= -- For implicit parameters, all the types must match
- [((emptyVarSet, ty, ty'), mkEqnMsg p1 p2) | p2@(IParam _ ty', _) <- ips, ty /= ty']
+ [ ((emptyVarSet, ty, ty'), mkEqnMsg p1 p2)
+ | p2@(IParam _ ty', _) <- ips, not (ty `tcEqType` ty')]
checkGroup inst_env clss@((ClassP cls _, _) : _)
= -- For classes life is more complicated
nest 2 (sep [ppr pred2 <> comma, nest 2 from2])]
----------
-checkClsFD :: TyVarSet -- The quantified type variables, which
- -- can be instantiated to make the types match
+checkClsFD :: TyVarSet -- Quantified type variables; see note below
-> FunDep TyVar -> [TyVar] -- One functional dependency from the class
-> [Type] -> [Type]
-> [Equation]
checkClsFD qtvs fd clas_tvs tys1 tys2
+-- 'qtvs' are the quantified type variables, the ones which an be instantiated
+-- to make the types match. For example, given
+-- class C a b | a->b where ...
+-- instance C (Maybe x) (Tree x) where ..
+--
+-- and an Inst of form (C (Maybe t1) t2),
+-- then we will call checkClsFD with
+--
+-- qtvs = {x}, tys1 = [Maybe x, Tree x]
+-- tys2 = [Maybe t1, t2]
+--
+-- We can instantiate x to t1, and then we want to force
+-- (Tree x) [t1/x] :=: t2
+
-- We use 'unify' even though we are often only matching
-- unifyTyListsX will only bind variables in qtvs, so it's OK!
= case unifyTyListsX qtvs ls1 ls2 of
Nothing -> []
- Just unif -> [ (qtvs', substTy full_unif r1, substTy full_unif r2)
+ Just unif -> -- pprTrace "checkFD" (vcat [ppr_fd fd,
+ -- ppr (varSetElems qtvs) <+> (ppr ls1 $$ ppr ls2),
+ -- ppr unif]) $
+ [ (qtvs', substTy full_unif r1, substTy full_unif r2)
| (r1,r2) <- rs1 `zip` rs2,
not (maybeToBool (unifyExtendTysX qtvs unif r1 r2))]
+ -- Don't include any equations that already hold
+ -- taking account of the fact that any qtvs that aren't
+ -- already instantiated can be instantiated to anything at all
+ -- NB: qtvs, not qtvs' because unifyExtendTysX only tries to
+ -- look template tyvars up in the substitution
where
full_unif = mkSubst emptyInScopeSet unif
-- No for-alls in sight; hmm
qtvs' = filterVarSet (\v -> not (v `elemSubstEnv` unif)) qtvs
-- qtvs' are the quantified type variables
-- that have not been substituted out
+ --
+ -- Eg. class C a b | a -> b
+ -- instance C Int [y]
+ -- Given constraint C Int z
+ -- we generate the equation
+ -- ({y}, [y], z)
where
(ls1, rs1) = instFD fd clas_tvs tys1
(ls2, rs2) = instFD fd clas_tvs tys2