Three improvements to Template Haskell (fixes #3467)
[ghc-hetmet.git] / compiler / typecheck / Inst.lhs
index 31a9354..a45422a 100644 (file)
@@ -7,7 +7,7 @@ The @Inst@ type: dictionaries or method instances
 
 \begin{code}
 module Inst ( 
-       Inst, 
+       Inst,
 
        pprInstances, pprDictsTheta, pprDictsInFull,    -- User error messages
        showLIE, pprInst, pprInsts, pprInstInFull,      -- Debugging messages
@@ -15,15 +15,16 @@ module Inst (
        tidyInsts, tidyMoreInsts,
 
        newDictBndr, newDictBndrs, newDictBndrsO,
+       newDictOccs, newDictOcc,
        instCall, instStupidTheta,
        cloneDict, mkOverLit,
        newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy, 
        tcInstClassOp, 
-       tcSyntaxName, isHsVar,
+       tcSyntaxName, 
 
-       tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
-       ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
-       getDictClassTys, dictPred,
+       tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, tcTyVarsOfInst,
+       tcTyVarsOfInsts, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst,
+       fdPredsOfInsts, growInstsTyVars, getDictClassTys, dictPred,
 
        lookupSimpleInst, LookupInstResult(..), 
        tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
@@ -39,12 +40,12 @@ module Inst (
 
        InstOrigin(..), InstLoc, pprInstLoc,
 
-       mkWantedCo, mkGivenCo,
-       fromWantedCo, fromGivenCo,
-       eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
-       finalizeEqInst, writeWantedCoercion,
-       eqInstType, updateEqInstCoercion,
-       eqInstCoercion, eqInstTys
+       mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo, 
+        mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo,
+        mkTyConEqInstCo, mkFunEqInstCo,
+        wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst,
+        wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion,
+        eqInstTys
     ) where
 
 #include "HsVersions.h"
@@ -61,7 +62,8 @@ import InstEnv
 import FunDeps
 import TcMType
 import TcType
-import DsUtils
+import MkCore ( mkBigCoreTupTy )
+import TyCon
 import Type
 import TypeRep
 import Class
@@ -92,6 +94,7 @@ import Control.Monad
 \end{code}
 
 
+
 Selection
 ~~~~~~~~~
 \begin{code}
@@ -116,8 +119,11 @@ instToVar (Dict {tci_name = nm, tci_pred = pred})
 instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
                       tci_wanted = wanteds})
   = mkLocalId nm (mkImplicTy tvs givens wanteds)
-instToVar i@(EqInst {})
-  = eitherEqInst i id (\(TyVarTy covar) -> covar)
+instToVar inst@(EqInst {})
+  = eitherEqInst inst id assertCoVar
+  where
+    assertCoVar (TyVarTy cotv) = cotv
+    assertCoVar coty           = pprPanic "Inst.instToVar" (ppr coty)
 
 instType :: Inst -> Type
 instType (LitInst {tci_ty = ty})  = ty
@@ -148,6 +154,7 @@ getDictClassTys :: Inst -> (Class, [Type])
 getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred
 getDictClassTys inst                    = pprPanic "getDictClassTys" (ppr inst)
 
+--------------------------------
 -- fdPredsOfInst is used to get predicates that contain functional 
 -- dependencies *or* might do so.  The "might do" part is because
 -- a constraint (C a b) might have a superclass with FDs
@@ -157,14 +164,16 @@ getDictClassTys inst                       = pprPanic "getDictClassTys" (ppr inst)
 fdPredsOfInst :: Inst -> [TcPredType]
 fdPredsOfInst (Dict {tci_pred = pred})              = [pred]
 fdPredsOfInst (Method {tci_theta = theta})   = theta
-fdPredsOfInst (ImplicInst {tci_given = gs, 
-                          tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws)
+fdPredsOfInst (ImplicInst {tci_wanted = ws}) = fdPredsOfInsts ws
+   -- The ImplicInst case doesn't look right;
+   -- what if ws mentions skolem variables?
 fdPredsOfInst (LitInst {})                  = []
 fdPredsOfInst (EqInst {})                   = []
 
 fdPredsOfInsts :: [Inst] -> [PredType]
 fdPredsOfInsts insts = concatMap fdPredsOfInst insts
 
+---------------------------------
 isInheritableInst :: Inst -> Bool
 isInheritableInst (Dict {tci_pred = pred})     = isInheritablePred pred
 isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta
@@ -184,22 +193,53 @@ ipNamesOfInst (Method {tci_theta = theta})   = [ipNameName n | IParam n _ <- the
 ipNamesOfInst _                              = []
 
 ---------------------------------
-tyVarsOfInst :: Inst -> TcTyVarSet
+
+-- |All free type variables (not including the coercion variables of
+-- equalities)
+--
+tyVarsOfInst :: Inst -> TyVarSet
 tyVarsOfInst (LitInst {tci_ty = ty})  = tyVarsOfType  ty
 tyVarsOfInst (Dict {tci_pred = pred}) = tyVarsOfPred pred
-tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id
-                                -- The id might have free type variables; in the case of
-                                -- locally-overloaded class methods, for example
-tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds})
+tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) 
+  = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id
+    -- The id might have free type variables; in the case of
+    -- locally-overloaded class methods, for example
+tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, 
+                          tci_wanted = wanteds})
   = (tyVarsOfInsts givens `unionVarSet` tyVarsOfInsts wanteds) 
     `minusVarSet` mkVarSet tvs
     `unionVarSet` unionVarSets (map varTypeTyVars tvs)
                -- Remember the free tyvars of a coercion
-tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) 
+  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+
+-- |All free meta type variables *including* the coercion variables of
+-- equalities
+--
+tcTyVarsOfInst :: Inst -> TyVarSet
+tcTyVarsOfInst (LitInst {tci_ty = ty})  = tcTyVarsOfType  ty
+tcTyVarsOfInst (Dict {tci_pred = pred}) = tcTyVarsOfPred pred
+tcTyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) 
+  = tcTyVarsOfTypes tys `unionVarSet` varTypeTcTyVars id
+    -- The id might have free type variables; in the case of
+    -- locally-overloaded class methods, for example
+tcTyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, 
+                            tci_wanted = wanteds})
+  = (tcTyVarsOfInsts givens `unionVarSet` tcTyVarsOfInsts wanteds) 
+    `minusVarSet` mkVarSet tvs
+    `unionVarSet` unionVarSets (map varTypeTcTyVars tvs)
+               -- Remember the free tyvars of a coercion
+tcTyVarsOfInst (EqInst {tci_co = co, tci_left = ty1, tci_right = ty2}) 
+  = either unitVarSet tcTyVarsOfType co `unionVarSet`   -- include covars
+    tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
 
-tyVarsOfInsts :: [Inst] -> VarSet
+tyVarsOfInsts :: [Inst] -> TyVarSet
 tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
-tyVarsOfLIE :: Bag Inst -> VarSet
+
+tcTyVarsOfInsts :: [Inst] -> TcTyVarSet
+tcTyVarsOfInsts insts = foldr (unionVarSet . tcTyVarsOfInst) emptyVarSet insts
+
+tyVarsOfLIE :: Bag Inst -> TyVarSet
 tyVarsOfLIE   lie   = tyVarsOfInsts (lieToList lie)
 
 
@@ -212,8 +252,45 @@ addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds
 addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs
 \end{code}
 
-Predicates
-~~~~~~~~~~
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growInstsTyVars insts tvs) is the result of extending the set 
+    of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then grow precs tvs = {a,b,c}
+
+All the type variables from an implicit parameter are added, whether or
+not they are mentioned in tvs; see Note [Implicit parameters and ambiguity] 
+in TcSimplify.
+
+See also Note [Ambiguity] in TcSimplify
+
+\begin{code}
+growInstsTyVars :: [Inst] -> TyVarSet -> TyVarSet
+growInstsTyVars insts tvs
+  | null insts = tvs
+  | otherwise  = fixVarSet mk_next tvs
+  where
+    mk_next tvs = foldr grow_inst_tvs tvs insts
+
+grow_inst_tvs :: Inst -> TyVarSet -> TyVarSet
+grow_inst_tvs (Dict {tci_pred = pred})     tvs = growPredTyVars pred tvs
+grow_inst_tvs (Method {tci_theta = theta}) tvs = foldr growPredTyVars tvs theta
+grow_inst_tvs (ImplicInst {tci_tyvars = tvs1, tci_wanted = ws}) tvs
+  = tvs `unionVarSet` (foldr grow_inst_tvs (tvs `delVarSetList` tvs1) ws
+                         `delVarSetList` tvs1)
+grow_inst_tvs inst tvs   -- EqInst, LitInst
+  = growTyVars (tyVarsOfInst inst) tvs
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+               Predicates
+%*                                                                     *
+%************************************************************************
+
 \begin{code}
 
 isAbstractableInst :: Inst -> Bool
