Type families: new algorithm to solve equalities
[ghc-hetmet.git] / compiler / typecheck / Inst.lhs
index e175951..17dce30 100644 (file)
@@ -6,15 +6,8 @@
 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, 
+       Inst,
 
        pprInstances, pprDictsTheta, pprDictsInFull,    -- User error messages
        showLIE, pprInst, pprInsts, pprInstInFull,      -- Debugging messages
@@ -23,9 +16,8 @@ module Inst (
 
        newDictBndr, newDictBndrs, newDictBndrsO,
        instCall, instStupidTheta,
-       cloneDict, 
-       shortCutFracLit, shortCutIntLit, shortCutStringLit, newIPDict, 
-       newMethod, newMethodFromName, newMethodWithGivenTy, 
+       cloneDict, mkOverLit,
+       newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy, 
        tcInstClassOp, 
        tcSyntaxName, isHsVar,
 
@@ -42,25 +34,26 @@ module Inst (
        isTyVarDict, isMethodFor, 
 
        zonkInst, zonkInsts,
-       instToId, instToVar, instType, instName,
+       instToId, instToVar, instType, instName, instToDictBind,
+       addInstToDictBind,
 
        InstOrigin(..), InstLoc, pprInstLoc,
 
        mkWantedCo, mkGivenCo,
-       fromWantedCo, fromGivenCo,
-       eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
-       finalizeEqInst, writeWantedCoercion,
+       isWantedCo, fromWantedCo, fromGivenCo, eqInstCoType,
+        mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo,
+        mkRightTransEqInstCo, mkAppEqInstCo,
+       eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, finalizeEqInst, 
        eqInstType, updateEqInstCoercion,
-       eqInstCoercion,
-       eqInstLeftTy, eqInstRightTy
+       eqInstCoercion, eqInstTys
     ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-}  TcExpr( tcPolyExpr )
-import {-# SOURCE #-}  TcUnify( boxyUnify, unifyType )
+import {-# SOURCE #-}  TcUnify( boxyUnify {- , unifyType -} )
 
-import FastString(FastString)
+import FastString
 import HsSyn
 import TcHsSyn
 import TcRnMonad
@@ -69,6 +62,7 @@ import InstEnv
 import FunDeps
 import TcMType
 import TcType
+import MkCore
 import Type
 import TypeRep
 import Class
@@ -77,29 +71,29 @@ import Module
 import Coercion
 import HscTypes
 import CoreFVs
-import DataCon
 import Id
 import Name
 import NameSet
-import Literal
 import Var      ( Var, TyVar )
 import qualified Var
 import VarEnv
 import VarSet
-import TysWiredIn
 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}
 
 
+
 Selection
 ~~~~~~~~~
 \begin{code}
@@ -136,23 +130,23 @@ instType imp@(ImplicInst {})      = mkImplicTy (tci_tyvars imp) (tci_given imp)
 -- instType i@(EqInst {tci_co = co}) = eitherEqInst i TyVarTy id
 instType (EqInst {tci_left = ty1, tci_right = ty2}) = mkPredTy (EqPred ty1 ty2)
 
+mkImplicTy :: [TyVar] -> [Inst] -> [Inst] -> Type
 mkImplicTy tvs givens wanteds  -- The type of an implication constraint
-  = ASSERT( all isDict givens )
+  = ASSERT( all isAbstractableInst givens )
     -- pprTrace "mkImplicTy" (ppr givens) $
     -- 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)
+      mkBigCoreTupTy (map instType dict_wanteds)
 
+dictPred :: Inst -> TcPredType
 dictPred (Dict {tci_pred = pred}) = pred
 dictPred (EqInst {tci_left=ty1,tci_right=ty2}) = EqPred ty1 ty2
 dictPred inst                    = pprPanic "dictPred" (ppr inst)
 
+getDictClassTys :: Inst -> (Class, [Type])
 getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred
 getDictClassTys inst                    = pprPanic "getDictClassTys" (ppr inst)
 
@@ -162,6 +156,7 @@ getDictClassTys inst                         = pprPanic "getDictClassTys" (ppr inst)
 -- Leaving these in is really important for the call to fdPredsOfInsts
 -- in TcSimplify.inferLoop, because the result is fed to 'grow',
 -- which is supposed to be conservative
+fdPredsOfInst :: Inst -> [TcPredType]
 fdPredsOfInst (Dict {tci_pred = pred})              = [pred]
 fdPredsOfInst (Method {tci_theta = theta})   = theta
 fdPredsOfInst (ImplicInst {tci_given = gs, 
@@ -172,9 +167,10 @@ 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
-isInheritableInst other                               = True
+isInheritableInst _                            = True
 
 
 ---------------------------------
@@ -187,7 +183,7 @@ ipNamesOfInsts insts = [n | inst <- insts, n <- ipNamesOfInst inst]
 
 ipNamesOfInst (Dict {tci_pred = IParam n _}) = [ipNameName n]
 ipNamesOfInst (Method {tci_theta = theta})   = [ipNameName n | IParam n _ <- theta]
-ipNamesOfInst other                         = []
+ipNamesOfInst _                              = []
 
 ---------------------------------
 tyVarsOfInst :: Inst -> TcTyVarSet
@@ -203,8 +199,19 @@ tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wan
                -- Remember the free tyvars of a coercion
 tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 
+tyVarsOfInsts :: [Inst] -> VarSet
 tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
+tyVarsOfLIE :: Bag Inst -> VarSet
 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
@@ -216,39 +223,40 @@ isAbstractableInst inst = isDict inst || isEqInst inst
 
 isEqInst :: Inst -> Bool
 isEqInst (EqInst {}) = True
-isEqInst other       = False
+isEqInst _           = False
 
 isDict :: Inst -> Bool
 isDict (Dict {}) = True
-isDict other    = False
+isDict _         = False
 
 isClassDict :: Inst -> Bool
 isClassDict (Dict {tci_pred = pred}) = isClassPred pred
-isClassDict other                   = False
+isClassDict _                        = False
 
 isTyVarDict :: Inst -> Bool
 isTyVarDict (Dict {tci_pred = pred}) = isTyVarClassPred pred
-isTyVarDict other                   = False
+isTyVarDict _                        = False
 
 isIPDict :: Inst -> Bool
 isIPDict (Dict {tci_pred = pred}) = isIPPred pred
-isIPDict other                   = False
+isIPDict _                        = False
 
+isImplicInst :: Inst -> Bool
 isImplicInst (ImplicInst {}) = True
-isImplicInst other          = False
+isImplicInst _               = False
 
 isMethod :: Inst -> Bool
 isMethod (Method {}) = True
-isMethod other      = False
+isMethod _           = False
 
 isMethodFor :: TcIdSet -> Inst -> Bool
 isMethodFor ids (Method {tci_oid = id}) = id `elemVarSet` ids
-isMethodFor ids inst                   = False
+isMethodFor _   _                       = False
 
 isMethodOrLit :: Inst -> Bool
 isMethodOrLit (Method {})  = True
 isMethodOrLit (LitInst {}) = True
-isMethodOrLit other        = False
+isMethodOrLit _            = False
 \end{code}
 
 
@@ -314,7 +322,7 @@ instCallDicts :: InstLoc -> TcThetaType -> TcM HsWrapper
 -- 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 _ [] = return idHsWrapper
 
 -- instCallDicts loc (EqPred ty1 ty2 : preds)
 --   = do  { unifyType ty1 ty2 -- For now, we insist that they unify right away 
@@ -343,7 +351,7 @@ instCallDicts loc (pred : preds)
 
 -------------
 cloneDict :: Inst -> TcM Inst
-cloneDict dict@(Dict nm ty loc) = do { uniq <- newUnique
+cloneDict dict@(Dict nm _ _) = do { uniq <- newUnique
                                     ; return (dict {tci_name = setNameUnique nm uniq}) }
 cloneDict eq@(EqInst {})       = return eq
 cloneDict other = pprPanic "cloneDict" (ppr other)
@@ -354,15 +362,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 (\_ -> instToId dict) ip_name, dict)
 \end{code}
 
 
@@ -379,7 +387,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}
 
@@ -392,22 +400,23 @@ 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
+       -- always a class op, but with -XNoImplicitPrelude 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)
-
-newMethodWithGivenTy orig id tys
-  = getInstLoc orig            `thenM` \ loc ->
-    newMethod loc id tys       `thenM` \ inst ->
-    extendLIE inst             `thenM_`
-    returnM (instToId inst)
+    loc <- getInstLoc origin
+    inst <- tcInstClassOp loc id [ty]
+    extendLIE inst
+    return (instToId inst)
+
+newMethodWithGivenTy :: InstOrigin -> Id -> [Type] -> TcRn TcId
+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 
@@ -421,11 +430,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 ()
@@ -446,64 +454,34 @@ checkKind tv ty
 
 
 ---------------------------
-newMethod inst_loc id tys
-  = newUnique          `thenM` \ new_uniq ->
+newMethod :: InstLoc -> Id -> [Type] -> TcRn Inst
+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
-
-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
-  where
-    mk_lit con lit = HsApp (nlHsVar (dataConWrapId con)) (nlHsLit lit)
-
-shortCutStringLit :: FastString -> TcType -> Maybe (HsExpr TcId)
-shortCutStringLit s ty
-  | isStringTy ty                      -- Short cut for String
-  = Just (HsLit (HsString s))
-  | 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))
-
-mkRatLit :: Rational -> TcM (LHsExpr TcId)
-mkRatLit r
-  = tcMetaTy rationalTyConName         `thenM` \ rat_ty ->
-    getSrcSpanM                        `thenM` \ span -> 
-    returnM (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))
+mkOverLit :: OverLitVal -> TcM HsLit
+mkOverLit (HsIntegral i) 
+  = do { integer_ty <- tcMetaTy integerTyConName
+       ; return (HsInteger i integer_ty) }
+
+mkOverLit (HsFractional r)
+  = do { rat_ty <- tcMetaTy rationalTyConName
+       ; return (HsRat r rat_ty) }
+
+mkOverLit (HsIsString s) = return (HsString s)
 
 isHsVar :: HsExpr Name -> Name -> Bool
