Merge remote branch 'origin/master'
[ghc-hetmet.git] / compiler / typecheck / Inst.lhs
index 49fc942..378bbd6 100644 (file)
@@ -7,43 +7,35 @@ The @Inst@ type: dictionaries or method instances
 
 \begin{code}
 module Inst ( 
-       Inst, 
-
-       pprInstances, pprDictsTheta, pprDictsInFull,    -- User error messages
-       showLIE, pprInst, pprInsts, pprInstInFull,      -- Debugging messages
-
-       tidyInsts, tidyMoreInsts,
-
-       newDictBndr, newDictBndrs, newDictBndrsO,
-       instCall, instStupidTheta,
-       cloneDict, 
-       shortCutFracLit, shortCutIntLit, newIPDict, 
-       newMethod, newMethodFromName, newMethodWithGivenTy, 
-       tcInstClassOp, 
-       tcSyntaxName, isHsVar,
-
-       tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
-       ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
-       getDictClassTys, dictPred,
-
-       lookupSimpleInst, LookupInstResult(..), lookupPred, 
-       tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
-
-       isDict, isClassDict, isMethod, isImplicInst,
-       isIPDict, isInheritableInst, isMethodOrLit,
-       isTyVarDict, isMethodFor, getDefaultableDicts,
-
-       zonkInst, zonkInsts,
-       instToId, instToVar, instName,
-
-       InstOrigin(..), InstLoc, pprInstLoc
+       deeplySkolemise, 
+       deeplyInstantiate, instCall, instStupidTheta,
+       emitWanted, emitWanteds,
+
+       newOverloadedLit, mkOverLit, 
+     
+       tcGetInstEnvs, getOverlapFlag, tcExtendLocalInstEnv,
+       instCallConstraints, newMethodFromName,
+       tcSyntaxName,
+
+       -- Simple functions over evidence variables
+       hasEqualities, unitImplication,
+       
+       tyVarsOfWC, tyVarsOfBag, tyVarsOfEvVarXs, tyVarsOfEvVarX,
+       tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication,
+
+       tidyWantedEvVar, tidyWantedEvVars, tidyWC,
+       tidyEvVar, tidyImplication, tidyFlavoredEvVar,
+
+       substWantedEvVar, substWantedEvVars, substFlavoredEvVar,
+       substEvVar, substImplication
     ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-}  TcExpr( tcPolyExpr )