@@ -278,16 +355,41 @@ newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst]
 newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
 
 newDictBndr :: InstLoc -> TcPredType -> TcM Inst
+-- Makes a "given"
 newDictBndr inst_loc pred@(EqPred ty1 ty2)
   = do { uniq <- newUnique 
        ; let name = mkPredName uniq inst_loc pred 
+             co   = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))
        ; return (EqInst {tci_name  = name, 
                          tci_loc   = inst_loc, 
                          tci_left  = ty1, 
                          tci_right = ty2, 
-                         tci_co    = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))})
-       }
-newDictBndr inst_loc pred
+                         tci_co    = co }) }
+
+newDictBndr inst_loc pred = newDict inst_loc pred
+
+-------------------
+newDictOccs :: InstLoc -> TcThetaType -> TcM [Inst]
+newDictOccs inst_loc theta = mapM (newDictOcc inst_loc) theta
+
+newDictOcc :: InstLoc -> TcPredType -> TcM Inst
+-- Makes a "wanted"
+newDictOcc inst_loc pred@(EqPred ty1 ty2)
+  = do { uniq <- newUnique 
+       ; cotv <- newMetaCoVar ty1 ty2
+       ; let name = mkPredName uniq inst_loc pred 
+       ; return (EqInst {tci_name  = name, 
+                         tci_loc   = inst_loc, 
+                         tci_left  = ty1, 
+                         tci_right = ty2, 
+                         tci_co    = Left cotv }) }
+
+newDictOcc inst_loc pred = newDict inst_loc pred
+
+----------------
+newDict :: InstLoc -> TcPredType -> TcM Inst
+-- Always makes a Dict, not an EqInst
+newDict inst_loc pred
   = do         { uniq <- newUnique 
        ; let name = mkPredName uniq inst_loc pred 
        ; return (Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}) }
@@ -334,15 +436,12 @@ instCallDicts _ [] = return idHsWrapper
 instCallDicts loc (EqPred ty1 ty2 : preds)
   = do  { traceTc (text "instCallDicts" <+> ppr (EqPred ty1 ty2))
        ; coi <- boxyUnify ty1 ty2
---     ; coi <- unifyType ty1 ty2
        ; let co = fromCoI coi ty1
        ; co_fn <- instCallDicts loc preds
        ; return (co_fn <.> WpTyApp co) }
 
 instCallDicts loc (pred : preds)
-  = do { uniq <- newUnique
-       ; let name = mkPredName uniq loc pred 
-             dict = Dict {tci_name = name, tci_pred = pred, tci_loc = loc}
+  = do { dict <- newDict loc pred
        ; extendLIE dict
        ; co_fn <- instCallDicts loc preds
        ; return (co_fn <.> WpApp (instToId dict)) }
@@ -350,8 +449,8 @@ instCallDicts loc (pred : preds)
 -------------
 cloneDict :: Inst -> TcM Inst
 cloneDict dict@(Dict nm _ _) = do { uniq <- newUnique
-                                    ; return (dict {tci_name = setNameUnique nm uniq}) }
-cloneDict eq@(EqInst {})       = return eq
+                                 ; return (dict {tci_name = setNameUnique nm uniq}) }
+cloneDict eq@(EqInst {})     = return eq
 cloneDict other = pprPanic "cloneDict" (ppr other)
 
 -- For vanilla implicit parameters, there is only one in scope
