X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypes%2FFunDeps.lhs;h=e3023aee27b678d4890f89b2f31ca6267232b6e4;hb=5943a1ad1ad1296251c1576722d41df83b0c8380;hp=4854e0ca8afc58fa6f5c76fcbf19b2c7a66fbc27;hpb=d069cec2bd92d4156aeab80f7eb1f222a82e4103;p=ghc-hetmet.git

diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs
index 4854e0c..e3023ae 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
 
@@ -16,10 +17,11 @@ import Name		( getSrcLoc )
 import Var		( Id, TyVar )
 import Class		( Class, FunDep, classTvsFds )
 import Subst		( mkSubst, emptyInScopeSet, substTy )
-import TcType		( Type, ThetaType, SourceType(..), PredType,
+import TcType		( Type, ThetaType, 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
@@ -168,7 +177,7 @@ 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}
@@ -264,20 +273,41 @@ mkEqnMsg (pred1,from1) (pred2,from2)
 	  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
@@ -285,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