X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypes%2FFunDeps.lhs;h=6fd587a2053d0fad29d31bd62a7c773561556c2d;hb=425008f93f115f9d5c92543e32838a47a7a7790f;hp=f06c50629bbbad0d5b4624348d9d7409b834d767;hpb=b20ad44787ce6f778de86aebe9504cbb11779d01;p=ghc-hetmet.git diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs index f06c506..6fd587a 100644 --- a/ghc/compiler/types/FunDeps.lhs +++ b/ghc/compiler/types/FunDeps.lhs @@ -7,6 +7,7 @@ It's better to read it as: "if we know these, then we're going to know these" \begin{code} module FunDeps ( + Equation, pprEquation, pprEquationDoc, oclose, grow, improve, checkInstFDs, checkClsFD, pprFundeps ) where @@ -20,6 +21,7 @@ import TcType ( Type, ThetaType, SourceType(..), PredType, predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred, unifyTyListsX, unifyExtendTysX, tcEqType ) +import PprType ( ) import VarSet import VarEnv import Outputable @@ -121,8 +123,8 @@ oclose preds fixed_tvs \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 @@ -148,6 +150,9 @@ grow preds 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 @@ -157,6 +162,10 @@ type Equation = (TyVarSet, Type, Type) -- These two types should be equal, for s -- +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 @@ -274,25 +283,31 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 -- 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), +-- +-- 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 +-- (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))] + 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 @@ -300,6 +315,12 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 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