Don't import FastString in HsVersions.h
[ghc-hetmet.git] / compiler / typecheck / Inst.lhs
index 04dd4a2..91e409f 100644 (file)
@@ -6,6 +6,13 @@
 The @Inst@ type: dictionaries or method instances
 
 \begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
 module Inst ( 
        Inst, 
 
@@ -29,22 +36,31 @@ module Inst (
        lookupSimpleInst, LookupInstResult(..), 
        tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
 
+       isAbstractableInst, isEqInst,
        isDict, isClassDict, isMethod, isImplicInst,
        isIPDict, isInheritableInst, isMethodOrLit,
        isTyVarDict, isMethodFor, 
 
        zonkInst, zonkInsts,
-       instToId, instToVar, instName,
+       instToId, instToVar, instType, instName, instToDictBind,
+       addInstToDictBind,
+
+       InstOrigin(..), InstLoc, pprInstLoc,
 
-       InstOrigin(..), InstLoc, pprInstLoc
+       mkWantedCo, mkGivenCo,
+       fromWantedCo, fromGivenCo,
+       eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
+       finalizeEqInst, writeWantedCoercion,
+       eqInstType, updateEqInstCoercion,
+       eqInstCoercion, eqInstTys
     ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-}  TcExpr( tcPolyExpr )
-import {-# SOURCE #-}  TcUnify( unifyType )
+import {-# SOURCE #-}  TcUnify( boxyUnify, unifyType )
 
-import FastString(FastString)
+import FastString
 import HsSyn
 import TcHsSyn
 import TcRnMonad
@@ -54,6 +70,8 @@ import FunDeps
 import TcMType
 import TcType
 import Type
+import TypeRep
+import Class
 import Unify
 import Module
 import Coercion
@@ -73,11 +91,16 @@ import PrelNames
 import BasicTypes
 import SrcLoc
 import DynFlags
+import Bag
 import Maybes
 import Util
+import Unique
 import Outputable
-
 import Data.List
+import TypeRep
+import Class
+
+import Control.Monad
 \end{code}
 
 
@@ -85,10 +108,12 @@ Selection
 ~~~~~~~~~
 \begin{code}
 instName :: Inst -> Name
+instName (EqInst {tci_name = name}) = name
 instName inst = Var.varName (instToVar inst)
 
 instToId :: Inst -> TcId
-instToId inst = ASSERT2( isId id, ppr inst ) id 
+instToId inst = WARN( not (isId id), ppr inst ) 
+             id 
              where
                id = instToVar inst
 
@@ -103,25 +128,33 @@ 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)
 
 instType :: Inst -> Type
-instType (LitInst {tci_ty = ty}) = ty
-instType (Method {tci_id = id}) = idType id
+instType (LitInst {tci_ty = ty})  = ty
+instType (Method {tci_id = id})   = idType id
 instType (Dict {tci_pred = pred}) = mkPredTy pred
 instType imp@(ImplicInst {})      = mkImplicTy (tci_tyvars imp) (tci_given imp)        
                                               (tci_wanted imp)
+-- instType i@(EqInst {tci_co = co}) = eitherEqInst i TyVarTy id
+instType (EqInst {tci_left = ty1, tci_right = ty2}) = mkPredTy (EqPred ty1 ty2)
 
 mkImplicTy tvs givens wanteds  -- The type of an implication constraint
-  = ASSERT( all isDict givens )
+  = ASSERT( all isAbstractableInst givens )
     -- pprTrace "mkImplicTy" (ppr givens) $
-    mkForAllTys tvs $ 
-    mkPhiTy (map dictPred givens) $
-    if isSingleton wanteds then
-       instType (head wanteds) 
-    else
-       mkTupleTy Boxed (length wanteds) (map instType wanteds)
+    -- See [Equational Constraints in Implication Constraints]
+    let dict_wanteds = filter (not . isEqInst) wanteds
+    in 
+      mkForAllTys tvs $ 
+      mkPhiTy (map dictPred givens) $
+      if isSingleton dict_wanteds then
+       instType (head dict_wanteds) 
+      else
+       mkTupleTy Boxed (length dict_wanteds) (map instType dict_wanteds)
 
 dictPred (Dict {tci_pred = pred}) = pred
+dictPred (EqInst {tci_left=ty1,tci_right=ty2}) = EqPred ty1 ty2
 dictPred inst                    = pprPanic "dictPred" (ppr inst)
 
 getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred
@@ -138,6 +171,7 @@ fdPredsOfInst (Method {tci_theta = theta})   = theta
 fdPredsOfInst (ImplicInst {tci_given = gs, 
                           tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws)
 fdPredsOfInst (LitInst {})                  = []
+fdPredsOfInst (EqInst {})                   = []
 
 fdPredsOfInsts :: [Inst] -> [PredType]
 fdPredsOfInsts insts = concatMap fdPredsOfInst insts
@@ -171,14 +205,32 @@ tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wan
     `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
 
 tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
 tyVarsOfLIE   lie   = tyVarsOfInsts (lieToList lie)
+
+
+--------------------------
+instToDictBind :: Inst -> LHsExpr TcId -> TcDictBinds
+instToDictBind inst rhs 
+  = unitBag (L (instSpan inst) (VarBind (instToId inst) rhs))
+
+addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds
+addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs
 \end{code}
 
 Predicates
 ~~~~~~~~~~
 \begin{code}
+
+isAbstractableInst :: Inst -> Bool
+isAbstractableInst inst = isDict inst || isEqInst inst
+
+isEqInst :: Inst -> Bool
+isEqInst (EqInst {}) = True
+isEqInst other       = False
+
 isDict :: Inst -> Bool
 isDict (Dict {}) = True
 isDict other    = False
@@ -233,6 +285,15 @@ newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst]
 newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
 
 newDictBndr :: InstLoc -> TcPredType -> TcM Inst
+newDictBndr inst_loc pred@(EqPred ty1 ty2)
+  = do { uniq <- newUnique 
+       ; let name = mkPredName uniq inst_loc 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
   = do         { uniq <- newUnique 
        ; let name = mkPredName uniq inst_loc pred 
@@ -244,12 +305,11 @@ instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
 --     (instCall o tys theta)
 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
 -- (b) Throws these dictionaries into the LIE
--- (c) Eeturns an HsWrapper ([.] tys dicts)
+-- (c) Returns an HsWrapper ([.] tys dicts)
 
 instCall orig tys theta 
   = do { loc <- getInstLoc orig
-       ; (dicts, dict_app) <- instCallDicts loc theta
-       ; extendLIEs dicts
+       ; dict_app <- instCallDicts loc theta
        ; return (dict_app <.> mkWpTyApps tys) }
 
 ----------------
@@ -258,35 +318,47 @@ instStupidTheta :: InstOrigin -> TcThetaType -> TcM ()
 -- Used exclusively for the 'stupid theta' of a data constructor
 instStupidTheta orig theta
   = do { loc <- getInstLoc orig
-       ; (dicts, _) <- instCallDicts loc theta
-       ; extendLIEs dicts }
+       ; _co <- instCallDicts loc theta        -- Discard the coercion
+       ; return () }
 
 ----------------
-instCallDicts :: InstLoc -> TcThetaType -> TcM ([Inst], HsWrapper)
+instCallDicts :: InstLoc -> TcThetaType -> TcM HsWrapper
+-- Instantiates the TcTheta, puts all constraints thereby generated
+-- into the LIE, and returns a HsWrapper to enclose the call site.
 -- This is the key place where equality predicates 
 -- are unleashed into the world
-instCallDicts loc [] = return ([], idHsWrapper)
+instCallDicts loc [] = return idHsWrapper
+
+-- 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 :: Type -> Type -> TcM ([Inst], Coercion)
+--     ; (dicts, co_fn) <- instCallDicts loc preds
+--     ; return (dicts, co_fn <.> WpTyApp ty1) }
+--     -- We use type application to apply the function to the 
+--     -- coercion; here ty1 *is* the appropriate identity coercion
 
 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 :: Type -> Type -> TcM ([Inst], Coercion)
-       ; (dicts, co_fn) <- instCallDicts loc preds
-       ; return (dicts, co_fn <.> WpTyApp ty1) }
-       -- We use type application to apply the function to the 
-       -- coercion; here ty1 *is* the appropriate identity coercion
+  = 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}
-       ; (dicts, co_fn) <- instCallDicts loc preds
-       ; return (dict:dicts, co_fn <.> WpApp (instToId dict)) }
+       ; extendLIE dict
+       ; co_fn <- instCallDicts loc preds
+       ; return (co_fn <.> WpApp (instToId dict)) }
 
 -------------
 cloneDict :: Inst -> TcM Inst
 cloneDict dict@(Dict nm ty loc) = do { uniq <- newUnique
                                     ; 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
@@ -295,15 +367,15 @@ 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
-  = getInstLoc orig                    `thenM` \ inst_loc ->
-    newUnique                          `thenM` \ uniq ->
+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}
-    in
-    returnM (mapIPName (\n -> instToId dict) ip_name, dict)
+    
+    return (mapIPName (\n -> instToId dict) ip_name, dict)
 \end{code}
 
 
@@ -333,22 +405,22 @@ mkPredName uniq loc pred_ty
 
 \begin{code}
 newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
-newMethodFromName origin ty name
-  = tcLookupId name            `thenM` \ id ->
+newMethodFromName origin ty name = do
+    id <- tcLookupId name
        -- Use tcLookupId not tcLookupGlobalId; the method is almost
        -- always a class op, but with -fno-implicit-prelude GHC is
        -- meant to find whatever thing is in scope, and that may
        -- be an ordinary function. 
-    getInstLoc origin          `thenM` \ loc ->
-    tcInstClassOp loc id [ty]  `thenM` \ inst ->
-    extendLIE inst             `thenM_`
-    returnM (instToId inst)
+    loc <- getInstLoc origin
+    inst <- tcInstClassOp loc id [ty]
+    extendLIE inst
+    return (instToId inst)
 
-newMethodWithGivenTy orig id tys
-  = getInstLoc orig            `thenM` \ loc ->
-    newMethod loc id tys       `thenM` \ inst ->
-    extendLIE inst             `thenM_`
-    returnM (instToId inst)
+newMethodWithGivenTy orig id tys = do
+    loc <- getInstLoc orig
+    inst <- newMethod loc id tys
+    extendLIE inst
+    return (instToId inst)
 
 --------------------------------------------
 -- tcInstClassOp, and newMethod do *not* drop the 
@@ -362,11 +434,10 @@ newMethodWithGivenTy orig id tys
 --     Hence the call to checkKind
 -- A worry: is this needed anywhere else?
 tcInstClassOp :: InstLoc -> Id -> [TcType] -> TcM Inst
-tcInstClassOp inst_loc sel_id tys
-  = let
+tcInstClassOp inst_loc sel_id tys = do
+    let
        (tyvars, _rho) = tcSplitForAllTys (idType sel_id)
-    in
-    zipWithM_ checkKind tyvars tys     `thenM_` 
+    zipWithM_ checkKind tyvars tys
     newMethod inst_loc sel_id tys
 
 checkKind :: TyVar -> TcType -> TcM ()
@@ -387,34 +458,35 @@ checkKind tv ty
 
 
 ---------------------------
-newMethod inst_loc id tys
-  = newUnique          `thenM` \ new_uniq ->
+newMethod inst_loc id tys = do
+    new_uniq <- newUnique
     let
        (theta,tau) = tcSplitPhiTy (applyTys (idType id) tys)
        meth_id     = mkUserLocal (mkMethodOcc (getOccName id)) new_uniq tau loc
        inst        = Method {tci_id = meth_id, tci_oid = id, tci_tys = tys,
                              tci_theta = theta, tci_loc = inst_loc}
        loc         = instLocSpan inst_loc
-    in
-    returnM inst
+    
+    return inst
 \end{code}
 
 \begin{code}
 shortCutIntLit :: Integer -> TcType -> Maybe (HsExpr TcId)
 shortCutIntLit i ty
-  | isIntTy ty && inIntRange i                 -- Short cut for Int
-  = Just (HsLit (HsInt i))
-  | isIntegerTy ty                     -- Short cut for Integer
-  = Just (HsLit (HsInteger i ty))
-  | otherwise = Nothing
+  | isIntTy ty && inIntRange i = Just (HsLit (HsInt i))
+  | isIntegerTy ty            = Just (HsLit (HsInteger i ty))
+  | otherwise                 = shortCutFracLit (fromInteger i) ty
+       -- The 'otherwise' case is important
+       -- Consider (3 :: Float).  Syntactically it looks like an IntLit,
+       -- so we'll call shortCutIntLit, but of course it's a float
+       -- This can make a big difference for programs with a lot of
+       -- literals, compiled without -O
 
 shortCutFracLit :: Rational -> TcType -> Maybe (HsExpr TcId)
 shortCutFracLit f ty
-  | isFloatTy ty 
-  = Just (mk_lit floatDataCon (HsFloatPrim f))
-  | isDoubleTy ty
-  = Just (mk_lit doubleDataCon (HsDoublePrim f))
-  | otherwise = Nothing
+  | isFloatTy ty  = Just (mk_lit floatDataCon  (HsFloatPrim f))
+  | isDoubleTy ty = Just (mk_lit doubleDataCon (HsDoublePrim f))
+  | otherwise     = Nothing
   where
     mk_lit con lit = HsApp (nlHsVar (dataConWrapId con)) (nlHsLit lit)
 
@@ -425,22 +497,22 @@ shortCutStringLit s ty
   | otherwise = Nothing
 
 mkIntegerLit :: Integer -> TcM (LHsExpr TcId)
-mkIntegerLit i
-  = tcMetaTy integerTyConName  `thenM` \ integer_ty ->
-    getSrcSpanM                        `thenM` \ span -> 
-    returnM (L span $ HsLit (HsInteger i integer_ty))
+mkIntegerLit i = do
+    integer_ty <- tcMetaTy integerTyConName
+    span <- getSrcSpanM
+    return (L span $ HsLit (HsInteger i integer_ty))
 
 mkRatLit :: Rational -> TcM (LHsExpr TcId)
-mkRatLit r
-  = tcMetaTy rationalTyConName         `thenM` \ rat_ty ->
-    getSrcSpanM                        `thenM` \ span -> 
-    returnM (L span $ HsLit (HsRat r rat_ty))
+mkRatLit r = do
+    rat_ty <- tcMetaTy rationalTyConName
+    span <- getSrcSpanM
+    return (L span $ HsLit (HsRat r rat_ty))
 
 mkStrLit :: FastString -> TcM (LHsExpr TcId)
-mkStrLit s
-  = --tcMetaTy stringTyConName         `thenM` \ string_ty ->
-    getSrcSpanM                        `thenM` \ span -> 
-    returnM (L span $ HsLit (HsString s))
+mkStrLit s = do
+    --string_ty <- tcMetaTy stringTyConName
+    span <- getSrcSpanM
+    return (L span $ HsLit (HsString s))
 
 isHsVar :: HsExpr Name -> Name -> Bool
 isHsVar (HsVar f) g = f==g
@@ -458,24 +530,24 @@ Zonking makes sure that the instance types are fully zonked.
 
 \begin{code}
 zonkInst :: Inst -> TcM Inst
-zonkInst dict@(Dict { tci_pred = pred})
-  = zonkTcPredType pred                        `thenM` \ new_pred ->
-    returnM (dict {tci_pred = new_pred})
+zonkInst dict@(Dict { tci_pred = pred}) = do
+    new_pred <- zonkTcPredType pred
+    return (dict {tci_pred = new_pred})
 
-zonkInst meth@(Method {tci_oid = id, tci_tys = tys, tci_theta = theta}) 
-  = zonkId id                  `thenM` \ new_id ->
+zonkInst meth@(Method {tci_oid = id, tci_tys = tys, tci_theta = theta}) = do
+    new_id <- zonkId id
        -- Essential to zonk the id in case it's a local variable
        -- Can't use zonkIdOcc because the id might itself be
        -- an InstId, in which case it won't be in scope
 
-    zonkTcTypes tys            `thenM` \ new_tys ->
-    zonkTcThetaType theta      `thenM` \ new_theta ->
-    returnM (meth { tci_oid = new_id, tci_tys = new_tys, tci_theta = new_theta })
+    new_tys <- zonkTcTypes tys
+    new_theta <- zonkTcThetaType theta
+    return (meth { tci_oid = new_id, tci_tys = new_tys, tci_theta = new_theta })
        -- No need to zonk the tci_id
 
-zonkInst lit@(LitInst {tci_ty = ty})
-  = zonkTcType ty                      `thenM` \ new_ty ->
-    returnM (lit {tci_ty = new_ty})
+zonkInst lit@(LitInst {tci_ty = ty}) = do
+    new_ty <- zonkTcType ty
+    return (lit {tci_ty = new_ty})
 
 zonkInst implic@(ImplicInst {})
   = ASSERT( all isImmutableTyVar (tci_tyvars implic) )
@@ -483,7 +555,16 @@ zonkInst implic@(ImplicInst {})
        ; wanteds' <- zonkInsts (tci_wanted implic)
        ; return (implic {tci_given = givens',tci_wanted = wanteds'}) }
 
-zonkInsts insts = mappM zonkInst insts
+zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2})
+  = do { co' <- eitherEqInst eqinst 
+                 (\covar -> return (mkWantedCo covar)) 
+                 (\co    -> liftM mkGivenCo $ zonkTcType co)
+       ; ty1' <- zonkTcType ty1
+       ; ty2' <- zonkTcType ty2
+       ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' })
+       }
+
+zonkInsts insts = mapM zonkInst insts
 \end{code}
 
 
@@ -518,16 +599,28 @@ pprInsts insts = brackets (interpp'SP insts)
 
 pprInst, pprInstInFull :: Inst -> SDoc
 -- Debugging: print the evidence :: type
-pprInst inst = ppr (instName inst) <+> dcolon 
-               <+> (braces (ppr (instType inst)) $$
-                    ifPprDebug implic_stuff)
+pprInst i@(EqInst {tci_left = ty1, tci_right = ty2, tci_co = co}) 
+       = eitherEqInst i
+               (\covar -> text "Wanted" <+> ppr (TyVarTy covar) <+> dcolon <+> ppr (EqPred ty1 ty2))
+               (\co    -> text "Given"  <+> ppr co              <+> dcolon <+> ppr (EqPred ty1 ty2))
+pprInst inst = ppr name <> braces (pprUnique (getUnique name)) <+> dcolon 
+               <+> braces (ppr (instType inst) <> implicWantedEqs)
   where
-    implic_stuff | isImplicInst inst = ppr (tci_reft inst)
-                | otherwise         = empty
+    name = instName inst
+    implicWantedEqs
+      | isImplicInst inst = text " &" <+> 
+                            ppr (filter isEqInst (tci_wanted inst))
+      | otherwise        = empty
 
+pprInstInFull inst@(EqInst {}) = pprInst inst
 pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]
 
 tidyInst :: TidyEnv -> Inst -> Inst
+tidyInst env eq@(EqInst {tci_left = lty, tci_right = rty, tci_co = co}) =
+  eq { tci_left  = tidyType env lty
+     , tci_right = tidyType env rty
+     , tci_co    = either Left (Right . tidyType env) co
+     }
 tidyInst env lit@(LitInst {tci_ty = ty})   = lit {tci_ty = tidyType env ty}
 tidyInst env dict@(Dict {tci_pred = pred}) = dict {tci_pred = tidyPred env pred}
 tidyInst env meth@(Method {tci_tys = tys}) = meth {tci_tys = tidyTypes env tys}
@@ -619,8 +712,8 @@ addLocalInst home_ie ispec
 getOverlapFlag :: TcM OverlapFlag
 getOverlapFlag 
   = do         { dflags <- getDOpts
-       ; let overlap_ok    = dopt Opt_AllowOverlappingInstances dflags
-             incoherent_ok = dopt Opt_AllowIncoherentInstances  dflags
+       ; let overlap_ok    = dopt Opt_OverlappingInstances dflags
+             incoherent_ok = dopt Opt_IncoherentInstances  dflags
              overlap_flag | incoherent_ok = Incoherent
                           | overlap_ok    = OverlapOk
                           | otherwise     = NoOverlap
@@ -667,12 +760,14 @@ lookupSimpleInst :: Inst -> TcM LookupInstResult
 -- the LIE.  Instead, any Insts needed by the lookup are returned in
 -- the LookupInstResult, where they can be further processed by tcSimplify
 
+lookupSimpleInst (EqInst {}) = return NoInstance
+
 --------------------- Implications ------------------------
 lookupSimpleInst (ImplicInst {}) = return NoInstance
 
 --------------------- Methods ------------------------
 lookupSimpleInst (Method {tci_oid = id, tci_tys = tys, tci_theta = theta, tci_loc = loc})
-  = do { (dicts, dict_app) <- instCallDicts loc theta
+  = do { (dict_app, dicts) <- getLIE $ instCallDicts loc theta
        ; let co_fn = dict_app <.> mkWpTyApps tys
        ; return (GenInst dicts (L span $ HsWrap co_fn (HsVar id))) }
   where
@@ -685,39 +780,39 @@ lookupSimpleInst (Method {tci_oid = id, tci_tys = tys, tci_theta = theta, tci_lo
 -- [Same shortcut as in newOverloadedLit, but we
 --  may have done some unification by now]             
 
-lookupSimpleInst (LitInst {tci_lit = HsIntegral i from_integer_name, tci_ty = ty, tci_loc = loc})
+lookupSimpleInst (LitInst {tci_lit = HsIntegral i from_integer_name _, tci_ty = ty, tci_loc = loc})
   | Just expr <- shortCutIntLit i ty
-  = returnM (GenInst [] (noLoc expr))
+  = return (GenInst [] (noLoc expr))
   | otherwise
-  = ASSERT( from_integer_name `isHsVar` fromIntegerName )      -- A LitInst invariant
-    tcLookupId fromIntegerName                 `thenM` \ from_integer ->
-    tcInstClassOp loc from_integer [ty]                `thenM` \ method_inst ->
-    mkIntegerLit i                             `thenM` \ integer_lit ->
-    returnM (GenInst [method_inst]
+  = ASSERT( from_integer_name `isHsVar` fromIntegerName ) do   -- A LitInst invariant
+    from_integer <- tcLookupId fromIntegerName
+    method_inst <- tcInstClassOp loc from_integer [ty]
+    integer_lit <- mkIntegerLit i
+    return (GenInst [method_inst]
                     (mkHsApp (L (instLocSpan loc)
                                 (HsVar (instToId method_inst))) integer_lit))
 
-lookupSimpleInst (LitInst {tci_lit = HsFractional f from_rat_name, tci_ty = ty, tci_loc = loc})
+lookupSimpleInst (LitInst {tci_lit = HsFractional f from_rat_name _, tci_ty = ty, tci_loc = loc})
   | Just expr <- shortCutFracLit f ty
-  = returnM (GenInst [] (noLoc expr))
+  = return (GenInst [] (noLoc expr))
 
   | otherwise
-  = ASSERT( from_rat_name `isHsVar` fromRationalName ) -- A LitInst invariant
-    tcLookupId fromRationalName                        `thenM` \ from_rational ->
-    tcInstClassOp loc from_rational [ty]       `thenM` \ method_inst ->
-    mkRatLit f                                 `thenM` \ rat_lit ->
-    returnM (GenInst [method_inst] (mkHsApp (L (instLocSpan loc) 
+  = ASSERT( from_rat_name `isHsVar` fromRationalName ) do      -- A LitInst invariant
+    from_rational <- tcLookupId fromRationalName
+    method_inst <- tcInstClassOp loc from_rational [ty]
+    rat_lit <- mkRatLit f
+    return (GenInst [method_inst] (mkHsApp (L (instLocSpan loc) 
                                               (HsVar (instToId method_inst))) rat_lit))
 
-lookupSimpleInst (LitInst {tci_lit = HsIsString s from_string_name, tci_ty = ty, tci_loc = loc})
+lookupSimpleInst (LitInst {tci_lit = HsIsString s from_string_name _, tci_ty = ty, tci_loc = loc})
   | Just expr <- shortCutStringLit s ty
-  = returnM (GenInst [] (noLoc expr))
+  = return (GenInst [] (noLoc expr))
   | otherwise
-  = ASSERT( from_string_name `isHsVar` fromStringName )        -- A LitInst invariant
-    tcLookupId fromStringName                  `thenM` \ from_string ->
-    tcInstClassOp loc from_string [ty]         `thenM` \ method_inst ->
-    mkStrLit s                                 `thenM` \ string_lit ->
-    returnM (GenInst [method_inst]
+  = ASSERT( from_string_name `isHsVar` fromStringName ) do     -- A LitInst invariant
+    from_string <- tcLookupId fromStringName
+    method_inst <- tcInstClassOp loc from_string [ty]
+    string_lit <- mkStrLit s
+    return (GenInst [method_inst]
                     (mkHsApp (L (instLocSpan loc)
                                 (HsVar (instToId method_inst))) string_lit))
 
@@ -740,17 +835,17 @@ lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
 
     ; let inst_tv (Left tv)  = do { tv' <- tcInstTyVar tv; return (mkTyVarTy tv') }
          inst_tv (Right ty) = return ty
-    ; tys <- mappM inst_tv mb_inst_tys
+    ; tys <- mapM inst_tv mb_inst_tys
     ; let
        (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
        src_loc    = instLocSpan loc
        dfun       = HsVar dfun_id
     ; if null theta then
-       returnM (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
+        return (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
       else do
-    { (dicts, dict_app) <- instCallDicts loc theta
+    { (dict_app, dicts) <- getLIE $ instCallDicts loc theta -- !!!
     ; let co_fn = dict_app <.> mkWpTyApps tys
-    ; returnM (GenInst dicts (L src_loc $ HsWrap co_fn dfun))
+    ; return (GenInst dicts (L src_loc $ HsWrap co_fn dfun))
     }}}}
 
 ---------------
@@ -846,34 +941,122 @@ tcSyntaxName :: InstOrigin
 
 tcSyntaxName orig ty (std_nm, HsVar user_nm)
   | std_nm == user_nm
-  = newMethodFromName orig ty std_nm   `thenM` \ id ->
-    returnM (std_nm, HsVar id)
+  = do id <- newMethodFromName orig ty std_nm
+       return (std_nm, HsVar id)
 
-tcSyntaxName orig ty (std_nm, user_nm_expr)
-  = tcLookupId std_nm          `thenM` \ std_id ->
+tcSyntaxName orig ty (std_nm, user_nm_expr) = do
+    std_id <- tcLookupId std_nm
     let        
        -- C.f. newMethodAtLoc
        ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
        sigma1          = substTyWith [tv] [ty] tau
        -- Actually, the "tau-type" might be a sigma-type in the
        -- case of locally-polymorphic methods.
-    in
-    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1)      $
+
+    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
 
        -- Check that the user-supplied thing has the
        -- same type as the standard one.  
        -- Tiresome jiggling because tcCheckSigma takes a located expression
-    getSrcSpanM                                        `thenM` \ span -> 
-    tcPolyExpr (L span user_nm_expr) sigma1    `thenM` \ expr ->
-    returnM (std_nm, unLoc expr)
+     span <- getSrcSpanM
+     expr <- tcPolyExpr (L span user_nm_expr) sigma1
+     return (std_nm, unLoc expr)
 
-syntaxNameCtxt name orig ty tidy_env
-  = getInstLoc orig            `thenM` \ inst_loc ->
+syntaxNameCtxt name orig ty tidy_env = do
+    inst_loc <- getInstLoc orig
     let
        msg = vcat [ptext SLIT("When checking that") <+> quotes (ppr name) <+> 
                                ptext SLIT("(needed by a syntactic construct)"),
                    nest 2 (ptext SLIT("has the required type:") <+> ppr (tidyType tidy_env ty)),
                    nest 2 (ptext SLIT("arising from") <+> pprInstLoc inst_loc)]
-    in
-    returnM (tidy_env, msg)
+    
+    return (tidy_env, msg)
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+               EqInsts
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+mkGivenCo   :: Coercion -> Either TcTyVar Coercion
+mkGivenCo   =  Right
+
+mkWantedCo  :: TcTyVar  -> Either TcTyVar Coercion
+mkWantedCo  =  Left
+
+fromGivenCo :: Either TcTyVar Coercion -> Coercion
+fromGivenCo (Right co)          = co
+fromGivenCo _           = panic "fromGivenCo: not a wanted coercion"
+
+fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
+fromWantedCo _ (Left covar) = covar
+fromWantedCo msg _         = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+
+eitherEqInst :: Inst               -- given or wanted EqInst
+            -> (TcTyVar  -> a)     --  result if wanted
+            -> (Coercion -> a)     --  result if given
+            -> a               
+eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
+       = case either_co of
+               Left  covar -> withWanted covar
+               Right co    -> withGiven  co
+
+mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst]
+mkEqInsts preds cos = zipWithM mkEqInst preds cos
+
+mkEqInst :: PredType -> Either TcTyVar Coercion -> 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} 
+            ; return inst
+            }
+       where mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
+
+mkWantedEqInst :: PredType -> TcM Inst
+mkWantedEqInst pred@(EqPred ty1 ty2)
+  = do { cotv <- newMetaCoVar ty1 ty2
+       ; mkEqInst pred (Left cotv)
+       }
+
+-- 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
+             }
+
+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
+            }
+
+eqInstType :: Inst -> TcType
+eqInstType inst = eitherEqInst inst mkTyVarTy id
+
+eqInstCoercion :: Inst -> Either TcTyVar Coercion
+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}