[project @ 2001-10-19 10:04:37 by sewardj]

[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs

diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs
index b9da476..444d496 100644 (file)
--- a/ghc/compiler/typecheck/TcSimplify.lhs
+++ b/ghc/compiler/typecheck/TcSimplify.lhs
@@ -46,7 +46,7 @@ import TcType         ( ThetaType, PredType, mkClassPred, isOverloadedTy,
 import Id              ( idType )
 import NameSet         ( mkNameSet )
 import Class           ( classBigSig )
-import FunDeps         ( oclose, grow, improve )
+import FunDeps         ( oclose, grow, improve, pprEquationDoc )
 import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass )
 
 import Subst           ( mkTopTyVarSubst, substTheta, substTy )
@@ -551,6 +551,9 @@ inferLoop doc tau_tvs wanteds
        --
        -- Hence the (irreds ++ frees)
 
+       -- However, NOTICE that when we are done, we might have some bindings, but
+       -- the final qtvs might be empty.  See [NO TYVARS] below.
+                               
        inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
        returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}
@@ -572,6 +575,27 @@ and improve by binding l->T, after which we can do some reduction
 on both the Lte and If constraints.  What we *can't* do is start again
 with (Max Z (S x) y)!
 
+[NO TYVARS]
+
+       class Y a b | a -> b where
+           y :: a -> X b
+       
+       instance Y [[a]] a where
+           y ((x:_):_) = X x
+       
+       k :: X a -> X a -> X a
+
+       g :: Num a => [X a] -> [X a]
+       g xs = h xs
+           where
+           h ys = ys ++ map (k (y [[0]])) xs
+
+The excitement comes when simplifying the bindings for h.  Initially
+try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
+From this we get t1:=:t2, but also various bindings.  We can't forget
+the bindings (because of [LOOP]), but in fact t1 is what g is
+polymorphic in.
+
 \begin{code}
 isFreeAndInheritable qtvs inst
   =  isFree qtvs inst                                  -- Constrains no quantified vars
@@ -1128,7 +1152,7 @@ tcImprove avails
      if null eqns then
        returnTc True
      else
-       traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns))    `thenNF_Tc_`
+       traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))     `thenNF_Tc_`
         mapTc_ unify eqns      `thenTc_`
        returnTc False
   where
@@ -1136,10 +1160,6 @@ tcImprove avails
         = tcAddErrCtxt doc                     $
           tcInstTyVars (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
           unifyTauTy (substTy tenv t1) (substTy tenv t2)
-    ppr_eqn ((qtvs, t1, t2), doc)
-       = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
-                                    <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2,
-               nest 2 doc]
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.