Record the original text along with parsed Rationals: fixes #2245
[ghc-hetmet.git] / compiler / typecheck / Inst.lhs
index 77ca56a..8db1aeb 100644 (file)
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section[Inst]{The @Inst@ type: dictionaries or method instances}
+
+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,
-
-       newDicts, newDictAtLoc, newDictsAtLoc, cloneDict, 
-       shortCutFracLit, shortCutIntLit, newIPDict, 
-       newMethod, newMethodFromName, newMethodWithGivenTy, 
-       tcInstClassOp, tcInstStupidTheta,
-       tcSyntaxName, isHsVar,
-
-       tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
-       ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
-       instLoc, getDictClassTys, dictPred,
-
-       lookupInst, LookupInstResult(..), lookupPred, 
-       tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
-
-       isDict, isClassDict, isMethod, 
-       isLinearInst, linearInstType, isIPDict, isInheritableInst,
-       isTyVarDict, isMethodFor, 
-
-       zonkInst, zonkInsts,
-       instToId, 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 HsSyn   ( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp,
-                 nlHsLit, nlHsVar )
-import TcHsSyn ( mkHsTyApp, mkHsDictApp, zonkId )
+import FastString
+import HsSyn
+import TcHsSyn
 import TcRnMonad
-import TcEnv   ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
-import InstEnv ( DFunId, InstEnv, Instance(..), OverlapFlag(..),
-                 lookupInstEnv, extendInstEnv, pprInstances, 
-                 instanceHead, instanceDFunId, setInstanceDFunId )
-import FunDeps ( checkFunDeps )
-import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, zonkTcThetaType, 
-                 tcInstTyVar, tcInstSkolType
-               )
-import TcType  ( Type, TcType, TcThetaType, TcTyVarSet, TcPredType,
-                 BoxyRhoType,
-                 PredType(..), SkolemInfo(..), typeKind, mkSigmaTy,
-                 tcSplitForAllTys, applyTys, 
-                 tcSplitPhiTy, tcSplitDFunHead,
-                 isIntTy,isFloatTy, isIntegerTy, isDoubleTy,
-                 mkPredTy, mkTyVarTys,
-                 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred,
-                 isClassPred, isTyVarClassPred, isLinearPred, 
-                 getClassPredTys, mkPredName,
-                 isInheritablePred, isIPPred, 
-                 tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy, 
-                 pprPred, pprParendType, pprTheta 
-               )
-import Type    ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSubst,
-                 notElemTvSubst, extendTvSubstList )
-import Unify   ( tcMatchTys )
-import Module  ( modulePackageId )
-import Kind    ( isSubKind )
-import HscTypes        ( ExternalPackageState(..), HscEnv(..) )
-import CoreFVs ( idFreeTyVars )
-import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName, dataConWrapId )
-import Id      ( Id, idName, idType, mkUserLocal, mkLocalId )
-import Name    ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
-                 isInternalName, setNameUnique )
-import NameSet ( addOneToNameSet )
-import Literal ( inIntRange )
-import Var     ( TyVar, tyVarKind, setIdType )
-import VarEnv  ( TidyEnv, emptyTidyEnv )
-import VarSet  ( elemVarSet, emptyVarSet, unionVarSet, mkVarSet )
-import TysWiredIn ( floatDataCon, doubleDataCon )
-import PrelNames       ( integerTyConName, fromIntegerName, fromRationalName, rationalTyConName )
-import BasicTypes( IPName(..), mapIPName, ipNameName )
-import UniqSupply( uniqsFromSupply )
-import SrcLoc  ( mkSrcSpan, noLoc, unLoc, Located(..) )
-import DynFlags        ( DynFlag(..), DynFlags(..), dopt )
-import Maybes  ( isJust )
+import TcEnv
+import InstEnv
+import FunDeps
+import TcMType
+import TcType
+import Class
+import Unify
+import HscTypes
+import Id
+import Name
+import Var      ( Var, TyVar, EvVar, varType, setVarType )
+import VarEnv
+import VarSet
+import PrelNames
+import SrcLoc
+import DynFlags
+import Bag
+import BasicTypes
+import Maybes
+import Util
 import Outputable
+import Data.List( mapAccumL )
 \end{code}
 
 