-isHsVar (HsVar f) g = f==g
-isHsVar other    g = False
+isHsVar (HsVar f) g = f == g
+isHsVar _        _ = False
 \end{code}
 
 
@@ -517,24 +495,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) )
@@ -544,14 +522,15 @@ zonkInst implic@(ImplicInst {})
 
 zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2})
   = do { co' <- eitherEqInst eqinst 
-                       (\covar -> return (mkWantedCo covar)) 
-                       (\co    -> zonkTcType co >>= \coercion -> return (mkGivenCo coercion))
+                 (\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})
+       ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' })
        }
 
-zonkInsts insts = mappM zonkInst insts
+zonkInsts :: [Inst] -> TcRn [Inst]
+zonkInsts insts = mapM zonkInst insts
 \end{code}
 
 
@@ -586,16 +565,18 @@ pprInsts insts = brackets (interpp'SP insts)
 
 pprInst, pprInstInFull :: Inst -> SDoc
 -- Debugging: print the evidence :: type
-pprInst i@(EqInst {tci_left = ty1, tci_right = ty2, tci_co = co}) 
+pprInst i@(EqInst {tci_left = ty1, tci_right = ty2}) 
        = 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 (instName inst) <+> dcolon 
-               <+> (braces (ppr (instType inst)) $$
-                    ifPprDebug implic_stuff)
+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)]
@@ -705,21 +686,25 @@ getOverlapFlag
                           
        ; return overlap_flag }
 