@@ -360,15 +459,10 @@ cloneDict other = pprPanic "cloneDict" (ppr other)
 -- scope, so we make up a new namea.
 newIPDict :: InstOrigin -> IPName Name -> Type 
          -> TcM (IPName Id, Inst)
-newIPDict orig ip_name ty = do
-    inst_loc <- getInstLoc orig
-    uniq <- newUnique
-    let
-       pred = IParam ip_name ty
-        name = mkPredName uniq inst_loc pred 
-       dict = Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}
-    
-    return (mapIPName (\_ -> instToId dict) ip_name, dict)
+newIPDict orig ip_name ty
+  = do { inst_loc <- getInstLoc orig
+       ; dict <- newDict inst_loc (IParam ip_name ty)
+       ; return (mapIPName (\_ -> instToId dict) ip_name, dict) }
 \end{code}
 
 
@@ -385,7 +479,7 @@ mkPredName uniq loc pred_ty
                -- we use the outermost tycon of the lhs, if there is one, to
                -- improve readability of Core code
                baseOcc = case splitTyConApp_maybe ty of
-                           Nothing      -> mkOccName tcName "$"
+                           Nothing      -> mkTcOcc "$"
                             Just (tc, _) -> getOccName tc
 \end{code}
 
@@ -476,10 +570,6 @@ mkOverLit (HsFractional r)
        ; return (HsRat r rat_ty) }
 
 mkOverLit (HsIsString s) = return (HsString s)
-
-isHsVar :: HsExpr Name -> Name -> Bool
-isHsVar (HsVar f) g = f == g
-isHsVar _        _ = False
 \end{code}
 
 
@@ -493,7 +583,7 @@ Zonking makes sure that the instance types are fully zonked.
 
 \begin{code}
 zonkInst :: Inst -> TcM Inst
-zonkInst dict@(Dict { tci_pred = pred}) = do
+zonkInst dict@(Dict {tci_pred = pred}) = do
     new_pred <- zonkTcPredType pred
     return (dict {tci_pred = new_pred})
 
@@ -524,7 +614,7 @@ zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2})
                  (\co    -> liftM mkGivenCo $ zonkTcType co)
        ; ty1' <- zonkTcType ty1
        ; ty2' <- zonkTcType ty2
