[project @ 2001-07-23 10:24:57 by simonpj]

Yet another newtype-squashing bug; this time TcType.unifyTyX

diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs
index cff258a..65c2da8 100644 (file)
--- a/ghc/compiler/typecheck/TcSimplify.lhs
+++ b/ghc/compiler/typecheck/TcSimplify.lhs
@@ -1141,8 +1141,8 @@ tcImprove avails
           unifyTauTy (substTy tenv t1) (substTy tenv t2)
     ppr_eqn ((qtvs, t1, t2), doc)
        = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
-                                    <+> ppr t1 <+> equals <+> ppr t2,
-               doc]
+                                    <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2,
+               nest 2 doc]
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 8ebc1b4..90e4a3a 100644 (file)
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -752,6 +752,14 @@ uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
   | tyvar2 `elemVarSet` tmpls
   = uVarX tyvar2 ty1 k subst
 
+       -- Predicates
+uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
+  | n1 == n2 = uTysX t1 t2 k subst
+uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
+  | c1 == c2 = uTyListsX tys1 tys2 k subst
+uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
+  | tc1 == tc2 = uTyListsX tys1 tys2 k subst
+
        -- Functions; just check the two parts
 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
@@ -891,6 +899,15 @@ match (TyVarTy v) ty tmpls k senv
     -- variable may not match the pattern (TyVarTy v') as one would
     -- expect, due to an intervening Note.  KSW 2000-06.
 
+       -- Predicates
+match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
+  | n1 == n2 = match t1 t2 tmpls k senv
+match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
+  | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
+match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
+  | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+       -- Functions; just check the two parts
 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
   = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
 
@@ -900,11 +917,11 @@ match (AppTy fun1 arg1) ty2 tmpls k senv
        Nothing          -> Nothing     -- Fail
 
 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
-  | tc1 == tc2 = match_tc_app tys1 tys2 tmpls k senv
+  | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 
 -- Newtypes are opaque; other source types should not happen
 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
-  | tc1 == tc2 = match_tc_app tys1 tys2 tmpls k senv
+  | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 
 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
@@ -919,7 +936,7 @@ match ty1      (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
 -- Catch-all fails
 match _ _ _ _ _ = Nothing
 
-match_tc_app tys1 tys2 tmpls k senv
+match_list_exactly tys1 tys2 tmpls k senv
   = match_list tys1 tys2 tmpls k' senv
   where
     k' (senv', tys2') | null tys2' = k senv'   -- Succeed

diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs
index 4854e0c..f06c506 100644 (file)
--- a/ghc/compiler/types/FunDeps.lhs
+++ b/ghc/compiler/types/FunDeps.lhs
@@ -264,20 +264,35 @@ 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)
                     | (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
                  where
                    full_unif = mkSubst emptyInScopeSet unif
                        -- No for-alls in sight; hmm