-Selection
-~~~~~~~~~
-\begin{code}
-instName :: Inst -> Name
-instName inst = idName (instToId inst)
-
-instToId :: Inst -> TcId
-instToId (LitInst nm _ ty _) = mkLocalId nm ty
-instToId (Dict nm pred _)    = mkLocalId nm (mkPredTy pred)
-instToId (Method id _ _ _ _) = id
-
-instLoc (Dict _ _       loc) = loc
-instLoc (Method _ _ _ _ loc) = loc
-instLoc (LitInst _ _ _  loc) = loc
 
-dictPred (Dict _ pred _ ) = pred
-dictPred inst            = pprPanic "dictPred" (ppr inst)
+%************************************************************************
+%*                                                                     *
+               Emitting constraints
+%*                                                                     *
+%************************************************************************
 
-getDictClassTys (Dict _ pred _) = getClassPredTys pred
+\begin{code}
+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}
 
--- 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 _ pred _)       = [pred]
-fdPredsOfInst (Method _ _ _ theta _) = theta
-fdPredsOfInst other                 = []       -- LitInsts etc
 
-fdPredsOfInsts :: [Inst] -> [PredType]
-fdPredsOfInsts insts = concatMap fdPredsOfInst insts
+%************************************************************************
+%*                                                                     *
+       Deep instantiation and skolemisation
+%*                                                                     *
+%************************************************************************
 
-isInheritableInst (Dict _ pred _)       = isInheritablePred pred
-isInheritableInst (Method _ _ _ theta _) = all isInheritablePred theta
-isInheritableInst other                         = True
+Note [Deep skolemisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+deeplySkolemise decomposes and skolemises a type, returning a type
+with all its arrows visible (ie not buried under foralls)
 
+Examples:
 
-ipNamesOfInsts :: [Inst] -> [Name]
-ipNamesOfInst  :: Inst   -> [Name]
--- Get the implicit parameters mentioned by these Insts
--- NB: ?x and %x get different Names
-ipNamesOfInsts insts = [n | inst <- insts, n <- ipNamesOfInst inst]
+  deeplySkolemise (Int -> forall a. Ord a => blah)  
+    =  ( wp, [a], [d:Ord a], Int -> blah )
+    where wp = \x:Int. /\a. \(d:Ord a). <hole> x
 
-ipNamesOfInst (Dict _ (IParam n _) _) = [ipNameName n]
-ipNamesOfInst (Method _ _ _ theta _)  = [ipNameName n | IParam n _ <- theta]
-ipNamesOfInst other                  = []
+  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
 
-tyVarsOfInst :: Inst -> TcTyVarSet
-tyVarsOfInst (LitInst _ _ ty _)    = tyVarsOfType  ty
-tyVarsOfInst (Dict _ pred _)       = tyVarsOfPred pred
-tyVarsOfInst (Method _ id tys _ _) = tyVarsOfTypes tys `unionVarSet` idFreeTyVars id
-                                        -- The id might have free type variables; in the case of
-                                        -- locally-overloaded class methods, for example
+In general,
+  if      deeplySkolemise ty = (wrap, tvs, evs, rho)
+    and   e :: rho
+  then    wrap e :: ty
+    and   'wrap' binds tvs, evs
 
+ToDo: this eta-abstraction plays fast and loose with termination,
+      because it can introduce extra lambdas.  Maybe add a `seq` to
+      fix this
 
-tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
-tyVarsOfLIE   lie   = tyVarsOfInsts (lieToList lie)
-\end{code}
 
-Predicates
-~~~~~~~~~~
 \begin{code}
-isDict :: Inst -> Bool
-isDict (Dict _ _ _) = True
-isDict other       = False
-
-isClassDict :: Inst -> Bool
-isClassDict (Dict _ pred _) = isClassPred pred
-isClassDict other          = False
-
-isTyVarDict :: Inst -> Bool
-isTyVarDict (Dict _ pred _) = isTyVarClassPred pred
-isTyVarDict other          = False
-
-isIPDict :: Inst -> Bool
-isIPDict (Dict _ pred _) = isIPPred pred
-isIPDict other          = False
-
-isMethod :: Inst -> Bool
-isMethod (Method {}) = True
-isMethod other      = False
-
-isMethodFor :: TcIdSet -> Inst -> Bool
-isMethodFor ids (Method uniq id tys _ loc) = id `elemVarSet` ids
-isMethodFor ids inst                      = False
-
-isLinearInst :: Inst -> Bool
-isLinearInst (Dict _ pred _) = isLinearPred pred
-isLinearInst other          = False
-       -- We never build Method Insts that have
-       -- linear implicit paramters in them.
-       -- Hence no need to look for Methods
-       -- See TcExpr.tcId 
-
-linearInstType :: Inst -> TcType       -- %x::t  -->  t
-linearInstType (Dict _ (IParam _ ty) _) = ty
-\end{code}
+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
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-newDicts :: InstOrigin
-        -> TcThetaType
-        -> TcM [Inst]
-newDicts orig theta
-  = getInstLoc orig            `thenM` \ loc ->
-    newDictsAtLoc loc theta
-
-cloneDict :: Inst -> TcM Inst
-cloneDict (Dict nm ty loc) = newUnique `thenM` \ uniq ->
-                            returnM (Dict (setNameUnique nm uniq) ty loc)
-
-newDictAtLoc :: InstLoc -> TcPredType -> TcM Inst
-newDictAtLoc inst_loc pred
-  = do { uniq <- newUnique
-       ; return (mkDict inst_loc uniq pred) }
-
-newDictsAtLoc :: InstLoc -> TcThetaType -> TcM [Inst]
-newDictsAtLoc inst_loc theta
-  = newUniqueSupply            `thenM` \ us ->
-    returnM (zipWith (mkDict inst_loc) (uniqsFromSupply us) theta)
-
-mkDict inst_loc uniq pred
-  = Dict name pred inst_loc
-  where
-    name = mkPredName uniq (instLocSrcLoc inst_loc) pred 
-
--- 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 name.
-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 (instLocSrcLoc inst_loc) pred 
-       dict = Dict name pred inst_loc
-    in
-    returnM (mapIPName (\n -> instToId dict) ip_name, dict)
+----------------
+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) Returns an HsWrapper ([.] tys dicts)
+
+instCall orig tys theta 
+  = do { dict_app <- instCallConstraints orig theta
+       ; return (dict_app <.> mkWpTyApps tys) }
+
+----------------
+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.
+
+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)) }
+
+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}
-tcInstStupidTheta :: DataCon -> [TcType] -> TcM ()
--- Instantiate the "stupid theta" of the data con, and throw 
--- the constraints into the constraint set
-tcInstStupidTheta data_con inst_tys
-  | null stupid_theta
-  = return ()
+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 })
+
   | otherwise