-       ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' })
+       ; return (eqinst {tci_co = co', tci_left = ty1', tci_right = ty2' })
        }
 
 zonkInsts :: [Inst] -> TcRn [Inst]
@@ -777,7 +867,7 @@ lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
 
     { use_stage <- getStage
     ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
-                     (topIdLvl dfun_id) use_stage
+                     (topIdLvl dfun_id) (thLevel use_stage)
 
        -- It's possible that not all the tyvars are in
        -- the substitution, tenv. For example:
@@ -838,7 +928,8 @@ record_dfun_usage :: Id -> TcRn ()
 record_dfun_usage dfun_id 
   = do { hsc_env <- getTopEnv
        ; let  dfun_name = idName dfun_id
-              dfun_mod  = nameModule dfun_name
+              dfun_mod  = ASSERT( isExternalName dfun_name ) 
+                          nameModule dfun_name
        ; if isInternalName dfun_name ||    -- Internal name => defined in this module
             modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
          then return () -- internal, or in another package
@@ -935,20 +1026,126 @@ syntaxNameCtxt name orig ty tidy_env = do
 %*                                                                     *
 %************************************************************************
 
+Operations on EqInstCo.
+
 \begin{code}
-mkGivenCo   :: Coercion -> Either TcTyVar Coercion
+mkGivenCo   :: Coercion -> EqInstCo
 mkGivenCo   =  Right
 
-mkWantedCo  :: TcTyVar  -> Either TcTyVar Coercion
+mkWantedCo  :: TcTyVar  -> EqInstCo
 mkWantedCo  =  Left
 
-fromGivenCo :: Either TcTyVar Coercion -> Coercion
-fromGivenCo (Right co)          = co
-fromGivenCo _           = panic "fromGivenCo: not a wanted coercion"
+isWantedCo :: EqInstCo -> Bool
+isWantedCo (Left _) = True
+isWantedCo _        = False
+
+eqInstCoType :: EqInstCo -> TcType
+eqInstCoType (Left cotv) = mkTyVarTy cotv
+eqInstCoType (Right co)  = co
+\end{code}
+
+Coercion transformations on EqInstCo.  These transformations work differently
+depending on whether a EqInstCo is for a wanted or local equality:
+
+  Local : apply the inverse of the specified coercion
+  Wanted: obtain a fresh coercion hole (meta tyvar) and update the old hole
+          to be the specified coercion applied to the new coercion hole
+
+\begin{code}
+-- Coercion transformation: co = id
+--
+mkIdEqInstCo :: EqInstCo -> Type -> TcM ()
+mkIdEqInstCo (Left cotv) t
+  = bindMetaTyVar cotv t
+mkIdEqInstCo (Right _) _
+  = return ()
+
+-- Coercion transformation: co = sym co'
+--
+mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo
+mkSymEqInstCo (Left cotv) (ty1, ty2)
+  = do { cotv' <- newMetaCoVar ty1 ty2
+       ; bindMetaTyVar cotv (mkSymCoercion (TyVarTy cotv'))
+       ; return $ Left cotv'
+       }
+mkSymEqInstCo (Right co) _ 
+  = return $ Right (mkSymCoercion co)
+
+-- Coercion transformation: co = co' |> given_co
+--
+mkLeftTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
+mkLeftTransEqInstCo (Left cotv) given_co (ty1, ty2)
+  = do { cotv' <- newMetaCoVar ty1 ty2
+       ; bindMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co)
+       ; return $ Left cotv'
+       }
+mkLeftTransEqInstCo (Right co) given_co _ 
+  = return $ Right (co `mkTransCoercion` mkSymCoercion given_co)
+
+-- Coercion transformation: co = given_co |> co'
+--
+mkRightTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
+mkRightTransEqInstCo (Left cotv) given_co (ty1, ty2)
+  = do { cotv' <- newMetaCoVar ty1 ty2
+       ; bindMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv')
+       ; return $ Left cotv'
+       }
+mkRightTransEqInstCo (Right co) given_co _ 
+  = return $ Right (mkSymCoercion given_co `mkTransCoercion` co)
+
+-- Coercion transformation: co = col cor
+--
+mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
+              -> TcM (EqInstCo, EqInstCo)
+mkAppEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
+  = do { cotv_l <- newMetaCoVar ty1_l ty2_l
+       ; cotv_r <- newMetaCoVar ty1_r ty2_r
+       ; bindMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
+       ; return (Left cotv_l, Left cotv_r)
+       }
+mkAppEqInstCo (Right co) _ _
+  = return (Right $ mkLeftCoercion co, Right $ mkRightCoercion co)
+
+-- Coercion transformation: co = con col -> cor
+--
+mkTyConEqInstCo :: EqInstCo -> TyCon -> [(Type, Type)] -> TcM ([EqInstCo])
+mkTyConEqInstCo (Left cotv) con ty12s
+  = do { cotvs <- mapM (uncurry newMetaCoVar) ty12s
+       ; bindMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs))
+       ; return (map Left cotvs)
+       }
+mkTyConEqInstCo (Right co) _ args
+  = return $ map (\mkCoes -> Right $ foldl (.) id mkCoes co) mkCoes
+    -- make cascades of the form 
+    --   mkRightCoercion (mkLeftCoercion .. (mkLeftCoercion co)..)
+  where
+    n      = length args
+    mkCoes = [mkRightCoercion : replicate i mkLeftCoercion | i <- [n-1, n-2..0]]
+
+-- Coercion transformation: co = col -> cor
+--
+mkFunEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
+              -> TcM (EqInstCo, EqInstCo)
+mkFunEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
+  = do { cotv_l <- newMetaCoVar ty1_l ty2_l
+       ; cotv_r <- newMetaCoVar ty1_r ty2_r
+       ; bindMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
+       ; return (Left cotv_l, Left cotv_r)
+       }
+mkFunEqInstCo (Right co) _ _
+  = return (Right $ mkRightCoercion (mkLeftCoercion co), 
+            Right $ mkRightCoercion co)
+\end{code}
+
+Operations on entire EqInst.
 
-fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
-fromWantedCo _ (Left covar) = covar
-fromWantedCo msg _         = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+\begin{code}
+-- |A wanted equality is unsolved as long as its cotv is unfilled.
+--
+wantedEqInstIsUnsolved :: Inst -> TcM Bool
+wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv})
+  = liftM not $ isFilledMetaTyVar cotv
+wantedEqInstIsUnsolved _ = return True
 
 eitherEqInst :: Inst               -- given or wanted EqInst
             -> (TcTyVar  -> a)     --  result if wanted