+import {-# SOURCE #-}  TcExpr( tcPolyExpr, tcSyntaxOp )
 import {-# SOURCE #-}  TcUnify( unifyType )
 
+import FastString
 import HsSyn
 import TcHsSyn
 import TcRnMonad
@@ -52,522 +44,345 @@ import InstEnv
 import FunDeps
 import TcMType
 import TcType
-import Type
 import Class
 import Unify
-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 Var      ( Var, TyVar, EvVar, varType, setVarType )
 import VarEnv
 import VarSet
-import TysWiredIn
 import PrelNames
-import BasicTypes
 import SrcLoc
 import DynFlags
+import Bag
 import Maybes
 import Util
 import Outputable
+import Data.List( mapAccumL )
 \end{code}
 
 
-Selection
-~~~~~~~~~
+
+%************************************************************************
+%*                                                                     *
+               Emitting constraints
+%*                                                                     *
+%************************************************************************
+
 \begin{code}
-instName :: Inst -> Name
-instName inst = Var.varName (instToVar inst)
-
-instToId :: Inst -> TcId
-instToId inst = ASSERT2( isId id, ppr inst ) id 
-             where
-               id = instToVar inst
-
-instToVar :: Inst -> Var
-instToVar (LitInst {tci_name = nm, tci_ty = ty})
-  = mkLocalId nm ty
-instToVar (Method {tci_id = id}) 
-  = id
-instToVar (Dict {tci_name = nm, tci_pred = pred})    
-  | isEqPred pred = Var.mkCoVar nm (mkPredTy pred)
-  | otherwise    = mkLocalId nm (mkPredTy pred)
-instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
-                      tci_wanted = wanteds})
-  = mkLocalId nm (mkImplicTy tvs givens wanteds)
-
-instType :: Inst -> Type
-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)
-
-mkImplicTy tvs givens wanteds  -- The type of an implication constraint
-  = ASSERT( all isDict 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)
-
-dictPred (Dict {tci_pred = pred}) = pred
-dictPred inst                    = pprPanic "dictPred" (ppr inst)
-
-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
--- 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 (Dict {tci_pred = pred})              = [pred]
-fdPredsOfInst (Method {tci_theta = theta})   = theta
-fdPredsOfInst (ImplicInst {tci_given = gs, 
-                          tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws)
-fdPredsOfInst (LitInst {})                  = []
-
-fdPredsOfInsts :: [Inst] -> [PredType]
-fdPredsOfInsts insts = concatMap fdPredsOfInst insts
-
-isInheritableInst (Dict {tci_pred = pred})     = isInheritablePred pred
-isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta
-isInheritableInst other                               = True
-
-
----------------------------------
--- Get the implicit parameters mentioned by these Insts
--- NB: the results of these functions are insensitive to zonking
-
-ipNamesOfInsts :: [Inst] -> [Name]
-ipNamesOfInst  :: Inst   -> [Name]
-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                         = []
-
----------------------------------
-tyVarsOfInst :: Inst -> TcTyVarSet
-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` idFreeTyVars 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
-
-
-tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
-tyVarsOfLIE   lie   = tyVarsOfInsts (lieToList lie)
+emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
+emitWanteds origin theta = mapM (emitWanted origin) theta
+
+emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
+emitWanted origin pred = do { loc <- getCtLoc origin
+                            ; ev  <- newWantedEvVar pred
+                            ; emitFlat (mkEvVarX ev loc)
+                            ; return ev }
+
+newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
+-- Used when Name is the wired-in name for a wired-in class method,
+-- so the caller knows its type for sure, which should be of form
+--    forall a. C a => <blah>
+-- newMethodFromName is supposed to instantiate just the outer 
+-- type variable and constraint
+
+newMethodFromName origin name inst_ty
+  = do { id <- tcLookupId name
+             -- Use tcLookupId not tcLookupGlobalId; the method is almost
+             -- always a class op, but with -XRebindableSyntax GHC is
+             -- meant to find whatever thing is in scope, and that may
+             -- be an ordinary function. 
+
+       ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
+             (the_tv:rest) = tvs
+             subst = zipOpenTvSubst [the_tv] [inst_ty]
+
+       ; wrap <- ASSERT( null rest && isSingleton theta )
+                 instCall origin [inst_ty] (substTheta subst theta)
+       ; return (mkHsWrap wrap (HsVar id)) }
 \end{code}
 
-Predicates
-~~~~~~~~~~
-\begin{code}
-isDict :: Inst -> Bool
-isDict (Dict {}) = True
-isDict other    = False
 
-isClassDict :: Inst -> Bool
-isClassDict (Dict {tci_pred = pred}) = isClassPred pred
-isClassDict other                   = False
+%************************************************************************
+%*                                                                     *
+       Deep instantiation and skolemisation
+%*                                                                     *
+%************************************************************************
+
+Note [Deep skolemisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+deeplySkolemise decomposes and skolemises a type, returning a type
+with all its arrows visible (ie not buried under foralls)
 
-isTyVarDict :: Inst -> Bool
-isTyVarDict (Dict {tci_pred = pred}) = isTyVarClassPred pred
-isTyVarDict other                   = False
+Examples:
 
-isIPDict :: Inst -> Bool
-isIPDict (Dict {tci_pred = pred}) = isIPPred pred
-isIPDict other                   = False
+  deeplySkolemise (Int -> forall a. Ord a => blah)  
+    =  ( wp, [a], [d:Ord a], Int -> blah )
+    where wp = \x:Int. /\a. \(d:Ord a). <hole> x
 
-isImplicInst (ImplicInst {}) = True
-isImplicInst other          = False
+  deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)  
+    =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
+    where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
 
-isMethod :: Inst -> Bool
-isMethod (Method {}) = True
-isMethod other      = False
+In general,
+  if      deeplySkolemise ty = (wrap, tvs, evs, rho)
+    and   e :: rho
+  then    wrap e :: ty
+    and   'wrap' binds tvs, evs
 
-isMethodFor :: TcIdSet -> Inst -> Bool
-isMethodFor ids (Method {tci_oid = id}) = id `elemVarSet` ids
-isMethodFor ids inst                   = False
+ToDo: this eta-abstraction plays fast and loose with termination,
+      because it can introduce extra lambdas.  Maybe add a `seq` to
+      fix this
 
-isMethodOrLit :: Inst -> Bool
-isMethodOrLit (Method {})  = True
-isMethodOrLit (LitInst {}) = True
-isMethodOrLit other        = False
-\end{code}
 
 \begin{code}
-getDefaultableDicts :: [Inst] -> ([(Inst, Class, TcTyVar)], TcTyVarSet)
--- Look for free dicts of the form (C tv), even inside implications
--- *and* the set of tyvars mentioned by all *other* constaints
--- This disgustingly ad-hoc function is solely to support defaulting
-getDefaultableDicts insts
-  = (concat ps, unionVarSets tvs)
-  where
-    (ps, tvs) = mapAndUnzip get insts
-    get d@(Dict {tci_pred = ClassP cls [ty]})
-       | Just tv <- tcGetTyVar_maybe ty = ([(d,cls,tv)], emptyVarSet)
-       | otherwise                      = ([], tyVarsOfType ty)
-    get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
-       = ([ up | up@(_,_,tv) <- ups, not (tv `elemVarSet` tv_set)],
-          ftvs `minusVarSet` tv_set)
-       where
-          tv_set = mkVarSet tvs
-          (ups, ftvs) = getDefaultableDicts wanteds
-    get inst = ([], tyVarsOfInst inst)
+deeplySkolemise
+  :: TcSigmaType
+  -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
+
+deeplySkolemise ty
+  | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
+  = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
+       ; tvs1 <- tcInstSkolTyVars tvs
+       ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
+       ; ev_vars1 <- newEvVars (substTheta subst theta)
+       ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
+       ; return ( mkWpLams ids1
+                   <.> mkWpTyLams tvs1
+                   <.> mkWpLams ev_vars1
+                   <.> wrap
+                   <.> mkWpEvVarApps ids1
+                , tvs1     ++ tvs2
+                , ev_vars1 ++ ev_vars2
+                , mkFunTys arg_tys rho ) }
+
+  | otherwise
+  = return (idHsWrapper, [], [], ty)
+
+deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
+--   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
+-- In general if
+-- if    deeplyInstantiate ty = (wrap, rho)
+-- and   e :: ty
+-- then  wrap e :: rho
+
+deeplyInstantiate orig ty
+  | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
+  = do { (_, tys, subst) <- tcInstTyVars tvs
+       ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
+       ; wrap1 <- instCall orig tys (substTheta subst theta)
+       ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
+       ; return (mkWpLams ids1 
+                    <.> wrap2
+                    <.> wrap1 
+                    <.> mkWpEvVarApps ids1,
+                 mkFunTys arg_tys rho2) }
+
+  | otherwise = return (idHsWrapper, ty)
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
-\subsection{Building dictionaries}
+            Instantiating a call
 %*                                                                     *
 %************************************************************************
 
--- newDictBndrs makes a dictionary at a binding site
--- instCall makes a dictionary at an occurrence site
---     and throws it into the LIE
-
 \begin{code}
 ----------------
-newDictBndrsO :: InstOrigin -> TcThetaType -> TcM [Inst]
-newDictBndrsO orig theta = do { loc <- getInstLoc orig
-                             ; newDictBndrs loc theta }
-
-newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst]
-newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
-
-newDictBndr :: InstLoc -> TcPredType -> TcM Inst
-newDictBndr 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}) }
-
-----------------
-instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
+instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
 -- 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 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
+  = do { dict_app <- instCallConstraints orig theta
        ; return (dict_app <.> mkWpTyApps 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 }
+instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
+-- Instantiates the TcTheta, puts all constraints thereby generated
+-- into the LIE, and returns a HsWrapper to enclose the call site.
 
-----------------
-instCallDicts :: InstLoc -> TcThetaType -> TcM ([Inst], HsWrapper)
--- This is the key place where equality predicates 
--- are unleashed into the world
-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 (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)) }
-
--------------
-cloneDict :: Inst -> TcM Inst  -- Only used for linear implicit params
-cloneDict dict@(Dict nm ty loc) = do { uniq <- newUnique
-                                    ; return (dict {tci_name = setNameUnique nm uniq}) }
-cloneDict other = pprPanic "cloneDict" (ppr other)
-
--- 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 
--- 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 ->
-    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)
-\end{code}
+instCallConstraints _ [] = return idHsWrapper
 
+instCallConstraints origin (EqPred ty1 ty2 : preds)    -- Try short-cut
+  = do  { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
+        ; co    <- unifyType ty1 ty2
+       ; co_fn <- instCallConstraints origin preds
+        ; return (co_fn <.> WpEvApp (EvCoercion co)) }
 
-\begin{code}
-mkPredName :: Unique -> InstLoc -> PredType -> Name
-mkPredName uniq loc pred_ty
-  = mkInternalName uniq occ (srcSpanStart (instLocSpan loc))
-  where
-    occ = case pred_ty of
-           ClassP cls _ -> mkDictOcc (getOccName cls)
-           IParam ip  _ -> getOccName (ipNameName ip)
-           EqPred ty  _ -> mkEqPredCoOcc baseOcc
-             where
-               -- 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 "$"
-                            Just (tc, _) -> getOccName tc
+instCallConstraints origin (pred : preds)
+  = do { ev_var <- emitWanted origin pred
+       ; co_fn <- instCallConstraints origin preds
+       ; return (co_fn <.> WpEvApp (EvId ev_var)) }
+
+----------------
+instStupidTheta :: CtOrigin -> 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 { _co <- instCallConstraints orig theta -- Discard the coercion
+       ; return () }
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection{Building methods (calls of overloaded functions)}
+               Literals
 %*                                                                     *
 %************************************************************************
 
+In newOverloadedLit we convert directly to an Int or Integer if we
+know that's what we want.  This may save some time, by not
+temporarily generating overloaded literals, but it won't catch all
+cases (the rest are caught in lookupInst).
 
 \begin{code}
-newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
-newMethodFromName origin ty name
-  = tcLookupId name            `thenM` \ id ->
-       -- 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)
-
-newMethodWithGivenTy orig id tys
-  = getInstLoc orig            `thenM` \ loc ->
-    newMethod loc id tys       `thenM` \ inst ->
-    extendLIE inst             `thenM_`
-    returnM (instToId inst)
-
---------------------------------------------
--- tcInstClassOp, and newMethod do *not* drop the 
--- Inst into the LIE; they just returns the Inst
--- This is important because they are used by TcSimplify
--- to simplify Insts
-
--- NB: the kind of the type variable to be instantiated
---     might be a sub-kind of the type to which it is applied,
---     notably when the latter is a type variable of kind ??
---     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
-       (tyvars, _rho) = tcSplitForAllTys (idType sel_id)
-    in
-    zipWithM_ checkKind tyvars tys     `thenM_` 
-    newMethod inst_loc sel_id tys
-
-checkKind :: TyVar -> TcType -> TcM ()
--- Ensure that the type has a sub-kind of the tyvar
-checkKind tv ty
-  = do { let ty1 = ty 
-               -- ty1 <- zonkTcType ty
-       ; if typeKind ty1 `isSubKind` Var.tyVarKind tv
-         then return ()
-         else 
-
-    pprPanic "checkKind: adding kind constraint" 
-            (vcat [ppr tv <+> ppr (Var.tyVarKind tv), 
-                   ppr ty <+> ppr ty1 <+> ppr (typeKind ty1)])
-       }
---    do       { tv1 <- tcInstTyVar tv
---     ; unifyType ty1 (mkTyVarTy tv1) } }
-
-
----------------------------
-newMethod inst_loc id tys
-  = newUnique          `thenM` \ new_uniq ->
-    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         = srcSpanStart (instLocSpan inst_loc)
-    in
-    returnM inst
-\end{code}
+newOverloadedLit :: CtOrigin
+                -> HsOverLit Name
+                -> TcRhoType
+                -> TcM (HsOverLit TcId)
+newOverloadedLit orig 
+  lit@(OverLit { ol_val = val, ol_rebindable = rebindable
+              , ol_witness = meth_name }) res_ty
+
+  | not rebindable
+  , Just expr <- shortCutLit val res_ty 
+       -- Do not generate a LitInst for rebindable syntax.  
+       -- Reason: If we do, tcSimplify will call lookupInst, which
+       --         will call tcSyntaxName, which does unification, 
+       --         which tcSimplify doesn't like
+  = return (lit { ol_witness = expr, ol_type = res_ty })
 
-\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)
-
-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))
-
-isHsVar :: HsExpr Name -> Name -> Bool
-isHsVar (HsVar f) g = f==g
-isHsVar other    g = False
+  | otherwise
+  = do { hs_lit <- mkOverLit val
+       ; let lit_ty = hsLitType hs_lit
+       ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
+               -- Overloaded literals must have liftedTypeKind, because
+               -- we're instantiating an overloaded function here,
+               -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
+               -- However this'll be picked up by tcSyntaxOp if necessary
+       ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
+       ; return (lit { ol_witness = witness, ol_type = res_ty }) }
+
+------------
+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)
 \end{code}
 
 
+
+
 %************************************************************************
 %*                                                                     *
-\subsection{Zonking}
+               Re-mappable syntax
+    
+     Used only for arrow syntax -- find a way to nuke this
 %*                                                                     *
 %************************************************************************
 
-Zonking makes sure that the instance types are fully zonked.
+Suppose we are doing the -XRebindableSyntax 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
+this:
 
-\begin{code}
-zonkInst :: Inst -> TcM Inst
-zonkInst dict@(Dict { tci_pred = pred})
-  = zonkTcPredType pred                        `thenM` \ new_pred ->
-    returnM (dict {tci_pred = new_pred})
-
-zonkInst meth@(Method {tci_oid = id, tci_tys = tys, tci_theta = theta}) 
-  = zonkId id                  `thenM` \ new_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 })
-       -- 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 implic@(ImplicInst {})
-  = ASSERT( all isImmutableTyVar (tci_tyvars implic) )
-    do         { givens'  <- zonkInsts (tci_given  implic)
-       ; wanteds' <- zonkInsts (tci_wanted implic)
-       ; return (implic {tci_given = givens',tci_wanted = wanteds'}) }
-
-zonkInsts insts = mappM zonkInst insts
-\end{code}
+  (>>) :: HB m n mn => m a -> n b -> mn b
 
+So the idea is to generate a local binding for (>>), thus:
 
-%************************************************************************
-%*                                                                     *
-\subsection{Printing}
-%*                                                                     *
-%************************************************************************
+       let then72 :: forall a b. m a -> m b -> m b
+           then72 = ...something involving the user's (>>)...
+       in
+       ...the do-expression...
+
+Now the do-expression can proceed using then72, which has exactly
+the expected type.
 
-ToDo: improve these pretty-printing things.  The ``origin'' is really only
-relevant in error messages.
+In fact tcSyntaxName just generates the RHS for then72, because we only
+want an actual binding in the do-expression case. For literals, we can 
+just use the expression inline.
 
 \begin{code}
-instance Outputable Inst where
-    ppr inst = pprInst inst
-
-pprDictsTheta :: [Inst] -> SDoc
--- Print in type-like fashion (Eq a, Show b)
--- The Inst can be an implication constraint, but not a Method or LitInst
-pprDictsTheta insts = parens (sep (punctuate comma (map (ppr . instType) insts)))
-
-pprDictsInFull :: [Inst] -> SDoc
--- Print in type-like fashion, but with source location
-pprDictsInFull dicts 
-  = vcat (map go dicts)
-  where
-    go dict = sep [quotes (ppr (instType dict)), nest 2 (pprInstArising dict)]
-
-pprInsts :: [Inst] -> SDoc
--- Debugging: print the evidence :: type
-pprInsts insts = brackets (interpp'SP insts)
+tcSyntaxName :: CtOrigin
+            -> TcType                  -- Type to instantiate it at
+            -> (Name, HsExpr Name)     -- (Standard name, user name)
+            -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
+--     *** NOW USED ONLY FOR CmdTop (sigh) ***
+-- NB: tcSyntaxName calls tcExpr, and hence can do unification.
+-- So we do not call it from lookupInst, which is called from tcSimplify
 
-pprInst, pprInstInFull :: Inst -> SDoc
--- Debugging: print the evidence :: type
-pprInst inst = ppr (instName inst) <+> dcolon 
-               <+> (braces (ppr (instType inst)) $$
-                    ifPprDebug implic_stuff)
-  where
-    implic_stuff | isImplicInst inst = ppr (tci_reft inst)
-                | otherwise         = empty
-
-pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]
-
-tidyInst :: TidyEnv -> Inst -> Inst
-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}
-tidyInst env implic@(ImplicInst {})
-  = implic { tci_tyvars = tvs' 
-          , tci_given  = map (tidyInst env') (tci_given  implic)
-          , tci_wanted = map (tidyInst env') (tci_wanted implic) }
-  where
-    (env', tvs') = mapAccumL tidyTyVarBndr env (tci_tyvars implic)
+tcSyntaxName orig ty (std_nm, HsVar user_nm)
+  | std_nm == user_nm
+  = do rhs <- newMethodFromName orig std_nm ty
+       return (std_nm, rhs)
 
-tidyMoreInsts :: TidyEnv -> [Inst] -> (TidyEnv, [Inst])
--- This function doesn't assume that the tyvars are in scope
--- so it works like tidyOpenType, returning a TidyEnv
-tidyMoreInsts env insts
-  = (env', map (tidyInst env') insts)
-  where
-    env' = tidyFreeTyVars env (tyVarsOfInsts insts)
+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.
 
-tidyInsts :: [Inst] -> (TidyEnv, [Inst])
-tidyInsts insts = tidyMoreInsts emptyTidyEnv insts
+    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
 
-showLIE :: SDoc -> TcM ()      -- Debugging
-showLIE str
-  = do { lie_var <- getLIEVar ;
-        lie <- readMutVar lie_var ;
-        traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) }
+       -- Check that the user-supplied thing has the
+       -- same type as the standard one.  
+       -- Tiresome jiggling because tcCheckSigma takes a located expression
+     span <- getSrcSpanM
+     expr <- tcPolyExpr (L span user_nm_expr) sigma1
+     return (std_nm, unLoc expr)
+
+syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
+               -> TcRn (TidyEnv, SDoc)
+syntaxNameCtxt name orig ty tidy_env = do
+    inst_loc <- getCtLoc 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 (pprArisingAt inst_loc)]
+    return (tidy_env, msg)
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-       Extending the instance environment
+               Instances
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
+getOverlapFlag :: TcM OverlapFlag
+getOverlapFlag 
+  = do         { dflags <- getDOpts
+       ; let overlap_ok    = xopt Opt_OverlappingInstances dflags
+             incoherent_ok = xopt Opt_IncoherentInstances  dflags
+             overlap_flag | incoherent_ok = Incoherent
+                          | overlap_ok    = OverlapOk
+                          | otherwise     = NoOverlap
+                          
+       ; return overlap_flag }
+
+tcGetInstEnvs :: TcM (InstEnv, InstEnv)
+-- Gets both the external-package inst-env
+-- and the home-pkg inst env (includes module being compiled)
+tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
+                    return (eps_inst_env eps, tcg_inst_env env) }
+
 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
   -- Add new locally-defined instances
 tcExtendLocalInstEnv dfuns thing_inside
@@ -587,10 +402,18 @@ addLocalInst home_ie ispec
                -- This is important because the template variables must
                -- not overlap with anything in the things being looked up
                -- (since we do unification).  
-               -- We use tcInstSkolType because we don't want to allocate fresh
-               --  *meta* type variables.  
+                --
+                -- We use tcInstSkolType because we don't want to allocate fresh
+                --  *meta* type variables.
+                --
+                -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
+                -- these variables must be bindable by tcUnifyTys.  See
+                -- the call to tcUnifyTys in InstEnv, and the special
+                -- treatment that instanceBindFun gives to isOverlappableTyVar
+                -- This is absurdly delicate.
+
          let dfun = instanceDFunId ispec
-       ; (tvs', theta', tau') <- tcInstSkolType InstSkol (idType dfun)
+        ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
        ; let   (cls, tys') = tcSplitDFunHead tau'
                dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
                ispec'      = setInstanceDFunId ispec dfun'
@@ -608,7 +431,7 @@ addLocalInst home_ie ispec
                -- Check for duplicate instance decls
        ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
              ; dup_ispecs = [ dup_ispec 
-                            | (_, dup_ispec) <- matches
+                            | (dup_ispec, _) <- matches
                             , let (_,_,_,dup_tys) = instanceHead dup_ispec
                             , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
                -- Find memebers of the match list which ispec itself matches.
@@ -620,267 +443,162 @@ addLocalInst home_ie ispec
                -- OK, now extend the envt
        ; return (extendInstEnv home_ie ispec') }
 
-getOverlapFlag :: TcM OverlapFlag
-getOverlapFlag 
-  = do         { dflags <- getDOpts
-       ; let overlap_ok    = dopt Opt_AllowOverlappingInstances dflags
-             incoherent_ok = dopt Opt_AllowIncoherentInstances  dflags
-             overlap_flag | incoherent_ok = Incoherent
-                          | overlap_ok    = OverlapOk
-                          | otherwise     = NoOverlap
-                          
-       ; return overlap_flag }
-
+traceDFuns :: [Instance] -> TcRn ()
 traceDFuns ispecs
-  = traceTc (hang (text "Adding instances:") 2 (vcat (map pp ispecs)))
+  = traceTc "Adding instances:" (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
    loc = getSrcLoc ispec
 \end{code}
-    
 
 %************************************************************************
 %*                                                                     *
-\subsection{Looking up Insts}
+       Simple functions over evidence variables
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-data LookupInstResult
-  = NoInstance
-  | GenInst [Inst] (LHsExpr TcId)      -- The expression and its needed insts
-
-lookupSimpleInst :: Inst -> TcM LookupInstResult
--- This is "simple" in tthat it returns NoInstance for implication constraints
-
--- It's important that lookupInst does not put any new stuff into
--- the LIE.  Instead, any Insts needed by the lookup are returned in
--- the LookupInstResult, where they can be further processed by tcSimplify
-
---------------------- 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
-       ; let co_fn = dict_app <.> mkWpTyApps tys
-       ; return (GenInst dicts (L span $ HsWrap co_fn (HsVar id))) }
+unitImplication :: Implication -> Bag Implication
+unitImplication implic
+  | isEmptyWC (ic_wanted implic) = emptyBag
+  | otherwise                    = unitBag implic
+
+hasEqualities :: [EvVar] -> Bool
+-- Has a bunch of canonical constraints (all givens) got any equalities in it?
+hasEqualities givens = any (has_eq . evVarPred) givens
   where
-    span = instLocSpan loc
-
---------------------- Literals ------------------------
--- Look for short cuts first: if the literal is *definitely* a 
--- int, integer, float or a double, generate the real thing here.
--- This is essential (see nofib/spectral/nucleic).
--- [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))
-
-  | 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))
-
---------------------- Dictionaries ------------------------
-lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
-  = do         { mb_result <- lookupPred pred
-       ; case mb_result of {
-           Nothing -> return NoInstance ;
-           Just (tenv, dfun_id) -> do
-
-    -- tenv is a substitution that instantiates the dfun_id 
-    -- to match the requested result type.   
-    -- 
-    -- We ASSUME that the dfun is quantified over the very same tyvars 
-    -- that are bound by the tenv.
-    -- 
-    -- However, the dfun
-    -- might have some tyvars that *only* appear in arguments
-    -- dfun :: forall a b. C a b, Ord b => D [a]
-    -- We instantiate b to a flexi type variable -- it'll presumably
-    -- become fixed later via functional dependencies
-    { use_stage <- getStage
-    ; checkWellStaged (ptext SLIT("instance for") <+> quotes (ppr pred))
-                     (topIdLvl dfun_id) use_stage
-
-       -- It's possible that not all the tyvars are in
-       -- the substitution, tenv. For example:
-       --      instance C X a => D X where ...
-       -- (presumably there's a functional dependency in class C)
-       -- Hence the open_tvs to instantiate any un-substituted tyvars. 
-    ; let (tyvars, rho) = tcSplitForAllTys (idType dfun_id)
-         open_tvs      = filter (`notElemTvSubst` tenv) tyvars
-    ; open_tvs' <- mappM tcInstTyVar open_tvs
-    ; let
-       tenv' = extendTvSubstList tenv open_tvs (mkTyVarTys open_tvs')
-               -- Since the open_tvs' are freshly made, they cannot possibly be captured by
-               -- any nested for-alls in rho.  So the in-scope set is unchanged
-       dfun_rho   = substTy tenv' rho
-       (theta, _) = tcSplitPhiTy dfun_rho
-       src_loc    = instLocSpan loc
-       dfun       = HsVar dfun_id
-       tys        = map (substTyVar tenv') tyvars
-    ; if null theta then
-       returnM (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
-      else do
-    { (dicts, dict_app) <- instCallDicts loc theta
-    ; let co_fn = dict_app <.> mkWpTyApps tys
-    ; returnM (GenInst dicts (L src_loc $ HsWrap co_fn dfun))
-    }}}}
-
----------------
-lookupPred :: TcPredType -> TcM (Maybe (TvSubst, DFunId))
--- Look up a class constraint in the instance environment
-lookupPred pred@(ClassP clas tys)
-  = do { eps     <- getEps
-       ; tcg_env <- getGblEnv
-       ; let inst_envs = (eps_inst_env eps, tcg_inst_env tcg_env)
-       ; case lookupInstEnv inst_envs clas tys of {
-           ([(tenv, ispec)], []) 
-               -> do   { let dfun_id = is_dfun ispec
-                       ; traceTc (text "lookupInst success" <+> 
-                                  vcat [text "dict" <+> ppr pred, 
-                                        text "witness" <+> ppr dfun_id
-                                        <+> ppr (idType dfun_id) ])
-                               -- Record that this dfun is needed
-                       ; record_dfun_usage dfun_id
-                       ; return (Just (tenv, dfun_id)) } ;
-
-           (matches, unifs)
-               -> do   { traceTc (text "lookupInst fail" <+> 
-                                  vcat [text "dict" <+> ppr pred,
-                                        text "matches" <+> ppr matches,
-                                        text "unifs" <+> ppr unifs])
-               -- In the case of overlap (multiple matches) we report
-               -- NoInstance here.  That has the effect of making the 
-               -- context-simplifier return the dict as an irreducible one.
-               -- Then it'll be given to addNoInstanceErrs, which will do another
-               -- lookupInstEnv to get the detailed info about what went wrong.
-                       ; return Nothing }
-       }}
-
-lookupPred ip_pred = return Nothing    -- Implicit parameters
-
-record_dfun_usage dfun_id 
-  = do { hsc_env <- getTopEnv
-       ; let  dfun_name = idName dfun_id
-              dfun_mod  = 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
-          else do { tcg_env <- getGblEnv
-                  ; updMutVar (tcg_inst_uses tcg_env)
-                              (`addOneToNameSet` idName dfun_id) }}
-
-
-tcGetInstEnvs :: TcM (InstEnv, InstEnv)
--- Gets both the external-package inst-env
--- and the home-pkg inst env (includes module being compiled)
-tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
-                    return (eps_inst_env eps, tcg_inst_env env) }
-\end{code}
-
-
-
-%************************************************************************
-%*                                                                     *
-               Re-mappable syntax
-%*                                                                     *
-%************************************************************************
-
-Suppose we are doing the -fno-implicit-prelude 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
-this:
-
-  (>>) :: HB m n mn => m a -> n b -> mn b
-
-So the idea is to generate a local binding for (>>), thus:
-
-       let then72 :: forall a b. m a -> m b -> m b
-           then72 = ...something involving the user's (>>)...
-       in
-       ...the do-expression...
+    has_eq (EqPred {})              = True
+    has_eq (IParam {})              = False
+    has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
+
+---------------- Getting free tyvars -------------------------
+tyVarsOfWC :: WantedConstraints -> TyVarSet
+tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+  = tyVarsOfEvVarXs flat `unionVarSet`
+    tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
+    tyVarsOfEvVarXs insol
+
+tyVarsOfImplication :: Implication -> TyVarSet
+tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
+  = tyVarsOfWC wanted `minusVarSet` skols
+
+tyVarsOfEvVarX :: EvVarX a -> TyVarSet
+tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev
+
+tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet
+tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX
+
+tyVarsOfEvVar :: EvVar -> TyVarSet
+tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
+
+tyVarsOfEvVars :: [EvVar] -> TyVarSet
+tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
+
+tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
+tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
+
+---------------- Tidying -------------------------
+tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints
+tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+  = WC { wc_flat  = tidyWantedEvVars env flat
+       , wc_impl  = mapBag (tidyImplication env) implic
+       , wc_insol = mapBag (tidyFlavoredEvVar env) insol }
+
+tidyImplication :: TidyEnv -> Implication -> Implication
+tidyImplication env implic@(Implic { ic_skols = tvs
+                                   , ic_given = given
+                                   , ic_wanted = wanted
+                                   , ic_loc = loc })
+  = implic { ic_skols = mkVarSet tvs'
+           , ic_given = map (tidyEvVar env1) given
+           , ic_wanted = tidyWC env1 wanted
+           , ic_loc = tidyGivenLoc env1 loc }
+  where
+   (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs)
+
+tidyEvVar :: TidyEnv -> EvVar -> EvVar
+tidyEvVar env var = setVarType var (tidyType env (varType var))
+
+tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
+tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l
+
+tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
+tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
+
+tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar
+tidyFlavoredEvVar env (EvVarX v fl)
+  = EvVarX (tidyEvVar env v) (tidyFlavor env fl)
+
+tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
+tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk
+tidyFlavor _   fl          = fl
+
+tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
+tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
+
+tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
+tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
+tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
+tidySkolemInfo _   info            = info
+
+---------------- Substitution -------------------------
+substWC :: TvSubst -> WantedConstraints -> WantedConstraints
+substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+  = WC { wc_flat = substWantedEvVars subst flat
+       , wc_impl = mapBag (substImplication subst) implic
+       , wc_insol = mapBag (substFlavoredEvVar subst) insol }
+
+substImplication :: TvSubst -> Implication -> Implication
+substImplication subst implic@(Implic { ic_skols = tvs
+                                      , ic_given = given
+                                      , ic_wanted = wanted
+                                      , ic_loc = loc })
+  = implic { ic_skols  = mkVarSet tvs'
+           , ic_given  = map (substEvVar subst1) given
+           , ic_wanted = substWC subst1 wanted
+           , ic_loc    = substGivenLoc subst1 loc }
+  where
+   (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs)
 
-Now the do-expression can proceed using then72, which has exactly
-the expected type.
+substEvVar :: TvSubst -> EvVar -> EvVar
+substEvVar subst var = setVarType var (substTy subst (varType var))
 
-In fact tcSyntaxName just generates the RHS for then72, because we only
-want an actual binding in the do-expression case. For literals, we can 
-just use the expression inline.
+substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
+substWantedEvVars subst = mapBag (substWantedEvVar subst)
 
-\begin{code}
-tcSyntaxName :: InstOrigin
-            -> TcType                  -- Type to instantiate it at
-            -> (Name, HsExpr Name)     -- (Standard name, user name)
-            -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
---     *** NOW USED ONLY FOR CmdTop (sigh) ***
--- NB: tcSyntaxName calls tcExpr, and hence can do unification.
--- So we do not call it from lookupInst, which is called from tcSimplify
+substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
+substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l
 
-tcSyntaxName orig ty (std_nm, HsVar user_nm)
-  | std_nm == user_nm
-  = newMethodFromName orig ty std_nm   `thenM` \ id ->
-    returnM (std_nm, HsVar id)
+substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
+substFlavoredEvVar subst (EvVarX v fl)
+  = EvVarX (substEvVar subst v) (substFlavor subst fl)
 
-tcSyntaxName orig ty (std_nm, user_nm_expr)
-  = tcLookupId std_nm          `thenM` \ std_id ->
-    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)      $
+substFlavor :: TvSubst -> CtFlavor -> CtFlavor
+substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk
+substFlavor _     fl             = fl
 
-       -- 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)
+substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
+substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
 
-syntaxNameCtxt name orig ty tidy_env
-  = getInstLoc orig            `thenM` \ inst_loc ->
-    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)
+substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
+substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
+substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
+substSkolemInfo _     info            = info
 \end{code}