Complete the evidence generation for GADTs

Mon Sep 18 14:43:22 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Complete the evidence generation for GADTs
  Sat Aug  5 21:39:51 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Complete the evidence generation for GADTs
    Thu Jul 13 17:18:07 EDT 2006  simonpj@microsoft.com
      
      This patch completes FC evidence generation for GADTs.
      
      It doesn't work properly yet, because part of the compiler thinks
      	(t1 :=: t2) => t3
      is represented with FunTy/PredTy, while the rest thinks it's represented
      using ForAllTy.  Once that's done things should start to work.

21 files changed, 263 insertions, 210 deletions

diff --git a/compiler/coreSyn/CoreTidy.lhs b/compiler/coreSyn/CoreTidy.lhs
index 7b80eacf89..35948fc0c2 100644
--- a/compiler/coreSyn/CoreTidy.lhs
+++ b/compiler/coreSyn/CoreTidy.lhs
@@ -11,13 +11,11 @@ module CoreTidy (
 
 import CoreSyn
 import CoreUtils	( exprArity )
-import DataCon		( DataCon )
-import Id		( Id, mkUserLocal, idInfo, setIdInfo, idUnique,
-			  idType, setIdType )
+import Id		( Id, mkUserLocal, idInfo, setIdInfo, idUnique, idType )
 import IdInfo		( setArityInfo, vanillaIdInfo,
 			  newStrictnessInfo, setAllStrictnessInfo,
 			  newDemandInfo, setNewDemandInfo )
-import Type		( Type, tidyType, tidyTyVarBndr, substTy, mkOpenTvSubst )
+import Type		( tidyType, tidyTyVarBndr, substTy )
 import Var		( Var, TyVar, varName )
 import VarEnv
 import UniqFM		( lookupUFM )
diff --git a/compiler/deSugar/DsArrows.lhs b/compiler/deSugar/DsArrows.lhs
index 3484a5df27..d477eff08b 100644
--- a/compiler/deSugar/DsArrows.lhs
+++ b/compiler/deSugar/DsArrows.lhs
@@ -513,8 +513,8 @@ dsCmd ids local_vars env_ids stack res_ty (HsCase exp (MatchGroup matches match_
     let
 	left_id  = HsVar (dataConWrapId left_con)
 	right_id = HsVar (dataConWrapId right_con)
-	left_expr  ty1 ty2 e = noLoc $ HsApp (noLoc $ HsCoerce (CoTyApps [ty1, ty2]) left_id ) e
-	right_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ HsCoerce (CoTyApps [ty1, ty2]) right_id) e
+	left_expr  ty1 ty2 e = noLoc $ HsApp (noLoc $ HsCoerce (mkCoTyApps [ty1, ty2]) left_id ) e
+	right_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ HsCoerce (mkCoTyApps [ty1, ty2]) right_id) e
 
 	-- Prefix each tuple with a distinct series of Left's and Right's,
 	-- in a balanced way, keeping track of the types.
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index de8e9818cf..58e42fd1ac 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -424,14 +424,14 @@ dsCoercion CoHole 	     thing_inside = thing_inside
 dsCoercion (CoCompose c1 c2) thing_inside = dsCoercion c1 (dsCoercion c2 thing_inside)
 dsCoercion (ExprCoFn co)     thing_inside = do { expr <- thing_inside
 					       ; return (Cast expr co) }
-dsCoercion (CoLams ids)      thing_inside = do { expr <- thing_inside
-					       ; return (mkLams ids expr) }
-dsCoercion (CoTyLams tvs)    thing_inside = do { expr <- thing_inside
-					       ; return (mkLams tvs expr) }
-dsCoercion (CoApps ids)      thing_inside = do { expr <- thing_inside
-					       ; return (mkVarApps expr ids) }
-dsCoercion (CoTyApps tys)    thing_inside = do { expr <- thing_inside
-					       ; return (mkTyApps expr tys) }
+dsCoercion (CoLam id)        thing_inside = do { expr <- thing_inside
+					       ; return (Lam id expr) }
+dsCoercion (CoTyLam tv)      thing_inside = do { expr <- thing_inside
+					       ; return (Lam tv expr) }
+dsCoercion (CoApp id)        thing_inside = do { expr <- thing_inside
+					       ; return (App expr (Var id)) }
+dsCoercion (CoTyApp ty)      thing_inside = do { expr <- thing_inside
+					       ; return (App expr (Type ty)) }
 dsCoercion (CoLet bs)        thing_inside = do { prs <- dsLHsBinds bs
 					       ; expr <- thing_inside
 					       ; return (Let (Rec prs) expr) }
diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index f3a0d0b316..900b8009db 100644
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -310,33 +310,48 @@ data ExprCoFn
   | ExprCoFn Coercion		-- A cast:  [] `cast` co
 				-- Guaranteedn not the identity coercion
 
-	-- Non-empty list in all of these, so that the identity coercion
-	-- is always exactly CoHole, not, say, (CoTyLams [])
-  | CoApps [Var]		-- [] x1 .. xn; the xi are dicts or coercions
-  | CoTyApps [Type]		-- [] t1 .. tn
-  | CoLams [Id] 		-- \x1..xn. []; the xi are dicts or coercions
-  | CoTyLams [TyVar] 		-- \a1..an. []
+  | CoApp Var			-- [] x; the xi are dicts or coercions
+  | CoTyApp Type		-- [] t
+  | CoLam Id	 		-- \x. []; the xi are dicts or coercions
+  | CoTyLam TyVar 		-- \a. []
+
+	-- Non-empty bindings, so that the identity coercion
+	-- is always exactly CoHole
   | CoLet (LHsBinds Id)		-- let binds in []
 				-- (ould be nicer to be core bindings)
 
-instance Outputable ExprCoFn where
-  ppr CoHole	     = ptext SLIT("<>")
-  ppr (ExprCoFn co)  = ppr co
-  ppr (CoApps ids)   = ppr CoHole <+> interppSP ids
-  ppr (CoTyApps tys) = ppr CoHole <+> hsep (map pprParendType tys)
-  ppr (CoTyLams tvs) = sep [ptext SLIT("/\\") <> hsep (map (pprBndr LambdaBind) tvs),
-		 	    ptext SLIT("->") <+> ppr CoHole]
-  ppr (CoLams ids)   = sep [ptext SLIT("\\") <> hsep (map (pprBndr LambdaBind) ids),
-			    ptext SLIT("->") <+> ppr CoHole]
-  ppr (CoLet binds)  = sep [ptext SLIT("let") <+> braces (ppr binds),
-			    ppr CoHole]
-  ppr (CoCompose co1 co2) = sep [ppr co1, ptext SLIT("<.>"), ppr co2]
+instance Outputable ExprCoFn where 
+  ppr co_fn = pprCoFn (ptext SLIT("<>")) co_fn
+
+pprCoFn it CoHole = it
+pprCoFn it (CoCompose f1 f2) = pprCoFn (pprCoFn it f2) f1
+pprCoFn it (ExprCoFn co)     = it <+> ptext SLIT("`cast`") <+> pprParendType co
+pprCoFn it (CoApp id)    = it <+> ppr id
+pprCoFn it (CoTyApp ty)  = it <+> ptext SLIT("@") <+> pprParendType ty
+pprCoFn it (CoLam id)    = ptext SLIT("\\") <> pprBndr LambdaBind id <> dot <+> it
+pprCoFn it (CoTyLam tv)  = ptext SLIT("/\\") <> pprBndr LambdaBind tv <> dot <+> it
+pprCoFn it (CoLet binds) = sep [ptext SLIT("let") <+> braces (ppr binds), it]
 
 (<.>) :: ExprCoFn -> ExprCoFn -> ExprCoFn
 CoHole <.> c = c
 c <.> CoHole = c
 c1 <.> c2    = c1 `CoCompose` c2
 
+mkCoTyApps :: [Type] -> ExprCoFn
+mkCoTyApps tys = mk_co_fn CoTyApp (reverse tys)
+
+mkCoApps :: [Id] -> ExprCoFn
+mkCoApps ids = mk_co_fn CoApp (reverse ids)
+
+mkCoTyLams :: [TyVar] -> ExprCoFn
+mkCoTyLams ids = mk_co_fn CoTyLam ids
+
+mkCoLams :: [Id] -> ExprCoFn
+mkCoLams ids = mk_co_fn CoLam ids
+
+mk_co_fn :: (a -> ExprCoFn) -> [a] -> ExprCoFn
+mk_co_fn f as = foldr (CoCompose . f) CoHole as
+
 idCoercion :: ExprCoFn
 idCoercion = CoHole
 
diff --git a/compiler/hsSyn/HsExpr.lhs b/compiler/hsSyn/HsExpr.lhs
index 25ecbb1138..18306a98de 100644
--- a/compiler/hsSyn/HsExpr.lhs
+++ b/compiler/hsSyn/HsExpr.lhs
@@ -14,7 +14,8 @@ import HsPat		( LPat )
 import HsLit		( HsLit(..), HsOverLit )
 import HsTypes		( LHsType, PostTcType )
 import HsImpExp		( isOperator, pprHsVar )
-import HsBinds		( HsLocalBinds, DictBinds, ExprCoFn, isEmptyLocalBinds )
+import HsBinds		( HsLocalBinds, DictBinds, isEmptyLocalBinds,
+			  ExprCoFn, pprCoFn )
 
 -- others:
 import Type		( Type, pprParendType )
@@ -379,10 +380,8 @@ ppr_expr (EAsPat v e) = ppr v <> char '@' <> pprParendExpr e
 ppr_expr (HsSCC lbl expr)
   = sep [ ptext SLIT("_scc_") <+> doubleQuotes (ftext lbl), pprParendExpr expr ]
 
-ppr_expr (HsCoerce co_fn e)
-  = ppr_expr e <+> ptext SLIT("`cast`") <+> ppr co_fn
-
-ppr_expr (HsType id) = ppr id
+ppr_expr (HsCoerce co_fn e) = pprCoFn (ppr_expr e) co_fn
+ppr_expr (HsType id)	    = ppr id
 
 ppr_expr (HsSpliceE s)       = pprSplice s
 ppr_expr (HsBracket b)       = pprHsBracket b
diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs
index cbc59c4ba4..1839aefa0d 100644
--- a/compiler/hsSyn/HsUtils.lhs
+++ b/compiler/hsSyn/HsUtils.lhs
@@ -72,7 +72,7 @@ mkHsApp :: LHsExpr name -> LHsExpr name -> LHsExpr name
 mkHsApp e1 e2 = addCLoc e1 e2 (HsApp e1 e2)
 
 nlHsTyApp :: name -> [Type] -> LHsExpr name
-nlHsTyApp fun_id tys = noLoc (HsCoerce (CoTyApps tys) (HsVar fun_id))
+nlHsTyApp fun_id tys = noLoc (HsCoerce (mkCoTyApps tys) (HsVar fun_id))
 
 mkLHsCoerce :: ExprCoFn -> LHsExpr id -> LHsExpr id
 mkLHsCoerce co_fn (L loc e) = L loc (mkHsCoerce co_fn e)
diff --git a/compiler/simplCore/SimplEnv.lhs b/compiler/simplCore/SimplEnv.lhs
index 3556b7eae3..960475c0b5 100644
--- a/compiler/simplCore/SimplEnv.lhs
+++ b/compiler/simplCore/SimplEnv.lhs
@@ -42,9 +42,9 @@ module SimplEnv (
 import SimplMonad	
 import Id		( Id, idType, idOccInfo, idUnfolding, setIdUnfolding )
 import IdInfo		( IdInfo, vanillaIdInfo, occInfo, setOccInfo, specInfo, setSpecInfo,
-			  arityInfo, setArityInfo, workerInfo, setWorkerInfo, 
+			  arityInfo, workerInfo, setWorkerInfo, 
 			  unfoldingInfo, setUnfoldingInfo, isEmptySpecInfo,
-			  unknownArity, workerExists
+			  workerExists
 			    )
 import CoreSyn
 import Rules		( RuleBase )
@@ -58,7 +58,7 @@ import OrdList
 import qualified CoreSubst	( Subst, mkSubst, substExpr, substSpec, substWorker )
 import qualified Type		( substTy, substTyVarBndr )
 
-import Type             ( Type, TvSubst(..), TvSubstEnv, composeTvSubst,
+import Type             ( Type, TvSubst(..), TvSubstEnv,
 			  isUnLiftedType, seqType, tyVarsOfType )
 import Coercion         ( Coercion )
 import BasicTypes	( OccInfo(..), isFragileOcc )
@@ -556,8 +556,7 @@ substIdInfo subst info
 		    not (workerExists old_wrkr) &&
 		    not (hasUnfolding (unfoldingInfo info))
     
-    keep_occ   = not (isFragileOcc old_occ)
-    old_arity = arityInfo info
+    keep_occ  = not (isFragileOcc old_occ)
     old_occ   = occInfo info
     old_rules = specInfo info
     old_wrkr  = workerInfo info
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index cc91be8239..63b5f26c27 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -12,17 +12,18 @@ module Inst (
 
 	tidyInsts, tidyMoreInsts,
 
-	newDicts, newDictsAtLoc, cloneDict, 
+	newDictBndr, newDictBndrs, newDictBndrsO,
+	instCall, instStupidTheta,
+	cloneDict, 
 	shortCutFracLit, shortCutIntLit, newIPDict, 
 	newMethod, newMethodFromName, newMethodWithGivenTy, 
-	tcInstClassOp, tcInstStupidTheta,
+	tcInstClassOp, 
 	tcSyntaxName, isHsVar,
 
 	tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
 	ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
 	instLoc, getDictClassTys, dictPred,
 
-	mkInstCoFn, 
 	lookupInst, LookupInstResult(..), lookupPred, 
 	tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
 
@@ -39,9 +40,11 @@ module Inst (
 #include "HsVersions.h"
 
 import {-# SOURCE #-}	TcExpr( tcPolyExpr )
+import {-# SOURCE #-}	TcUnify( unifyType )
 
 import HsSyn	( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp,
-		  ExprCoFn(..), (<.>), nlHsLit, nlHsVar )
+		  ExprCoFn(..), (<.>), mkCoTyApps, idCoercion,
+		  nlHsLit, nlHsVar )
 import TcHsSyn	( zonkId )
 import TcRnMonad
 import TcEnv	( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
@@ -66,7 +69,7 @@ import TcType	( Type, TcType, TcThetaType, TcTyVarSet, TcPredType,
 		  tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy, 
 		  pprPred, pprParendType, pprTheta 
 		)
-import Type	( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSubst,
+import Type	( TvSubst, substTy, substTyVar, substTyWith,
 		  notElemTvSubst, extendTvSubstList )
 import Unify	( tcMatchTys )
 import Module	( modulePackageId )
@@ -74,20 +77,18 @@ import {- Kind parts of -} Type	( isSubKind )
 import Coercion ( isEqPred )
 import HscTypes	( ExternalPackageState(..), HscEnv(..) )
 import CoreFVs	( idFreeTyVars )
-import DataCon	( DataCon, dataConStupidTheta, dataConName, 
-                  dataConWrapId, dataConUnivTyVars )
+import DataCon	( dataConWrapId )
 import Id	( Id, idName, idType, mkUserLocal, mkLocalId, isId )
 import Name	( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
 		  isInternalName, setNameUnique )
 import NameSet	( addOneToNameSet )
 import Literal	( inIntRange )
-import Var	( Var, TyVar, tyVarKind, setIdType, mkTyVar )
+import Var	( Var, TyVar, tyVarKind, setIdType, isId, mkTyVar )
 import VarEnv	( TidyEnv, emptyTidyEnv )
 import VarSet	( elemVarSet, emptyVarSet, unionVarSet, mkVarSet )
 import TysWiredIn ( floatDataCon, doubleDataCon )
 import PrelNames	( integerTyConName, fromIntegerName, fromRationalName, rationalTyConName )
 import BasicTypes( IPName(..), mapIPName, ipNameName )
-import UniqSupply( uniqsFromSupply )
 import SrcLoc	( mkSrcSpan, noLoc, unLoc, Located(..) )
 import DynFlags	( DynFlag(..), DynFlags(..), dopt )
 import Maybes	( isJust )
@@ -98,9 +99,6 @@ import Outputable
 Selection
 ~~~~~~~~~
 \begin{code}
-mkInstCoFn :: [TcType] -> [Inst] -> ExprCoFn
-mkInstCoFn tys dicts = CoApps (map instToId dicts) <.> CoTyApps tys
-
 instName :: Inst -> Name
 instName inst = idName (instToId inst)
 
@@ -212,32 +210,75 @@ linearInstType (Dict _ (IParam _ ty) _) = ty
 %*									*
 %************************************************************************
 
-\begin{code}
-newDicts :: InstOrigin
-	 -> TcThetaType
-	 -> TcM [Inst]
-newDicts orig theta
-  = getInstLoc orig		`thenM` \ loc ->
-    newDictsAtLoc loc theta
+-- newDictBndrs makes a dictionary at a binding site
+-- instCall makes a dictionary at an occurrence site
+--	and throws it into the LIE
 
-cloneDict :: Inst -> TcM Inst	-- Only used for linear implicit params
-cloneDict (Dict nm ty loc) = newUnique	`thenM` \ uniq ->
-			     returnM (Dict (setNameUnique nm uniq) ty loc)
+\begin{code}
+----------------
+newDictBndrsO :: InstOrigin -> TcThetaType -> TcM [Inst]
+newDictBndrsO orig theta = do { loc <- getInstLoc orig
+			      ; newDictBndrs loc theta }
 
-newDictsAtLoc :: InstLoc -> TcThetaType -> TcM [Inst]
-newDictsAtLoc inst_loc theta = mapM (newDictAtLoc inst_loc) theta
+newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst]
+newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
 
-{-
-newDictOcc :: InstLoc -> TcPredType -> TcM Inst
-newDictOcc inst_loc (EqPred ty1 ty2)
-  = do	{ unifyType ty1 ty2	-- We insist that they unify right away
-	; return ty1 }		-- And return the relexive coercion
--}
-newDictAtLoc inst_loc pred
+newDictBndr :: InstLoc -> TcPredType -> TcM Inst
+newDictBndr inst_loc pred
   = do 	{ uniq <- newUnique 
 	; let name = mkPredName uniq (instLocSrcLoc inst_loc) pred 
 	; return (Dict name pred inst_loc) }
 
+----------------
+instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM ExprCoFn
+-- Instantiate the constraints of a call
+--	(instCall o tys theta)
+-- (a) Makes fresh dictionaries as necessary for the constraints (theta)
+-- (b) Throws these dictionaries into the LIE
+-- (c) Eeturns an ExprCoFn ([.] tys dicts)
+
+instCall orig tys theta 
+  = do	{ loc <- getInstLoc orig
+	; (dicts, dict_app) <- instCallDicts loc theta
+	; extendLIEs dicts
+	; return (dict_app <.> mkCoTyApps tys) }
+
+----------------
+instStupidTheta :: InstOrigin -> TcThetaType -> TcM ()
+-- Similar to instCall, but only emit the constraints in the LIE
+-- Used exclusively for the 'stupid theta' of a data constructor
+instStupidTheta orig theta
+  = do	{ loc <- getInstLoc orig
+	; (dicts, _) <- instCallDicts loc theta
+	; extendLIEs dicts }
+
+----------------
+instCallDicts :: InstLoc -> TcThetaType -> TcM ([Inst], ExprCoFn)
+-- This is the key place where equality predicates 
+-- are unleashed into the world
+instCallDicts loc [] = return ([], idCoercion)
+
+instCallDicts loc (EqPred ty1 ty2 : preds)
+  = do  { unifyType ty1 ty2	-- For now, we insist that they unify right away 
+				-- Later on, when we do associated types, 
+				-- unifyType might return a coercion
+	; (dicts, co_fn) <- instCallDicts loc preds
+	; return (dicts, co_fn <.> CoTyApp ty1) }
+	-- We use type application to apply the function to the 
+	-- coercion; here ty1 *is* the appropriate identity coercion
+
+instCallDicts loc (pred : preds)
+  = do	{ uniq <- newUnique
+	; let name = mkPredName uniq (instLocSrcLoc loc) pred 
+	      dict = Dict name pred loc
+	; (dicts, co_fn) <- instCallDicts loc preds
+	; return (dict:dicts, co_fn <.> CoApp (instToId dict)) }
+
+-------------
+cloneDict :: Inst -> TcM Inst	-- Only used for linear implicit params
+cloneDict (Dict nm ty loc) = newUnique	`thenM` \ uniq ->
+			     returnM (Dict (setNameUnique nm uniq) ty loc)
+
 -- For vanilla implicit parameters, there is only one in scope
 -- at any time, so we used to use the name of the implicit parameter itself
 -- But with splittable implicit parameters there may be many in 
@@ -265,20 +306,6 @@ newIPDict orig ip_name ty
 
 
 \begin{code}
-tcInstStupidTheta :: DataCon -> [TcType] -> TcM ()
--- Instantiate the "stupid theta" of the data con, and throw 
--- the constraints into the constraint set
-tcInstStupidTheta data_con inst_tys
-  | null stupid_theta
-  = return ()
-  | otherwise
-  = do	{ stupid_dicts <- newDicts (OccurrenceOf (dataConName data_con))
-				   (substTheta tenv stupid_theta)
-	; extendLIEs stupid_dicts }
-  where
-    stupid_theta = dataConStupidTheta data_con
-    tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
-
 newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
 newMethodFromName origin ty name
   = tcLookupId name		`thenM` \ id ->
@@ -592,8 +619,8 @@ lookupInst :: Inst -> TcM LookupInstResult
 -- Methods
 
 lookupInst inst@(Method _ id tys theta loc)
-  = do	{ dicts <- newDictsAtLoc loc theta
-	; let co_fn = mkInstCoFn tys dicts
+  = do	{ (dicts, dict_app) <- instCallDicts loc theta
+	; let co_fn = dict_app <.> mkCoTyApps tys
 	; return (GenInst dicts (L span $ HsCoerce co_fn (HsVar id))) }
   where
     span = instLocSrcSpan loc
@@ -671,10 +698,10 @@ lookupInst (Dict _ pred loc)
 	dfun	   = HsVar dfun_id
 	tys	   = map (substTyVar tenv') tyvars
     ; if null theta then
-    	returnM (SimpleInst (L src_loc $ HsCoerce (CoTyApps tys) dfun))
+    	returnM (SimpleInst (L src_loc $ HsCoerce (mkCoTyApps tys) dfun))
       else do
-    { dicts <- newDictsAtLoc loc theta
-    ; let co_fn = mkInstCoFn tys dicts
+    { (dicts, dict_app) <- instCallDicts loc theta
+    ; let co_fn = dict_app <.> mkCoTyApps tys
     ; returnM (GenInst dicts (L src_loc $ HsCoerce co_fn dfun))
     }}}}
 
diff --git a/compiler/typecheck/TcArrows.lhs b/compiler/typecheck/TcArrows.lhs
index b4afcaf30a..2316162c18 100644
--- a/compiler/typecheck/TcArrows.lhs
+++ b/compiler/typecheck/TcArrows.lhs
@@ -264,7 +264,7 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
 		-- the s1..sm and check each cmd
 	; cmds' <- mapM (tc_cmd w_tv) cmds_w_tys
 
-	; returnM (HsArrForm (noLoc $ HsCoerce (CoTyLams [w_tv]) 
+	; returnM (HsArrForm (noLoc $ HsCoerce (CoTyLam w_tv) 
 					       (unLoc $ mkHsDictLet inst_binds expr')) 
 			     fixity cmds')
 	}
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 9cc66e3951..4223af4da4 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -28,7 +28,7 @@ import HsSyn		( HsExpr(..), HsBind(..), LHsBinds, LHsBind, Sig(..),
 import TcHsSyn		( zonkId )
 
 import TcRnMonad
-import Inst		( newDictsAtLoc, newIPDict, instToId )
+import Inst		( newDictBndrs, newIPDict, instToId )
 import TcEnv		( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 
 			  pprBinders, tcLookupId,
 			  tcGetGlobalTyVars )
@@ -773,7 +773,7 @@ might not otherwise be related.  This is a rather subtle issue.
 unifyCtxts :: [TcSigInfo] -> TcM [Inst]
 unifyCtxts (sig1 : sigs) 	-- Argument is always non-empty
   = do	{ mapM unify_ctxt sigs
-	; newDictsAtLoc (sig_loc sig1) (sig_theta sig1) }
+	; newDictBndrs (sig_loc sig1) (sig_theta sig1) }
   where
     theta1 = sig_theta sig1
     unify_ctxt :: TcSigInfo -> TcM ()
diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs
index 31e3d5a0b2..25795cef9a 100644
--- a/compiler/typecheck/TcClassDcl.lhs
+++ b/compiler/typecheck/TcClassDcl.lhs
@@ -16,7 +16,7 @@ import HsSyn
 import RnHsSyn		( maybeGenericMatch, extractHsTyVars )
 import RnExpr		( rnLExpr )
 import RnEnv		( lookupTopBndrRn, lookupImportedName )
-import Inst		( instToId, newDicts, newDictsAtLoc, newMethod, getOverlapFlag )
+import Inst		( instToId, newDictBndr, newDictBndrs, newMethod, getOverlapFlag )
 import InstEnv		( mkLocalInstance )
 import TcEnv		( tcLookupLocatedClass, 
 			  tcExtendTyVarEnv, tcExtendIdEnv,
@@ -246,9 +246,13 @@ tcClassDecl2 (L loc (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
 	-- default methods.  Better to make separate AbsBinds for each
     let
 	(tyvars, _, _, op_items) = classBigSig clas
+	rigid_info  		 = ClsSkol clas
+	origin 			 = SigOrigin rigid_info
 	prag_fn			 = mkPragFun sigs
 	sig_fn			 = mkTcSigFun sigs
-	tc_dm			 = tcDefMeth clas tyvars default_binds sig_fn prag_fn
+	clas_tyvars		 = tcSkolSigTyVars rigid_info tyvars
+	tc_dm			 = tcDefMeth origin clas clas_tyvars
+					     default_binds sig_fn prag_fn
 
 	dm_sel_ids		 = [sel_id | (sel_id, DefMeth) <- op_items]
 	-- Generate code for polymorphic default methods only
@@ -261,19 +265,17 @@ tcClassDecl2 (L loc (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
     mapAndUnzipM tc_dm dm_sel_ids	`thenM` \ (defm_binds, dm_ids_s) ->
     returnM (listToBag defm_binds, concat dm_ids_s)
     
-tcDefMeth clas tyvars binds_in sig_fn prag_fn sel_id
+tcDefMeth origin clas tyvars binds_in sig_fn prag_fn sel_id
   = do	{ dm_name <- lookupTopBndrRn (mkDefMethRdrName sel_id)
-	; let	rigid_info  = ClsSkol clas
-		clas_tyvars = tcSkolSigTyVars rigid_info tyvars
-		inst_tys    = mkTyVarTys clas_tyvars
+	; let	inst_tys    = mkTyVarTys tyvars
 		dm_ty       = idType sel_id	-- Same as dict selector!
-	        theta       = [mkClassPred clas inst_tys]
+	        cls_pred    = mkClassPred clas inst_tys
 		local_dm_id = mkDefaultMethodId dm_name dm_ty
-		origin 	    = SigOrigin rigid_info
 
 	; (_, meth_info) <- mkMethodBind origin clas inst_tys binds_in (sel_id, DefMeth)
-	; [this_dict] <- newDicts origin theta
-	; (defm_bind, insts_needed) <- getLIE (tcMethodBind clas_tyvars theta [this_dict]
+	; loc <- getInstLoc origin
+	; this_dict <- newDictBndr loc cls_pred
+	; (defm_bind, insts_needed) <- getLIE (tcMethodBind tyvars [cls_pred] [this_dict]
 							    sig_fn prag_fn meth_info)
     
 	; addErrCtxt (defltMethCtxt clas) $ do
@@ -281,12 +283,12 @@ tcDefMeth clas tyvars binds_in sig_fn prag_fn sel_id
         -- Check the context
 	{ dict_binds <- tcSimplifyCheck
 			        (ptext SLIT("class") <+> ppr clas)
-				clas_tyvars
+				tyvars
 			        [this_dict]
 			        insts_needed
 
 	-- Simplification can do unification
-	; checkSigTyVars clas_tyvars
+	; checkSigTyVars tyvars
     
 	-- Inline pragmas 
 	-- We'll have an inline pragma on the local binding, made by tcMethodBind
@@ -297,9 +299,9 @@ tcDefMeth clas tyvars binds_in sig_fn prag_fn sel_id
 	      inline_prags     = filter isInlineLSig (prag_fn sel_name)
 	; prags <- tcPrags dm_inst_id inline_prags
 
-	; let full_bind = AbsBinds  clas_tyvars
+	; let full_bind = AbsBinds  tyvars
 		    		    [instToId this_dict]
-		    		    [(clas_tyvars, local_dm_id, dm_inst_id, prags)]
+		    		    [(tyvars, local_dm_id, dm_inst_id, prags)]
 		    		    (dict_binds `unionBags` defm_bind)
 	; returnM (noLoc full_bind, [local_dm_id]) }}
 
@@ -374,7 +376,7 @@ tcMethodBind inst_tyvars inst_theta avail_insts sig_fn prag_fn
     in
 
     addErrCtxtM (sigCtxt sel_id inst_tyvars inst_theta (idType meth_id))	$
-    newDictsAtLoc (sig_loc sig) (sig_theta sig)		`thenM` \ meth_dicts ->
+    newDictBndrs (sig_loc sig) (sig_theta sig)		`thenM` \ meth_dicts ->
     let
 	meth_tvs   = sig_tvs sig
 	all_tyvars = meth_tvs ++ inst_tyvars
diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs
index b3e0d7fdea..1d093e2e7c 100644
--- a/compiler/typecheck/TcEnv.lhs
+++ b/compiler/typecheck/TcEnv.lhs
@@ -45,19 +45,19 @@ module TcEnv(
 
 import HsSyn		( LRuleDecl, LHsBinds, LSig, 
 			  LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds,
-		 	  ExprCoFn(..), idCoercion, (<.>) )
+		 	  idCoercion, (<.>) )
 import TcIface		( tcImportDecl )
 import IfaceEnv		( newGlobalBinder )
 import TcRnMonad
 import TcMType		( zonkTcType, zonkTcTyVarsAndFV )
-import TcType		( Type, TcKind, TcTyVar, TcTyVarSet, TcType, TvSubst,
-			  substTy, substTyVar, tyVarsOfType, tcTyVarsOfTypes, mkTyConApp,
+import TcType		( Type, TcKind, TcTyVar, TcTyVarSet, TcType, 
+			  substTy, tyVarsOfType, tcTyVarsOfTypes, mkTyConApp,
 			  getDFunTyKey, tcTyConAppTyCon, tcGetTyVar, mkTyVarTy,
 			  tidyOpenType, isRefineableTy
 			)
 import TcGadt		( Refinement, refineType )
 import qualified Type	( getTyVar_maybe )
-import Id		( idName, isLocalId, setIdType )
+import Id		( idName, isLocalId )
 import Var		( TyVar, Id, idType, tyVarName )
 import VarSet
 import VarEnv
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index 43360c7edf..bda4e2facf 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -29,15 +29,15 @@ import TcUnify		( tcInfer, tcSubExp, tcFunResTy, tcGen, boxyUnify, subFunTys, za
 			  boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, preSubType,
 			  unBox )
 import BasicTypes	( Arity, isMarkedStrict )
-import Inst		( newMethodFromName, newIPDict, mkInstCoFn,
-			  newDicts, newMethodWithGivenTy, tcInstStupidTheta )
+import Inst		( newMethodFromName, newIPDict, instCall,
+			  newMethodWithGivenTy, instStupidTheta )
 import TcBinds		( tcLocalBinds )
 import TcEnv		( tcLookup, tcLookupDataCon, tcLookupField )
 import TcArrows		( tcProc )
 import TcMatches	( tcMatchesCase, tcMatchLambda, tcDoStmts, tcBody,
 			  TcMatchCtxt(..) )
 import TcHsType		( tcHsSigType, UserTypeCtxt(..) )
-import TcPat		( tcOverloadedLit, badFieldCon )
+import TcPat		( tcOverloadedLit, addDataConStupidTheta, badFieldCon )
 import TcMType		( tcInstTyVars, newFlexiTyVarTy, newBoxyTyVars,
 			  readFilledBox, zonkTcTypes )
 import TcType		( TcType, TcSigmaType, TcRhoType, TvSubst,
@@ -489,14 +489,11 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _) res_ty
 	-- dictionaries for the data type context, since we are going to
 	-- do pattern matching over the data cons.
 	--
-	-- What dictionaries do we need?  
-	-- We just take the context of the first data constructor
-	-- This isn't right, but I just can't bear to union up all the relevant ones
+	-- What dictionaries do we need?  The tyConStupidTheta tells us.
     let
 	theta' = substTheta inst_env (tyConStupidTheta tycon)
     in
-    newDicts RecordUpdOrigin theta'	`thenM` \ dicts ->
-    extendLIEs dicts			`thenM_`
+    instStupidTheta RecordUpdOrigin theta'	`thenM_`
 
 	-- Phew!
     returnM (mkHsCoerce co_fn (RecordUpd record_expr' rbinds' record_ty result_record_ty))
@@ -791,7 +788,8 @@ instFun orig fun subst tv_theta_prs
 	= (map (substTyVar subst) tvs, substTheta subst theta)
 
     inst_stupid (HsVar fun_id) ((tys,_):_)
-	| Just con <- isDataConId_maybe fun_id = tcInstStupidTheta con tys
+	| Just con <- isDataConId_maybe fun_id 
+	= addDataConStupidTheta orig con tys
     inst_stupid _ _ = return ()
 
     go _ fun [] = return fun
@@ -804,9 +802,7 @@ instFun orig fun subst tv_theta_prs
 		-- of newMethod: see Note [Multiple instantiation]
 
     go _ fun ((tys, theta) : prs)
-	= do { dicts <- newDicts orig theta
-	     ; extendLIEs dicts
-	     ; let co_fn = mkInstCoFn tys dicts
+	= do { co_fn <- instCall orig tys theta
 	     ; go False (HsCoerce co_fn fun) prs }
 
 	-- 	Hack Alert (want_method_inst)!
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 8ab91ce893..4e650c53ee 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -537,14 +537,14 @@ zonkCoFn env (ExprCoFn co)     = do { co' <- zonkTcTypeToType env co
 zonkCoFn env (CoCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
 				    ; (env2, c2') <- zonkCoFn env1 c2
 				    ; return (env2, CoCompose c1' c2') }
-zonkCoFn env (CoLams ids)   = do { ids' <- zonkIdBndrs env ids
-				 ; let env1 = extendZonkEnv env ids'
-				 ; return (env1, CoLams ids') }
-zonkCoFn env (CoTyLams tvs) = ASSERT( all isImmutableTyVar tvs )
-			      do { return (env, CoTyLams tvs) }
-zonkCoFn env (CoApps ids)   = do { return (env, CoApps (zonkIdOccs env ids)) }
-zonkCoFn env (CoTyApps tys) = do { tys' <- zonkTcTypeToTypes env tys
-				 ; return (env, CoTyApps tys') }
+zonkCoFn env (CoLam id)     = do { id' <- zonkIdBndr env id
+				 ; let env1 = extendZonkEnv1 env id'
+				 ; return (env1, CoLam id') }
+zonkCoFn env (CoTyLam tv)   = ASSERT( isImmutableTyVar tv )
+			      do { return (env, CoTyLam tv) }
+zonkCoFn env (CoApp id)     = do { return (env, CoApp (zonkIdOcc env id)) }
+zonkCoFn env (CoTyApp ty)   = do { ty' <- zonkTcTypeToType env ty
+				 ; return (env, CoTyApp ty') }
 zonkCoFn env (CoLet bs)     = do { (env1, bs') <- zonkRecMonoBinds env bs
 				 ; return (env1, CoLet bs') }
 
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 1bb1bb7671..ba57563806 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -14,9 +14,9 @@ import TcClassDcl	( tcMethodBind, mkMethodBind, badMethodErr,
 			  tcClassDecl2, getGenericInstances )
 import TcRnMonad       
 import TcMType		( tcSkolSigType, checkValidInstance, checkValidInstHead )
-import TcType		( mkClassPred, tcSplitSigmaTy, tcSplitDFunHead, mkTyVarTys,
+import TcType		( mkClassPred, tcSplitSigmaTy, tcSplitDFunHead, 
                           SkolemInfo(InstSkol), tcSplitDFunTy, mkFunTy )
-import Inst		( tcInstClassOp, newDicts, instToId, showLIE, 
+import Inst		( newDictBndr, newDictBndrs, instToId, showLIE, 
 			  getOverlapFlag, tcExtendLocalInstEnv )
 import InstEnv		( mkLocalInstance, instanceDFunId )
 import TcDeriv		( tcDeriving )
@@ -25,19 +25,19 @@ import TcEnv		( InstInfo(..), InstBindings(..),
 			)
 import TcHsType		( kcHsSigType, tcHsKindedType )
 import TcUnify		( checkSigTyVars )
-import TcSimplify	( tcSimplifyCheck, tcSimplifySuperClasses )
-import Type		( zipOpenTvSubst, substTheta, substTys, mkTyConApp, mkTyVarTy )
+import TcSimplify	( tcSimplifySuperClasses )
+import Type		( zipOpenTvSubst, substTheta, mkTyConApp, mkTyVarTy )
 import Coercion         ( mkAppCoercion, mkAppsCoercion )
 import TyCon            ( TyCon, newTyConCo )
 import DataCon		( classDataCon, dataConTyCon, dataConInstArgTys )
-import Class		( classBigSig, classMethods )
+import Class		( classBigSig )
 import Var		( TyVar, Id, idName, idType )
 import Id               ( mkSysLocal )
 import UniqSupply       ( uniqsFromSupply, splitUniqSupply )
 import MkId		( mkDictFunId )
 import Name		( Name, getSrcLoc )
 import Maybe		( catMaybes )
-import SrcLoc		( noSrcSpan, srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart )
+import SrcLoc		( srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart )
 import ListSetOps	( minusList )
 import Outputable
 import Bag
@@ -309,7 +309,7 @@ First comes the easy case of a non-local instance decl.
 tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
 -- Returns a binding for the dfun
 
---
+------------------------
 -- Derived newtype instances
 --
 -- We need to make a copy of the dictionary we are deriving from
@@ -334,22 +334,20 @@ tcInstDecl2 (InstInfo { iSpec = ispec,
 	      rigid_info   = InstSkol dfun_id
 	      origin	   = SigOrigin rigid_info
 	      inst_ty      = idType dfun_id
-              maybe_co_con = newTyConCo tycon
+	; inst_loc <- getInstLoc origin
 	; (tvs, theta, inst_head) <- tcSkolSigType rigid_info inst_ty
-	; dicts <- newDicts origin theta
+	; dicts <- newDictBndrs inst_loc theta
         ; uniqs <- newUniqueSupply
         ; let (cls, cls_inst_tys) = tcSplitDFunHead inst_head
-        ; [this_dict] <- newDicts origin [mkClassPred cls rep_tys]
-        ; let (rep_dict_id:sc_dict_ids) =
-                 if null dicts then
-                     [instToId this_dict]
-                 else
-                     map instToId dicts
+        ; this_dict <- newDictBndr inst_loc (mkClassPred cls rep_tys)
+        ; let (rep_dict_id:sc_dict_ids)
+                 | null dicts = [instToId this_dict]
+ 		 | otherwise  = map instToId dicts
 
 		-- (Here, we are relying on the order of dictionary 
 		-- arguments built by NewTypeDerived in TcDeriv.)
 
-              wrap_fn = CoTyLams tvs <.> CoLams (rep_dict_id:sc_dict_ids)
+              wrap_fn = mkCoTyLams tvs <.> mkCoLams (rep_dict_id:sc_dict_ids)
 	 
               coerced_rep_dict = mkHsCoerce (co_fn tvs cls_tycon) (HsVar rep_dict_id)
 
@@ -358,7 +356,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec,
 				 MatchGroup [the_match] (mkFunTy in_dict_ty inst_head)
 	      in_dict_ty = mkTyConApp cls_tycon cls_inst_tys
 
-              the_match = mkSimpleMatch [the_pat] the_rhs
+              the_match = mkSimpleMatch [noLoc the_pat] the_rhs
+	      the_rhs = mkHsConApp cls_data_con cls_inst_tys (map HsVar (sc_dict_ids ++ op_ids))
 
 	      (uniqs1, uniqs2) = splitUniqSupply uniqs
 
@@ -368,23 +367,21 @@ tcInstDecl2 (InstInfo { iSpec = ispec,
               dict_ids = zipWith (mkSysLocal FSLIT("dict"))
                           (uniqsFromSupply uniqs2) (map idType sc_dict_ids)
 
-	      the_pat = noLoc $
-                        ConPatOut { pat_con = noLoc cls_data_con, pat_tvs = [],
+	      the_pat = ConPatOut { pat_con = noLoc cls_data_con, pat_tvs = [],
 				    pat_dicts = dict_ids,
 				    pat_binds = emptyLHsBinds,
 				    pat_args = PrefixCon (map nlVarPat op_ids),
 				    pat_ty = in_dict_ty} 
 
               cls_data_con = classDataCon cls
-              cls_tycon = dataConTyCon cls_data_con
-              cls_arg_tys = dataConInstArgTys cls_data_con cls_inst_tys 
+              cls_tycon    = dataConTyCon cls_data_con
+              cls_arg_tys  = dataConInstArgTys cls_data_con cls_inst_tys 
               
               n_dict_args = if length dicts == 0 then 0 else length dicts - 1
               op_tys = drop n_dict_args cls_arg_tys
               
-	      the_rhs = mkHsConApp cls_data_con cls_inst_tys (map HsVar (sc_dict_ids ++ op_ids))
-              dict = (mkHsCoerce wrap_fn body)
-        ; return (unitBag (noLoc $ VarBind (dfun_id) (noLoc dict))) }
+              dict    = mkHsCoerce wrap_fn body
+        ; return (unitBag (noLoc $ VarBind dfun_id (noLoc dict))) }
   where
     co_fn :: [TyVar] -> TyCon -> ExprCoFn
     co_fn tvs cls_tycon | Just co_con <- newTyConCo tycon
@@ -395,6 +392,9 @@ tcInstDecl2 (InstInfo { iSpec = ispec,
 	  | otherwise
 	  = idCoercion
 
+------------------------
+-- Ordinary instances
+
 tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
   = let 
 	dfun_id    = instanceDFunId ispec
@@ -420,9 +420,11 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
 	origin	  = SigOrigin rigid_info
     in
 	 -- Create dictionary Ids from the specified instance contexts.
-    newDicts InstScOrigin sc_theta'			`thenM` \ sc_dicts ->
-    newDicts origin dfun_theta'				`thenM` \ dfun_arg_dicts ->
-    newDicts origin [mkClassPred clas inst_tys'] 	`thenM` \ [this_dict] ->
+    getInstLoc InstScOrigin				`thenM` \ sc_loc -> 
+    newDictBndrs sc_loc sc_theta'			`thenM` \ sc_dicts ->
+    getInstLoc origin					`thenM` \ inst_loc -> 
+    newDictBndrs inst_loc dfun_theta'			`thenM` \ dfun_arg_dicts ->
+    newDictBndr inst_loc (mkClassPred clas inst_tys') 	`thenM` \ this_dict ->
 		-- Default-method Ids may be mentioned in synthesised RHSs,
 		-- but they'll already be in the environment.
 
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index 33b76302c9..2316c9395d 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -5,7 +5,7 @@
 
 \begin{code}
 module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
-	       badFieldCon, polyPatSig ) where
+	       addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
 
@@ -17,7 +17,7 @@ import HsSyn		( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExp
 import TcHsSyn		( TcId, hsLitType )
 import TcRnMonad
 import Inst		( InstOrigin(..), shortCutFracLit, shortCutIntLit, 
-			  newDicts, instToId, tcInstStupidTheta, isHsVar
+			  newDictBndrs, instToId, instStupidTheta, isHsVar
 			)
 import Id		( Id, idType, mkLocalId )
 import CoreFVs		( idFreeTyVars )
@@ -47,7 +47,8 @@ import Type		( substTys, substTheta )
 import StaticFlags	( opt_IrrefutableTuples )
 import TyCon		( TyCon, FieldLabel )
 import DataCon		( DataCon, dataConTyCon, dataConFullSig, dataConName,
-			  dataConFieldLabels, dataConSourceArity )
+			  dataConFieldLabels, dataConSourceArity, 
+			  dataConStupidTheta, dataConUnivTyVars )
 import PrelNames	( integralClassName, fromIntegerName, integerTyConName, 
 			  fromRationalName, rationalTyConName )
 import BasicTypes	( isBoxed )
@@ -460,8 +461,7 @@ tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 	-- The Report says that n+k patterns must be in Integral
 	-- We may not want this when using re-mappable syntax, though (ToDo?)
 	; icls <- tcLookupClass integralClassName
-	; dicts <- newDicts orig [mkClassPred icls [pat_ty']]	
-	; extendLIEs dicts
+	; instStupidTheta orig [mkClassPred icls [pat_ty']]	
     
 	; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
 	; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
@@ -490,6 +490,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
   = do	{ span <- getSrcSpanM	-- Span for the whole pattern
 	; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
 	      skol_info = PatSkol data_con span
+	      origin    = SigOrigin skol_info
 
 	  -- Instantiate the constructor type variables [a->ty]
 	; ctxt_res_tys <- boxySplitTyConApp tycon pat_ty
@@ -506,10 +507,11 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 	; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 		tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
 
-	; dicts <- newDicts (SigOrigin skol_info) theta'
+	; loc <- getInstLoc origin
+	; dicts <- newDictBndrs loc theta'
 	; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
 
-	; tcInstStupidTheta data_con ctxt_res_tys
+	; addDataConStupidTheta origin data_con ctxt_res_tys
 
 	; return (ConPatOut { pat_con = L con_span data_con, 
 			      pat_tvs = ex_tvs' ++ co_vars,
@@ -589,6 +591,19 @@ tcConArg (arg_pat, arg_ty) pstate thing_inside
 	--     refinements from peer argument patterns to the left
 \end{code}
 
+\begin{code}
+addDataConStupidTheta :: InstOrigin -> DataCon -> [TcType] -> TcM ()
+-- Instantiate the "stupid theta" of the data con, and throw 
+-- the constraints into the constraint set
+addDataConStupidTheta origin data_con inst_tys
+  | null stupid_theta = return ()
+  | otherwise	      = instStupidTheta origin inst_theta
+  where
+    stupid_theta = dataConStupidTheta data_con
+    tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
+    inst_theta = substTheta tenv stupid_theta
+\end{code}
+
 
 %************************************************************************
 %*									*
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index c0bb23bc47..98fdaf921c 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -21,19 +21,19 @@ module TcSimplify (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TcUnify( unifyType )
-import HsSyn		( HsBind(..), HsExpr(..), LHsExpr, 
+import HsSyn		( HsBind(..), HsExpr(..), LHsExpr, mkCoTyApps,
 			  ExprCoFn(..), (<.>), nlHsTyApp, emptyLHsBinds )
 import TcHsSyn		( mkHsApp )
 
 import TcRnMonad
 import Inst		( lookupInst, LookupInstResult(..),
-			  tyVarsOfInst, fdPredsOfInsts, newDicts, 
+			  tyVarsOfInst, fdPredsOfInsts,
 			  isDict, isClassDict, isLinearInst, linearInstType,
 			  isMethodFor, isMethod,
 			  instToId, tyVarsOfInsts,  cloneDict,
 			  ipNamesOfInsts, ipNamesOfInst, dictPred,
-			  fdPredsOfInst, mkInstCoFn,
-			  newDictsAtLoc, tcInstClassOp,
+			  fdPredsOfInst, 
+			  newDictBndrs, newDictBndrsO, tcInstClassOp,
 			  getDictClassTys, isTyVarDict, instLoc,
 			  zonkInst, tidyInsts, tidyMoreInsts,
 			  pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
@@ -1912,7 +1912,7 @@ addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
 	-- Invariant: the Inst is already in Avails.
 
 addSCs is_loop avails dict
-  = do	{ sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
+  = do	{ sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
 	; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
   where
     (clas, tys) = getDictClassTys dict
@@ -1925,7 +1925,7 @@ addSCs is_loop avails dict
       | otherwise		   = addSCs is_loop avails' sc_dict
       where
 	sc_sel_rhs = L (instSpan dict) (HsCoerce co_fn (HsVar sc_sel))
-	co_fn	   = mkInstCoFn tys [dict]
+	co_fn	   = CoApp (instToId dict) <.> mkCoTyApps tys
 	avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
 
     is_given :: Inst -> Bool
@@ -2279,7 +2279,7 @@ tcSimplifyDeriv tc tyvars theta
 	-- The main loop may do unification, and that may crash if 
 	-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
 	-- ToDo: what if two of them do get unified?
-    newDicts DerivOrigin (substTheta tenv theta)	`thenM` \ wanteds ->
+    newDictBndrsO DerivOrigin (substTheta tenv theta)	`thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds		`thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )			-- reduceMe never returns Free
 
@@ -2325,7 +2325,7 @@ tcSimplifyDefault :: ThetaType	-- Wanted; has no type variables in it
 		  -> TcM ()
 
 tcSimplifyDefault theta
-  = newDicts DefaultOrigin theta		`thenM` \ wanteds ->
+  = newDictBndrsO DefaultOrigin theta		`thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds	`thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )	-- try_me never returns Free
     addNoInstanceErrs Nothing []  irreds 	`thenM_`
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 84d944a0d0..55e20fc3cf 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -187,7 +187,7 @@ import PrelNames	-- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn	( unitTyCon, charTyCon, listTyCon )
 import BasicTypes	( IPName(..), Arity, ipNameName )
 import SrcLoc		( SrcLoc, SrcSpan )
-import Util		( snocView, equalLength )
+import Util		( equalLength )
 import Maybes		( maybeToBool, expectJust, mapCatMaybes )
 import ListSetOps	( hasNoDups )
 import List		( nubBy )
@@ -988,8 +988,9 @@ tcTyVarsOfTypes :: [Type] -> TyVarSet
 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
 
 tcTyVarsOfPred :: PredType -> TyVarSet
-tcTyVarsOfPred (IParam _ ty)  = tcTyVarsOfType ty
-tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys
+tcTyVarsOfPred (IParam _ ty)  	= tcTyVarsOfType ty
+tcTyVarsOfPred (ClassP _ tys) 	= tcTyVarsOfTypes tys
+tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
 \end{code}
 
 Note [Silly type synonym]
@@ -1026,8 +1027,9 @@ exactTyVarsOfType ty
     go (AppTy fun arg)	    	  = go fun `unionVarSet` go arg
     go (ForAllTy tyvar ty)  	  = delVarSet (go ty) tyvar
 
-    go_pred (IParam _ ty)  = go ty
-    go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
+    go_pred (IParam _ ty)    = go ty
+    go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
+    go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
 
 exactTyVarsOfTypes :: [TcType] -> TyVarSet
 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
@@ -1043,6 +1045,7 @@ tyClsNamesOfType (TyConApp tycon tys)	    = unitNameSet (getName tycon) `unionNa
 tyClsNamesOfType (NoteTy _ ty2) 	    = tyClsNamesOfType ty2
 tyClsNamesOfType (PredTy (IParam n ty))     = tyClsNamesOfType ty
 tyClsNamesOfType (PredTy (ClassP cl tys))   = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (PredTy (EqPred ty1 ty2))  = tyClsNamesOfType ty1 `unionNameSets` tyClsNamesOfType ty2
 tyClsNamesOfType (FunTy arg res)	    = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
 tyClsNamesOfType (AppTy fun arg)	    = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
 tyClsNamesOfType (ForAllTy tyvar ty)	    = tyClsNamesOfType ty
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 1295ab3dfe..000024e1b3 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -25,7 +25,8 @@ module TcUnify (
 
 #include "HsVersions.h"
 
-import HsSyn		( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) )
+import HsSyn		( ExprCoFn(..), idCoercion, isIdCoercion, (<.>),
+			  mkCoLams, mkCoTyLams, mkCoApps )
 import TypeRep		( Type(..), PredType(..) )
 
 import TcMType		( lookupTcTyVar, LookupTyVarResult(..),
@@ -61,7 +62,7 @@ import Type		( Kind, SimpleKind, KindVar,
 			  isSubKind, pprKind, splitKindFunTys, isSubKindCon,
                           isOpenTypeKind, isArgTypeKind )
 import TysPrim		( alphaTy, betaTy )
-import Inst		( newDicts, instToId, mkInstCoFn )
+import Inst		( newDictBndrsO, instCall, instToId )
 import TyCon		( TyCon, tyConArity, tyConTyVars, isSynTyCon )
 import TysWiredIn	( listTyCon )
 import Id		( Id, mkSysLocal )
@@ -698,13 +699,12 @@ tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty
 	; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty, 
 						ppr tyvars <+> ppr theta <+> ppr tau,
 						ppr tau'])
-	; co_fn <- tc_sub mb_fun tau' tau' exp_ib exp_sty expected_ty
+	; co_fn2 <- tc_sub mb_fun tau tau exp_ib exp_sty expected_ty
 
 		-- Deal with the dictionaries
-	; dicts <- newDicts InstSigOrigin (substTheta subst' theta)
-	; extendLIEs dicts
-	; let inst_fn = mkInstCoFn inst_tys dicts
-	; return (co_fn <.> inst_fn) }
+ 	; co_fn1 <- instCall InstSigOrigin (mkTyVarTys tyvars) theta
+ 	; co_fn2 <- tc_sub False tau tau exp_sty expected_ty
+ 	; return (co_fn2 <.> co_fn1) }
 
 -----------------------------------
 -- Function case (rule F1)
@@ -748,7 +748,7 @@ wrapFunResCoercion arg_tys co_fn_res
   | otherwise 	       
   = do	{ us <- newUniqueSupply
 	; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys
-	; return (CoLams arg_ids <.> co_fn_res <.> CoApps arg_ids) }
+	; return (mkCoLams arg_ids <.> co_fn_res <.> mkCoApps arg_ids) }
 \end{code}
 
 
@@ -802,7 +802,7 @@ tcGen expected_ty extra_tvs thing_inside	-- We expect expected_ty to be a forall
 	-- Conclusion: include the free vars of the expected_ty in the
 	-- list of "free vars" for the signature check.
 
-	; dicts <- newDicts (SigOrigin skol_info) theta
+	; dicts <- newDictBndrsO (SigOrigin skol_info) theta
 	; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
 
 	; checkSigTyVarsWrt free_tvs forall_tvs
@@ -811,7 +811,7 @@ tcGen expected_ty extra_tvs thing_inside	-- We expect expected_ty to be a forall
 	; let
 	    -- The CoLet binds any Insts which came out of the simplification.
 		dict_ids = map instToId dicts
-		co_fn = CoTyLams forall_tvs <.> CoLams dict_ids <.> CoLet inst_binds
+		co_fn = mkCoTyLams forall_tvs <.> mkCoLams dict_ids <.> CoLet inst_binds
 	; returnM (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
@@ -1331,6 +1331,7 @@ checkTauTvUpdate orig_tv orig_ty
 
     go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
     go_pred (IParam n ty)  = do { ty' <- go ty;        return (IParam n ty') }
+    go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
 
     go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
     go_tyvar tv (MetaTv box ref)
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 461439509b..fd8e8c5ac6 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -106,18 +106,15 @@ import TypeRep
 
 -- friends:
 import Var	( Var, TyVar, tyVarKind, tyVarName, 
-		  setTyVarName, setTyVarKind, mkTyVar, isTyVar )
-import Name	( Name(..) )
-import Unique	( Unique )
+		  setTyVarName, setTyVarKind )
 import VarEnv
 import VarSet
 
 import OccName	( tidyOccName )
-import Name	( NamedThing(..), mkInternalName, tidyNameOcc )
+import Name	( NamedThing(..), tidyNameOcc )
 import Class	( Class, classTyCon )
 import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey, 
-                  ubxTupleKindTyConKey, argTypeKindTyConKey, 
-                  eqCoercionKindTyConKey )
+                  ubxTupleKindTyConKey, argTypeKindTyConKey )
 import TyCon	( TyCon, isRecursiveTyCon, isPrimTyCon,
 		  isUnboxedTupleTyCon, isUnLiftedTyCon,
 		  isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
@@ -129,7 +126,6 @@ import TyCon	( TyCon, isRecursiveTyCon, isPrimTyCon,
 
 -- others
 import StaticFlags	( opt_DictsStrict )
-import SrcLoc		( noSrcLoc )
 import Util		( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
 import Outputable
 import UniqSet		( sizeUniqSet )		-- Should come via VarSet
@@ -681,8 +677,9 @@ tyVarsOfTypes :: [Type] -> TyVarSet
 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 
 tyVarsOfPred :: PredType -> TyVarSet
-tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
-tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
+tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
+tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
+tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 
 tyVarsOfTheta :: ThetaType -> TyVarSet
 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
@@ -756,6 +753,7 @@ tidyTypes env tys = map (tidyType env) tys
 tidyPred :: TidyEnv -> PredType -> PredType
 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
+tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
 \end{code}
 
 
@@ -874,8 +872,9 @@ seqNote :: TyNote -> ()
 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 
 seqPred :: PredType -> ()
-seqPred (ClassP c tys) = c  `seq` seqTypes tys
-seqPred (IParam n ty)  = n  `seq` seqType ty
+seqPred (ClassP c tys)   = c `seq` seqTypes tys
+seqPred (IParam n ty)    = n `seq` seqType ty
+seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
 \end{code}
 
 
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 9f5b405415..0f810da8e5 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -11,13 +11,10 @@ module Unify (
 import Var		( Var, TyVar, tyVarKind )
 import VarEnv
 import VarSet
-import Type		( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
-			  TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX,
-			  mkOpenTvSubst, tcView, isSubKind, eqKind, repSplitAppTy_maybe )
-import TypeRep          ( Type(..), PredType(..), funTyCon )
-import DataCon 		( DataCon, dataConResTys )
-import Util		( snocView )
-import ErrUtils		( Message )
+import Type		( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, 
+			  TvSubstEnv, emptyTvSubstEnv, TvSubst(..), tcEqTypeX,
+			  tcView, isSubKind, repSplitAppTy_maybe )
+import TypeRep          ( Type(..), PredType(..) )
 import Outputable
 import Maybes
 \end{code}