[project @ 2002-09-13 15:02:25 by simonpj]
[ghc-hetmet.git] / ghc / compiler / types / FunDeps.lhs
index efbd8d6..79f62fb 100644 (file)
@@ -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
 
@@ -15,9 +16,12 @@ module FunDeps (
 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, SourceType(..), PredType,
+                         predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred,
+                         unifyTyListsX, unifyExtendTysX, tcEqType
+                       )
+import PprType         (  )
 import VarSet
 import VarEnv
 import Outputable
@@ -119,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
@@ -155,6 +159,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
@@ -211,7 +219,8 @@ checkGroup :: InstEnv Id -> [(PredType,SDoc)] -> [(Equation, SDoc)]
 
 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  
@@ -261,20 +270,40 @@ 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