+traceDFuns :: [Instance] -> TcRn ()
 traceDFuns ispecs
   = traceTc (hang (text "Adding instances:") 2 (vcat (map pp ispecs)))
   where
     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
        -- Print the dfun name itself too
 
+funDepErr :: Instance -> [Instance] -> TcRn ()
 funDepErr ispec ispecs
   = addDictLoc ispec $
-    addErr (hang (ptext SLIT("Functional dependencies conflict between instance declarations:"))
+    addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
               2 (pprInstances (ispec:ispecs)))
+dupInstErr :: Instance -> Instance -> TcRn ()
 dupInstErr ispec dup_ispec
   = addDictLoc ispec $
-    addErr (hang (ptext SLIT("Duplicate instance declarations:"))
+    addErr (hang (ptext (sLit "Duplicate instance declarations:"))
               2 (pprInstances [ispec, dup_ispec]))
 
+addDictLoc :: Instance -> TcRn a -> TcRn a
 addDictLoc ispec thing_inside
   = setSrcSpan (mkSrcSpan loc loc) thing_inside
   where
@@ -765,41 +750,25 @@ 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})
-  | Just expr <- shortCutIntLit i ty
-  = returnM (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]
-                    (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})
-  | Just expr <- shortCutFracLit f ty
-  = returnM (GenInst [] (noLoc expr))
+lookupSimpleInst (LitInst { tci_lit = lit@OverLit { ol_val = lit_val
+                                                 , ol_rebindable = rebindable }
+                         , tci_ty = ty, tci_loc = iloc})
+  | debugIsOn && rebindable = panic "lookupSimpleInst" -- A LitInst invariant
+  | Just witness <- shortCutLit lit_val ty
+  = do { let lit' = lit { ol_witness = witness, ol_type = ty }
+       ; return (GenInst [] (L loc (HsOverLit lit'))) }
 
   | 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) 
-                                              (HsVar (instToId method_inst))) rat_lit))
-
-lookupSimpleInst (LitInst {tci_lit = HsIsString s from_string_name, tci_ty = ty, tci_loc = loc})
-  | Just expr <- shortCutStringLit s ty
-  = returnM (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]
-                    (mkHsApp (L (instLocSpan loc)
-                                (HsVar (instToId method_inst))) string_lit))
+  = do { hs_lit <- mkOverLit lit_val
+       ; from_thing <- tcLookupId (hsOverLitName lit_val)
+                 -- Not rebindable, so hsOverLitName is the right thing
+       ; method_inst <- tcInstClassOp iloc from_thing [ty]
+       ; let witness = HsApp (L loc (HsVar (instToId method_inst))) 
+                             (L loc (HsLit hs_lit))
+             lit' = lit { ol_witness = witness, ol_type = ty }
+       ; return (GenInst [method_inst] (L loc (HsOverLit lit'))) }
+  where
+    loc = instLocSpan iloc
 
 --------------------- Dictionaries ------------------------
 lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
@@ -809,7 +778,7 @@ lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
            Just (dfun_id, mb_inst_tys) -> do
 
     { use_stage <- getStage
-    ; checkWellStaged (ptext SLIT("instance for") <+> quotes (ppr pred))
+    ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
                      (topIdLvl dfun_id) use_stage
 
        -- It's possible that not all the tyvars are in
@@ -820,17 +789,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
     { (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))
     }}}}
 
 ---------------
@@ -864,8 +833,10 @@ lookupPred pred@(ClassP clas tys)
                        ; return Nothing }
        }}
 