@@ -960,20 +1157,23 @@ eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
                Right co    -> withGiven  co
 eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
 
-mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst]
-mkEqInsts preds cos = zipWithM mkEqInst preds cos
-
-mkEqInst :: PredType -> Either TcTyVar Coercion -> TcM Inst
+mkEqInst :: PredType -> EqInstCo -> TcM Inst
 mkEqInst (EqPred ty1 ty2) co
        = do { uniq <- newUnique
             ; src_span <- getSrcSpanM
             ; err_ctxt <- getErrCtxt
             ; let loc  = InstLoc EqOrigin src_span err_ctxt
                   name = mkName uniq src_span
-                  inst = EqInst {tci_left = ty1, tci_right = ty2, tci_co = co, tci_loc = loc, tci_name = name} 
+                  inst = EqInst { tci_left = ty1
+                                 , tci_right = ty2
+                                 , tci_co = co
+                                 , tci_loc = loc
+                                 , tci_name = name
+                                 } 
             ; return inst
             }
-       where mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
+       where 
+          mkName uniq src_span = mkInternalName uniq (mkVarOcc "co_ei") src_span
 mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred)
 
 mkWantedEqInst :: PredType -> TcM Inst
@@ -983,40 +1183,42 @@ mkWantedEqInst pred@(EqPred ty1 ty2)
        }
 mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred)
 
--- type inference:
---     We want to promote the wanted EqInst to a given EqInst
---     in the signature context.
---     This means we have to give the coercion a name
---     and fill it in as its own name.
-finalizeEqInst 
-       :: Inst                 -- wanted
-       -> TcM Inst             -- given
-finalizeEqInst wanted@(EqInst {tci_left = ty1, tci_right = ty2, tci_name = name})
-       = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
-                    ; writeWantedCoercion wanted (TyVarTy var)
-            ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
-            ; return given
-             }
-finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i)
+-- Turn a wanted equality into a local that propagates the uninstantiated
+-- coercion variable as witness.  We need this to propagate wanted irreds into
+-- attempts to solve implication constraints.
+--
+wantedToLocalEqInst :: Inst -> Inst
+wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv})
+  = eq {tci_co = Right (mkTyVarTy cotv)}
+wantedToLocalEqInst eq = eq
+
+-- Turn a wanted into a local EqInst (needed during type inference for
+-- signatures) 
+--
+-- * Give it a name and change the coercion around.
+--
+finalizeEqInst :: Inst                 -- wanted
+              -> TcM Inst              -- given
+finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, 
+                              tci_name = name, tci_co = Left cotv})
+  = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
+
+         -- fill the coercion hole
+       ; writeMetaTyVar cotv (TyVarTy var)
+
+         -- set the new coercion
+       ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
+       ; return given
+       }
 
-writeWantedCoercion 
-       :: Inst         -- wanted EqInst
-       -> Coercion     -- coercion to fill the hole with
-       -> TcM ()       
-writeWantedCoercion wanted co
-       = do { let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted
-            ; writeMetaTyVar cotv co
-            }
+finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i)
 
 eqInstType :: Inst -> TcType
 eqInstType inst = eitherEqInst inst mkTyVarTy id
 
-eqInstCoercion :: Inst -> Either TcTyVar Coercion
+eqInstCoercion :: Inst -> EqInstCo
 eqInstCoercion = tci_co
 
 eqInstTys :: Inst -> (TcType, TcType)
 eqInstTys inst = (tci_left inst, tci_right inst)
-
-updateEqInstCoercion :: (Either TcTyVar Coercion -> Either TcTyVar Coercion) -> Inst -> Inst
-updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst}
 \end{code}