-  = do { stupid_dicts <- newDicts (OccurrenceOf (dataConName data_con))
-                                  (substTheta tenv stupid_theta)
-       ; extendLIEs stupid_dicts }
-  where
-    stupid_theta = dataConStupidTheta data_con
-    tenv = zipTopTvSubst (dataConTyVars data_con) inst_tys
-
-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` tyVarKind tv
-         then return ()
-         else 
-
-    pprPanic "checkKind: adding kind constraint" 
-            (vcat [ppr tv <+> ppr (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 meth_id id tys theta inst_loc
-       loc         = instLocSrcLoc inst_loc
-    in
-    returnM inst
+  = 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 (fl_value r) rat_ty) }
+
+mkOverLit (HsIsString s) = return (HsString s)
 \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)
-
-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
-\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 name pred loc)
-  = zonkTcPredType pred                        `thenM` \ new_pred ->
-    returnM (Dict name new_pred loc)
-
-zonkInst (Method m id tys theta loc) 
-  = 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 (Method m new_id new_tys new_theta loc)
-
-zonkInst (LitInst nm lit ty loc)
-  = zonkTcType ty                      `thenM` \ new_ty ->
-    returnM (LitInst nm lit new_ty loc)
-
-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...
 
-ToDo: improve these pretty-printing things.  The ``origin'' is really only
-relevant in error messages.
+Now the do-expression can proceed using then72, which has exactly
+the expected type.
+
+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
+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
 
-pprDictsTheta :: [Inst] -> SDoc
--- Print in type-like fashion (Eq a, Show b)
-pprDictsTheta dicts = pprTheta (map dictPred dicts)
+tcSyntaxName orig ty (std_nm, HsVar user_nm)
+  | std_nm == user_nm
+  = do rhs <- newMethodFromName orig std_nm ty
+       return (std_nm, rhs)
 
-pprDictsInFull :: [Inst] -> SDoc
--- Print in type-like fashion, but with source location
-pprDictsInFull dicts 
-  = vcat (map go dicts)
-  where
-    go dict = sep [quotes (ppr (dictPred dict)), nest 2 (pprInstLoc (instLoc dict))]
-
-pprInsts :: [Inst] -> SDoc
--- Debugging: print the evidence :: type
-pprInsts insts  = brackets (interpp'SP insts)
-
-pprInst, pprInstInFull :: Inst -> SDoc
--- Debugging: print the evidence :: type
-pprInst (LitInst nm lit ty loc) = ppr nm <+> dcolon <+> ppr ty
-pprInst (Dict nm pred loc)      = ppr nm <+> dcolon <+> pprPred pred
-
-pprInst m@(Method inst_id id tys theta loc)
-  = ppr inst_id <+> dcolon <+> 
-       braces (sep [ppr id <+> ptext SLIT("at"),
-                    brackets (sep (map pprParendType tys))])
-
-pprInstInFull inst
-  = sep [quotes (pprInst inst), nest 2 (pprInstLoc (instLoc inst))]
-
-tidyInst :: TidyEnv -> Inst -> Inst
-tidyInst env (LitInst nm lit ty loc)    = LitInst nm lit (tidyType env ty) loc
-tidyInst env (Dict nm pred loc)         = Dict nm (tidyPred env pred) loc
-tidyInst env (Method u id tys theta loc) = Method u id (tidyTypes env tys) theta loc
-
-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
@@ -493,10 +403,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 dfun) (idType dfun)
+        ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
        ; let   (cls, tys') = tcSplitDFunHead tau'
                dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
                ispec'      = setInstanceDFunId ispec dfun'
@@ -514,7 +432,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.
@@ -526,265 +444,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
-  | SimpleInst (LHsExpr TcId)          -- Just a variable, type application, or literal
-  | GenInst    [Inst] (LHsExpr TcId)   -- The expression and its needed insts
-
-lookupInst :: Inst -> TcM LookupInstResult
--- 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
-
-
--- Methods
-
-lookupInst inst@(Method _ id tys theta loc)
-  = newDictsAtLoc loc theta            `thenM` \ dicts ->
-    returnM (GenInst dicts (mkHsDictApp (mkHsTyApp (L span (HsVar id)) tys) (map instToId dicts)))
+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 = instLocSrcSpan 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]             
-
-lookupInst inst@(LitInst _nm (HsIntegral i from_integer_name) ty loc)
-  | Just expr <- shortCutIntLit i ty
-  = returnM (GenInst [] (noLoc expr))  -- GenInst, not SimpleInst, because 
-                                       -- expr may be a constructor application
-  | 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 (instLocSrcSpan loc)
-                                (HsVar (instToId method_inst))) integer_lit))
-
-lookupInst inst@(LitInst _nm (HsFractional f from_rat_name) ty 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 (instLocSrcSpan loc) 
-                                              (HsVar (instToId method_inst))) rat_lit))
-
--- Dictionaries
-lookupInst (Dict _ pred 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
-       ty_app     = mkHsTyApp (L (instLocSrcSpan loc) (HsVar dfun_id)) 
-                              (map (substTyVar tenv') tyvars)
-    ; if null theta then
-       returnM (SimpleInst ty_app)
-      else do
-    { dicts <- newDictsAtLoc loc theta
-    ; let rhs = mkHsDictApp ty_app (map instToId dicts)
-    ; returnM (GenInst dicts rhs)
-    }}}}
-
----------------
-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
-
-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
-%*                                                                     *
-%************************************************************************
+    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) = Given (tidyGivenLoc env loc)
+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)
 
-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:
+substEvVar :: TvSubst -> EvVar -> EvVar
+substEvVar subst var = setVarType var (substTy subst (varType var))
 
-  (>>) :: HB m n mn => m a -> n b -> mn b
+substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
+substWantedEvVars subst = mapBag (substWantedEvVar subst)
 
-So the idea is to generate a local binding for (>>), thus:
+substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
+substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l
 
-       let then72 :: forall a b. m a -> m b -> m b
-           then72 = ...something involving the user's (>>)...
-       in
-       ...the do-expression...
+substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
+substFlavoredEvVar subst (EvVarX v fl)
+  = EvVarX (substEvVar subst v) (substFlavor subst fl)
 
-Now the do-expression can proceed using then72, which has exactly
-the expected type.
+substFlavor :: TvSubst -> CtFlavor -> CtFlavor
+substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
+substFlavor _     fl          = fl
 
-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.
+substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
+substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
 
-\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
-
-tcSyntaxName orig ty (std_nm, HsVar user_nm)
-  | std_nm == user_nm
-  = newMethodFromName orig ty std_nm   `thenM` \ id ->
-    returnM (std_nm, HsVar id)
-
-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)      $
-
-       -- 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 ->
-    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 (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}