-lookupPred ip_pred = return Nothing    -- Implicit parameters
+lookupPred (IParam {}) = return Nothing        -- Implicit parameters
+lookupPred (EqPred {}) = panic "lookupPred EqPred"
 
+record_dfun_usage :: Id -> TcRn ()
 record_dfun_usage dfun_id 
   = do { hsc_env <- getTopEnv
        ; let  dfun_name = idName dfun_id
@@ -893,7 +864,7 @@ tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
 %*                                                                     *
 %************************************************************************
 
-Suppose we are doing the -fno-implicit-prelude thing, and we encounter
+Suppose we are doing the -XNoImplicitPrelude thing, and we encounter
 a do-expression.  We have to find (>>) in the current environment, which is
 done by the rename. Then we have to check that it has the same type as
 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
@@ -926,36 +897,38 @@ 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)
-
-syntaxNameCtxt name orig ty tidy_env
-  = getInstLoc orig            `thenM` \ inst_loc ->
+     span <- getSrcSpanM
+     expr <- tcPolyExpr (L span user_nm_expr) sigma1
+     return (std_nm, unLoc expr)
+
+syntaxNameCtxt :: HsExpr Name -> InstOrigin -> Type -> TidyEnv
+               -> TcRn (TidyEnv, SDoc)
+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)
+       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)]
+    
+    return (tidy_env, msg)
 \end{code}
 
 %************************************************************************
@@ -964,86 +937,168 @@ syntaxNameCtxt name orig ty tidy_env
 %*                                                                     *
 %************************************************************************
 
+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
+isWantedCo :: EqInstCo -> Bool
+isWantedCo (Left _) = True
+isWantedCo _        = False
+
+fromGivenCo :: EqInstCo -> Coercion
 fromGivenCo (Right co)          = co
 fromGivenCo _           = panic "fromGivenCo: not a wanted coercion"
 
-fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
+fromWantedCo :: String -> EqInstCo -> TcTyVar
 fromWantedCo _ (Left covar) = covar
-fromWantedCo msg _         = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+fromWantedCo msg _         = 
+  panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+
+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
 
-eitherEqInst 
-       :: Inst                 -- given or wanted EqInst
-       -> (TcTyVar  -> a)      --      result if wanted
-       -> (Coercion -> a)      --      result if given
-       -> a            
+\begin{code}
+-- Coercion transformation: co = id
+--
+mkIdEqInstCo :: EqInstCo -> Type -> TcM ()
+mkIdEqInstCo (Left cotv) t
+  = writeMetaTyVar 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
+       ; writeMetaTyVar 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
+       ; writeMetaTyVar 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
+       ; writeMetaTyVar 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
+       ; writeMetaTyVar 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)
+\end{code}
+
+Operations on entire EqInst.
+
+\begin{code}
+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
+eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
 
-mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst]
+mkEqInsts :: [PredType] -> [EqInstCo] -> 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") src_span
+mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred)
 
 mkWantedEqInst :: PredType -> TcM Inst
 mkWantedEqInst pred@(EqPred ty1 ty2)
-  = do { cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
+  = do { cotv <- newMetaCoVar ty1 ty2
        ; mkEqInst pred (Left cotv)
        }
+mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred)
+
+-- 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})
+  = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
+
+         -- fill the coercion hole
+       ; let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted
+       ; writeMetaTyVar cotv (TyVarTy var)
+
+         -- set the new coercion
+       ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
+       ; return given
+       }
 
--- 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
-            }
+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
 
-eqInstLeftTy, eqInstRightTy :: Inst -> TcType
-eqInstLeftTy  = tci_left
-eqInstRightTy = tci_right
+eqInstTys :: Inst -> (TcType, TcType)
+eqInstTys inst = (tci_left inst, tci_right inst)
 
-updateEqInstCoercion :: (Either TcTyVar Coercion -> Either TcTyVar Coercion) -> Inst -> Inst
+updateEqInstCoercion :: (EqInstCo -> EqInstCo) -> Inst -> Inst
 updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst}
 \end{code}