From b20ad44787ce6f778de86aebe9504cbb11779d01 Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Mon, 23 Jul 2001 10:24:58 +0000
Subject: [PATCH] [project @ 2001-07-23 10:24:57 by simonpj] Yet another
 newtype-squashing bug; this time TcType.unifyTyX

---
 ghc/compiler/typecheck/TcSimplify.lhs |    4 ++--
 ghc/compiler/typecheck/TcType.lhs     |   23 ++++++++++++++++++++---
 ghc/compiler/types/FunDeps.lhs        |   21 ++++++++++++++++++---
 3 files changed, 40 insertions(+), 8 deletions(-)

diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs
index cff258a..65c2da8 100644
--- 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
--- 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
--- 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
-- 
1.7.10.4