[project @ 2005-04-04 11:55:11 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / Inst.lhs
index f568f4f..7cde236 100644 (file)
 \section[Inst]{The @Inst@ type: dictionaries or method instances}
 
 \begin{code}
-module Inst (
-       LIE, emptyLIE, unitLIE, plusLIE, consLIE, zonkLIE,
-       plusLIEs, mkLIE, isEmptyLIE,
+module Inst ( 
+       Inst, 
 
-       Inst, OverloadedLit(..),
-       pprInst, pprInsts, pprInstsInFull, tidyInst, tidyInsts,
+       pprDFuns, pprDictsTheta, pprDictsInFull,        -- User error messages
+       showLIE, pprInst, pprInsts, pprInstInFull,      -- Debugging messages
 
-        InstanceMapper,
+       tidyInsts, tidyMoreInsts,
 
-       newDictFromOld, newDicts, newDictsAtLoc, 
-       newMethod, newMethodWithGivenTy, newOverloadedLit,
+       newDicts, newDictAtLoc, newDictsAtLoc, cloneDict, 
+       tcOverloadedLit, newIPDict, 
+       newMethod, newMethodFromName, newMethodWithGivenTy, 
+       tcInstClassOp, tcInstCall, tcInstStupidTheta,
+       tcSyntaxName, 
 
-       tyVarsOfInst, instLoc, getDictClassTys,
+       tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
+       ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
+       instLoc, getDictClassTys, dictPred,
 
-       lookupInst, lookupSimpleInst, LookupInstResult(..),
+       lookupInst, LookupInstResult(..), lookupPred, 
+       tcExtendLocalInstEnv, tcGetInstEnvs, 
 
-       isDict, isTyVarDict, isStdClassTyVarDict, isMethodFor,
-       instBindingRequired, instCanBeGeneralised,
+       isDict, isClassDict, isMethod, 
+       isLinearInst, linearInstType, isIPDict, isInheritableInst,
+       isTyVarDict, isStdClassTyVarDict, isMethodFor, 
+       instBindingRequired,
 
-       zonkInst, instToId, instToIdBndr,
+       zonkInst, zonkInsts,
+       instToId, instName,
 
-       InstOrigin(..), pprOrigin
+       InstOrigin(..), InstLoc(..), pprInstLoc
     ) where
 
 #include "HsVersions.h"
 
-import HsSyn   ( HsLit(..), HsExpr(..) )
-import RnHsSyn ( RenamedArithSeqInfo, RenamedHsExpr, RenamedPat )
-import TcHsSyn ( TcExpr, TcId, 
-                 mkHsTyApp, mkHsDictApp, zonkId
-               )
-import TcMonad
-import TcEnv   ( TcIdSet, tcLookupValueByKey, tcLookupTyConByKey )
-import TcType  ( TcThetaType,
-                 TcType, TcTauType, TcTyVarSet,
-                 zonkTcType, zonkTcTypes, 
-                 zonkTcThetaType
-               )
-import Bag
-import Class   ( classInstEnv,
-                 Class, ClassInstEnv 
+import {-# SOURCE #-}  TcExpr( tcCheckSigma, tcSyntaxOp )
+import {-# SOURCE #-}  TcUnify ( unifyTauTy )  -- Used in checkKind (sigh)
+
+import HsSyn   ( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp,
+                 nlHsLit, nlHsVar )
+import TcHsSyn ( TcId, TcIdSet, 
+                 mkHsTyApp, mkHsDictApp, zonkId, 
+                 mkCoercion, ExprCoFn
                )
-import Id      ( Id, idFreeTyVars, idType, mkUserLocal, mkSysLocal )
-import VarSet  ( elemVarSet )
-import PrelInfo        ( isStandardClass, isCcallishClass, isNoDictClass )
-import Name    ( OccName, Name, mkDictOcc, getOccName )
-import PprType ( pprConstraint )       
-import SpecEnv ( SpecEnv, lookupSpecEnv )
-import SrcLoc  ( SrcLoc )
-import Type    ( Type, ThetaType, substTy,
-                 isTyVarTy, mkDictTy, splitForAllTys, splitSigmaTy,
-                 splitRhoTy, tyVarsOfType, tyVarsOfTypes,
-                 mkSynTy, substTopTy, substTopTheta,
-                 tidyOpenType, tidyOpenTypes
+import TcRnMonad
+import TcEnv   ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
+import InstEnv ( DFunId, InstEnv, lookupInstEnv, checkFunDeps, extendInstEnv )
+import TcIface ( loadImportedInsts )
+import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, zonkTcThetaType, 
+                 tcInstTyVar, tcInstType, tcSkolType
                )
-import TyCon   ( TyCon )
-import VarEnv  ( zipVarEnv, lookupVarEnv, TidyEnv )
-import VarSet  ( unionVarSet )
-import TysPrim   ( intPrimTy, floatPrimTy, doublePrimTy )
-import TysWiredIn ( intDataCon, isIntTy, inIntRange,
-                   floatDataCon, isFloatTy,
-                   doubleDataCon, isDoubleTy,
-                   integerTy, isIntegerTy
-                 ) 
-import Unique  ( fromRationalClassOpKey, rationalTyConKey,
-                 fromIntClassOpKey, fromIntegerClassOpKey, Unique
+import TcType  ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar, TcPredType,
+                 PredType(..), SkolemInfo(..), Expected(..), typeKind, mkSigmaTy,
+                 tcSplitForAllTys, tcSplitForAllTys, mkFunTy,
+                 tcSplitPhiTy, tcIsTyVarTy, tcSplitDFunTy, tcSplitDFunHead,
+                 isIntTy,isFloatTy, isIntegerTy, isDoubleTy,
+                 tcIsTyVarTy, mkPredTy, mkTyVarTy, mkTyVarTys,
+                 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred,
+                 isClassPred, isTyVarClassPred, isLinearPred, 
+                 getClassPredTys, getClassPredTys_maybe, mkPredName,
+                 isInheritablePred, isIPPred, 
+                 tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy, 
+                 pprPred, pprParendType, pprThetaArrow, pprTheta, pprClassPred
                )
-import Maybes  ( expectJust )
-import Util    ( thenCmp, zipWithEqual, mapAccumL )
+import Type    ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSubst,
+                 notElemTvSubst, extendTvSubstList )
+import Unify   ( tcMatchTys )
+import Kind    ( isSubKind )
+import Packages        ( isHomeModule )
+import HscTypes        ( ExternalPackageState(..) )
+import CoreFVs ( idFreeTyVars )
+import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName, dataConWrapId )
+import Id      ( Id, idName, idType, mkUserLocal, mkLocalId )
+import PrelInfo        ( isStandardClass, isNoDictClass )
+import Name    ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
+                 isInternalName, setNameUnique, mkSystemVarNameEncoded )
+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( DynFlags )
+import Maybes  ( isJust )
 import Outputable
 \end{code}
 
-%************************************************************************
-%*                                                                     *
-\subsection[Inst-collections]{LIE: a collection of Insts}
-%*                                                                     *
-%************************************************************************
 
+Selection
+~~~~~~~~~
 \begin{code}
-type LIE = Bag Inst
-
-isEmptyLIE       = isEmptyBag
-emptyLIE          = emptyBag
-unitLIE inst     = unitBag inst
-mkLIE insts      = listToBag insts
-plusLIE lie1 lie2 = lie1 `unionBags` lie2
-consLIE inst lie  = inst `consBag` lie
-plusLIEs lies    = unionManyBags lies
-
-zonkLIE :: LIE -> NF_TcM s LIE
-zonkLIE lie = mapBagNF_Tc zonkInst lie
-
-pprInsts :: [Inst] -> SDoc
-pprInsts insts = parens (hsep (punctuate comma (map pprInst insts)))
-
-
-pprInstsInFull insts
-  = vcat (map go insts)
-  where
-    go inst = quotes (ppr inst) <+> pprOrigin inst
-\end{code}
+instName :: Inst -> Name
+instName inst = idName (instToId inst)
 
-%************************************************************************
-%*                                                                     *
-\subsection[Inst-types]{@Inst@ types}
-%*                                                                     *
-%************************************************************************
+instToId :: Inst -> TcId
+instToId (LitInst nm _ ty _)   = mkLocalId nm ty
+instToId (Dict nm pred _)      = mkLocalId nm (mkPredTy pred)
+instToId (Method id _ _ _ _ _) = id
 
-An @Inst@ is either a dictionary, an instance of an overloaded
-literal, or an instance of an overloaded value.  We call the latter a
-``method'' even though it may not correspond to a class operation.
-For example, we might have an instance of the @double@ function at
-type Int, represented by
+instLoc (Dict _ _         loc) = loc
+instLoc (Method _ _ _ _ _ loc) = loc
+instLoc (LitInst _ _ _    loc) = loc
 
-       Method 34 doubleId [Int] origin
+dictPred (Dict _ pred _ ) = pred
+dictPred inst            = pprPanic "dictPred" (ppr inst)
 
-\begin{code}
-data Inst
-  = Dict
-       Unique
-       Class           -- The type of the dict is (c ts), where
-       [TcType]        -- c is the class and ts the types;
-       InstOrigin
-       SrcLoc
-
-  | Method
-       Unique
-
-       TcId    -- The overloaded function
-                       -- This function will be a global, local, or ClassOpId;
-                       --   inside instance decls (only) it can also be an InstId!
-                       -- The id needn't be completely polymorphic.
-                       -- You'll probably find its name (for documentation purposes)
-                       --        inside the InstOrigin
-
-       [TcType]        -- The types to which its polymorphic tyvars
-                       --      should be instantiated.
-                       -- These types must saturate the Id's foralls.
-
-       TcThetaType     -- The (types of the) dictionaries to which the function
-                       -- must be applied to get the method
-
-       TcTauType       -- The type of the method
-
-       InstOrigin
-       SrcLoc
-
-       -- INVARIANT: in (Method u f tys theta tau loc)
-       --      type of (f tys dicts(from theta)) = tau
-
-  | LitInst
-       Unique
-       OverloadedLit
-       TcType          -- The type at which the literal is used
-       InstOrigin      -- Always a literal; but more convenient to carry this around
-       SrcLoc
-
-data OverloadedLit
-  = OverloadedIntegral  Integer        -- The number
-  | OverloadedFractional Rational      -- The number
-\end{code}
+getDictClassTys (Dict _ pred _) = getClassPredTys pred
 
-Ordering
-~~~~~~~~
-@Insts@ are ordered by their class/type info, rather than by their
-unique.  This allows the context-reduction mechanism to use standard finite
-maps to do their stuff.
+-- 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
 
-\begin{code}
-instance Ord Inst where
-  compare = cmpInst
-
-instance Eq Inst where
-  (==) i1 i2 = case i1 `cmpInst` i2 of
-                EQ    -> True
-                other -> False
-
-cmpInst  (Dict _ clas1 tys1 _ _) (Dict _ clas2 tys2 _ _)
-  = (clas1 `compare` clas2) `thenCmp` (tys1 `compare` tys2)
-cmpInst (Dict _ _ _ _ _) other
-  = LT
-
-
-cmpInst (Method _ _ _ _ _ _ _) (Dict _ _ _ _ _)
-  = GT
-cmpInst (Method _ id1 tys1 _ _ _ _) (Method _ id2 tys2 _ _ _ _)
-  = (id1 `compare` id2) `thenCmp` (tys1 `compare` tys2)
-cmpInst (Method _ _ _ _ _ _ _) other
-  = LT
-
-cmpInst (LitInst _ lit1 ty1 _ _) (LitInst _ lit2 ty2 _ _)
-  = (lit1 `cmpOverLit` lit2) `thenCmp` (ty1 `compare` ty2)
-cmpInst (LitInst _ _ _ _ _) other
-  = GT
-
-cmpOverLit (OverloadedIntegral   i1) (OverloadedIntegral   i2) = i1 `compare` i2
-cmpOverLit (OverloadedFractional f1) (OverloadedFractional f2) = f1 `compare` f2
-cmpOverLit (OverloadedIntegral _)    (OverloadedFractional _)  = LT
-cmpOverLit (OverloadedFractional _)  (OverloadedIntegral _)    = GT
-\end{code}
+fdPredsOfInsts :: [Inst] -> [PredType]
+fdPredsOfInsts insts = concatMap fdPredsOfInst insts
 
+isInheritableInst (Dict _ pred _)         = isInheritablePred pred
+isInheritableInst (Method _ _ _ theta _ _) = all isInheritablePred theta
+isInheritableInst other                           = True
 
-Selection
-~~~~~~~~~
-\begin{code}
-instOrigin (Dict   u clas tys    origin loc) = origin
-instOrigin (Method u clas ty _ _ origin loc) = origin
-instOrigin (LitInst u lit ty     origin loc) = origin
 
-instLoc (Dict   u clas tys    origin loc) = loc
-instLoc (Method u clas ty _ _ origin loc) = loc
-instLoc (LitInst u lit ty     origin loc) = loc
+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]
 
-getDictClassTys (Dict u clas tys _ _) = (clas, tys)
+ipNamesOfInst (Dict _ (IParam n _) _)  = [ipNameName n]
+ipNamesOfInst (Method _ _ _ theta _ _) = [ipNameName n | IParam n _ <- theta]
+ipNamesOfInst other                   = []
 
 tyVarsOfInst :: Inst -> TcTyVarSet
-tyVarsOfInst (Dict _ _ tys _ _)        = tyVarsOfTypes  tys
-tyVarsOfInst (Method _ id tys _ _ _ _) = tyVarsOfTypes tys `unionVarSet` idFreeTyVars id
+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
-tyVarsOfInst (LitInst _ _ ty _ _)     = tyVarsOfType  ty
+
+
+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
+isDict (Dict _ _ _) = True
+isDict other       = False
 
-isMethodFor :: TcIdSet -> Inst -> Bool
-isMethodFor ids (Method uniq id tys _ _ orig loc) 
-  = id `elemVarSet` ids
-isMethodFor ids inst 
-  = False
+isClassDict :: Inst -> Bool
+isClassDict (Dict _ pred _) = isClassPred pred
+isClassDict other          = False
 
 isTyVarDict :: Inst -> Bool
-isTyVarDict (Dict _ _ tys _ _) = all isTyVarTy tys
-isTyVarDict other             = False
+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
 
-isStdClassTyVarDict (Dict _ clas [ty] _ _) = isStandardClass clas && isTyVarTy ty
-isStdClassTyVarDict 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
+
+
+isStdClassTyVarDict (Dict _ pred _) = case getClassPredTys_maybe pred of
+                                       Just (clas, [ty]) -> isStandardClass clas && tcIsTyVarTy ty
+                                       other             -> False
 \end{code}
 
 Two predicates which deal with the case where class constraints don't
@@ -255,166 +206,284 @@ must be witnessed by an actual binding; the second tells whether an
 
 \begin{code}
 instBindingRequired :: Inst -> Bool
-instBindingRequired (Dict _ clas _ _ _) = not (isNoDictClass clas)
-instBindingRequired other              = True
-
-instCanBeGeneralised :: Inst -> Bool
-instCanBeGeneralised (Dict _ clas _ _ _) = not (isCcallishClass clas)
-instCanBeGeneralised other              = True
+instBindingRequired (Dict _ (ClassP clas _) _) = not (isNoDictClass clas)
+instBindingRequired other                     = True
 \end{code}
 
 
-Construction
-~~~~~~~~~~~~
+%************************************************************************
+%*                                                                     *
+\subsection{Building dictionaries}
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
 newDicts :: InstOrigin
         -> TcThetaType
-        -> NF_TcM s (LIE, [TcId])
+        -> TcM [Inst]
 newDicts orig theta
-  = tcGetSrcLoc                                `thenNF_Tc` \ loc ->
-    newDictsAtLoc orig loc theta        `thenNF_Tc` \ (dicts, ids) ->
-    returnNF_Tc (listToBag dicts, ids)
-
--- Local function, similar to newDicts, 
--- but with slightly different interface
-newDictsAtLoc :: InstOrigin
-              -> SrcLoc
-             -> TcThetaType
-             -> NF_TcM s ([Inst], [TcId])
-newDictsAtLoc orig loc theta =
- tcGetUniques (length theta)           `thenNF_Tc` \ new_uniqs ->
- let
-  mk_dict u (clas, tys) = Dict u clas tys orig loc
-  dicts = zipWithEqual "newDictsAtLoc" mk_dict new_uniqs theta
- in
- returnNF_Tc (dicts, map instToId dicts)
-
-newDictFromOld :: Inst -> Class -> [TcType] -> NF_TcM s Inst
-newDictFromOld (Dict _ _ _ orig loc) clas tys
-  = tcGetUnique              `thenNF_Tc` \ uniq ->
-    returnNF_Tc (Dict uniq clas tys orig loc)
-
-
-newMethod :: InstOrigin
-         -> TcId
-         -> [TcType]
-         -> NF_TcM s (LIE, TcId)
-newMethod orig id tys
-  =    -- Get the Id type and instantiate it at the specified types
+  = 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
-       (tyvars, rho) = splitForAllTys (idType id)
-       rho_ty        = substTy (zipVarEnv tyvars tys) rho
-       (theta, tau) = splitRhoTy rho_ty
+       pred = IParam ip_name ty
+        name = mkPredName uniq (instLocSrcLoc inst_loc) pred 
+       dict = Dict name pred inst_loc
     in
-    newMethodWithGivenTy orig id tys theta tau `thenNF_Tc` \ meth_inst ->
-    returnNF_Tc (unitLIE meth_inst, instToId meth_inst)
+    returnM (mapIPName (\n -> instToId dict) ip_name, dict)
+\end{code}
+
 
 
+%************************************************************************
+%*                                                                     *
+\subsection{Building methods (calls of overloaded functions)}
+%*                                                                     *
+%************************************************************************
+
+
+\begin{code}
+tcInstCall :: InstOrigin -> TcType -> TcM (ExprCoFn, [TcTyVar], TcType)
+tcInstCall orig fun_ty -- fun_ty is usually a sigma-type
+  = do { (tyvars, theta, tau) <- tcInstType fun_ty
+       ; dicts <- newDicts orig theta
+       ; extendLIEs dicts
+       ; let inst_fn e = unLoc (mkHsDictApp (mkHsTyApp (noLoc e) (mkTyVarTys tyvars)) 
+                                            (map instToId dicts))
+       ; return (mkCoercion inst_fn, tyvars, tau) }
+
+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 ()
+  | 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 -> TcType -> 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 theta tau
-  = tcGetSrcLoc                `thenNF_Tc` \ loc ->
-    tcGetUnique                `thenNF_Tc` \ new_uniq ->
-    let
-       meth_inst = Method new_uniq id tys theta tau orig loc
+  = getInstLoc orig                    `thenM` \ loc ->
+    newMethod loc id tys theta tau     `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)
+       rho_ty       = ASSERT( length tyvars == length tys )
+                      substTyWith tyvars tys rho
+       (preds,tau)  = tcSplitPhiTy rho_ty
     in
-    returnNF_Tc meth_inst
-
-newMethodAtLoc :: InstOrigin -> SrcLoc
-              -> Id -> [TcType]
-              -> NF_TcM s (Inst, TcId)
-newMethodAtLoc orig loc real_id tys    -- Local function, similar to newMethod but with 
-                                       -- slightly different interface
-  =    -- Get the Id type and instantiate it at the specified types
-    tcGetUnique                                        `thenNF_Tc` \ new_uniq ->
+    zipWithM_ checkKind tyvars tys     `thenM_` 
+    newMethod inst_loc sel_id tys preds tau
+
+checkKind :: TyVar -> TcType -> TcM ()
+-- Ensure that the type has a sub-kind of the tyvar
+checkKind tv ty
+  = do { ty1 <- zonkTcType ty
+       ; if typeKind ty1 `isSubKind` tyVarKind tv
+         then return ()
+         else do
+       { traceTc (text "checkKind: adding kind constraint" <+> ppr tv <+> ppr ty)
+       ; tv1 <- tcInstTyVar tv
+       ; unifyTauTy (mkTyVarTy tv1) ty1 }}
+
+
+---------------------------
+newMethod inst_loc id tys theta tau
+  = newUnique          `thenM` \ new_uniq ->
     let
-       (tyvars,rho) = splitForAllTys (idType real_id)
-       rho_ty        = ASSERT( length tyvars == length tys )
-                       substTopTy (zipVarEnv tyvars tys) rho
-       (theta, tau)  = splitRhoTy rho_ty
-       meth_inst     = Method new_uniq real_id tys theta tau orig loc
+       meth_id = mkUserLocal (mkMethodOcc (getOccName id)) new_uniq tau loc
+       inst    = Method meth_id id tys theta tau inst_loc
+       loc     = instLocSrcLoc inst_loc
     in
-    returnNF_Tc (meth_inst, instToId meth_inst)
+    returnM inst
 \end{code}
 
-In newOverloadedLit we convert directly to an Int or Integer if we
+In tcOverloadedLit 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}
-newOverloadedLit :: InstOrigin
-                -> OverloadedLit
+tcOverloadedLit :: InstOrigin
+                -> HsOverLit Name
                 -> TcType
-                -> NF_TcM s (TcExpr, LIE)
-newOverloadedLit orig (OverloadedIntegral i) ty
-  | isIntTy ty && inIntRange i         -- Short cut for Int
-  = returnNF_Tc (int_lit, emptyLIE)
-
+                -> TcM (HsOverLit TcId)
+tcOverloadedLit orig lit@(HsIntegral i fi) expected_ty
+  | fi `isHsVar` fromIntegerName       -- 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
+       -- ToDo: noLoc sadness
+  = do { integer_ty <- tcMetaTy integerTyConName
+       ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty expected_ty)
+       ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
+
+  | Just expr <- shortCutIntLit i expected_ty 
+  = return (HsIntegral i expr)
+
+  | otherwise
+  = do         { expr <- newLitInst orig lit expected_ty
+       ; return (HsIntegral i expr) }
+
+tcOverloadedLit orig lit@(HsFractional r fr) expected_ty
+  | fr `isHsVar` fromRationalName      -- c.f. HsIntegral case
+  = do { rat_ty <- tcMetaTy rationalTyConName
+       ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty expected_ty)
+       ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
+
+  | Just expr <- shortCutFracLit r expected_ty 
+  = return (HsFractional r expr)
+
+  | otherwise
+  = do         { expr <- newLitInst orig lit expected_ty
+       ; return (HsFractional r expr) }
+
+newLitInst :: InstOrigin -> HsOverLit Name -> TcType -> TcM (HsExpr TcId)
+newLitInst orig lit expected_ty        -- Make a LitInst
+  = do         { loc <- getInstLoc orig
+       ; new_uniq <- newUnique
+       ; let
+               lit_nm   = mkSystemVarNameEncoded new_uniq FSLIT("lit")
+               -- The "encoded" bit means that we don't need to
+               -- z-encode the string every time we call this!
+               lit_inst = LitInst lit_nm lit expected_ty loc
+       ; extendLIE lit_inst
+       ; return (HsVar (instToId lit_inst)) }
+
+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
-  = returnNF_Tc (integer_lit, emptyLIE)
-
+  = 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
-    intprim_lit    = HsLitOut (HsIntPrim i) intPrimTy
-    integer_lit    = HsLitOut (HsInt i) integerTy
-    int_lit        = HsCon intDataCon [] [intprim_lit]
-
-newOverloadedLit orig lit ty           -- The general case
-  = tcGetSrcLoc                        `thenNF_Tc` \ loc ->
-    tcGetUnique                        `thenNF_Tc` \ new_uniq ->
-    let
-       lit_inst = LitInst new_uniq lit ty orig loc
-    in
-    returnNF_Tc (HsVar (instToId lit_inst), unitLIE lit_inst)
+    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}
 
 
-\begin{code}
-instToId :: Inst -> TcId
-instToId inst = instToIdBndr inst
-
-instToIdBndr :: Inst -> TcId
-instToIdBndr (Dict u clas ty orig loc)
-  = mkUserLocal (mkDictOcc (getOccName clas)) u (mkDictTy clas ty)
-
-instToIdBndr (Method u id tys theta tau orig loc)
-  = mkUserLocal (getOccName id) u tau
-    
-instToIdBndr (LitInst u list ty orig loc)
-  = mkSysLocal SLIT("lit") u ty
-\end{code}
-
+%************************************************************************
+%*                                                                     *
+\subsection{Zonking}
+%*                                                                     *
+%************************************************************************
 
-Zonking
-~~~~~~~
-Zonking makes sure that the instance types are fully zonked,
-but doesn't do the same for the Id in a Method.  There's no
-need, and it's a lot of extra work.
+Zonking makes sure that the instance types are fully zonked.
 
 \begin{code}
-zonkInst :: Inst -> NF_TcM s Inst
-zonkInst (Dict u clas tys orig loc)
-  = zonkTcTypes        tys                     `thenNF_Tc` \ new_tys ->
-    returnNF_Tc (Dict u clas new_tys orig loc)
+zonkInst :: Inst -> TcM Inst
+zonkInst (Dict name pred loc)
+  = zonkTcPredType pred                        `thenM` \ new_pred ->
+    returnM (Dict name new_pred loc)
 
-zonkInst (Method u id tys theta tau orig loc) 
-  = zonkId id                  `thenNF_Tc` \ new_id ->
+zonkInst (Method m id tys theta tau 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            `thenNF_Tc` \ new_tys ->
-    zonkTcThetaType theta      `thenNF_Tc` \ new_theta ->
-    zonkTcType tau             `thenNF_Tc` \ new_tau ->
-    returnNF_Tc (Method u new_id new_tys new_theta new_tau orig loc)
+    zonkTcTypes tys            `thenM` \ new_tys ->
+    zonkTcThetaType theta      `thenM` \ new_theta ->
+    zonkTcType tau             `thenM` \ new_tau ->
+    returnM (Method m new_id new_tys new_theta new_tau loc)
+
+zonkInst (LitInst nm lit ty loc)
+  = zonkTcType ty                      `thenM` \ new_ty ->
+    returnM (LitInst nm lit new_ty loc)
 
-zonkInst (LitInst u lit ty orig loc)
-  = zonkTcType ty                      `thenNF_Tc` \ new_ty ->
-    returnNF_Tc (LitInst u lit new_ty orig loc)
+zonkInsts insts = mappM zonkInst insts
 \end{code}
 
 
-Printing
-~~~~~~~~
+%************************************************************************
+%*                                                                     *
+\subsection{Printing}
+%*                                                                     *
+%************************************************************************
+
 ToDo: improve these pretty-printing things.  The ``origin'' is really only
 relevant in error messages.
 
@@ -422,286 +491,369 @@ relevant in error messages.
 instance Outputable Inst where
     ppr inst = pprInst inst
 
-pprInst (LitInst u lit ty orig loc)
-  = hsep [case lit of
-             OverloadedIntegral   i -> integer i
-             OverloadedFractional f -> rational f,
-          ptext SLIT("at"),
-          ppr ty,
-          show_uniq u]
-
-pprInst (Dict u clas tys orig loc) = pprConstraint clas tys <+> show_uniq u
+pprDictsTheta :: [Inst] -> SDoc
+-- Print in type-like fashion (Eq a, Show b)
+pprDictsTheta dicts = pprTheta (map dictPred dicts)
 
-pprInst (Method u id tys _ _ orig loc)
-  = hsep [ppr id, ptext SLIT("at"), 
-         brackets (interppSP tys),
-         show_uniq u]
-
-tidyInst :: TidyEnv -> Inst -> (TidyEnv, Inst)
-tidyInst env (LitInst u lit ty orig loc)
-  = (env', LitInst u lit ty' orig loc)
+pprDictsInFull :: [Inst] -> SDoc
+-- Print in type-like fashion, but with source location
+pprDictsInFull dicts 
+  = vcat (map go dicts)
   where
-    (env', ty') = tidyOpenType env ty
+    go dict = sep [quotes (ppr (dictPred dict)), nest 2 (pprInstLoc (instLoc dict))]
 
-tidyInst env (Dict u clas tys orig loc)
-  = (env', Dict u clas tys' orig loc)
+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 tau 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))]
+
+pprDFuns :: [DFunId] -> SDoc
+-- Prints the dfun as an instance declaration
+pprDFuns dfuns = vcat [ hang (ppr (getSrcLoc dfun) <> colon)
+                       2 (ptext SLIT("instance") <+> sep [pprThetaArrow theta,
+                                                          pprClassPred clas tys])
+                     | dfun <- dfuns
+                     , let (_, theta, clas, tys) = tcSplitDFunTy (idType dfun) ]
+       -- Print without the for-all, which the programmer doesn't write
+
+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 tau loc) = Method u id (tidyTypes env tys) theta tau 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', tys') = tidyOpenTypes env tys
+    env' = tidyFreeTyVars env (tyVarsOfInsts insts)
 
-tidyInst env (Method u id tys theta tau orig loc)
-  = (env', Method u id tys' theta tau orig loc)
-               -- Leave theta, tau alone cos we don't print them
-  where
-    (env', tys') = tidyOpenTypes env tys
-    
-tidyInsts env insts = mapAccumL tidyInst env insts
+tidyInsts :: [Inst] -> (TidyEnv, [Inst])
+tidyInsts insts = tidyMoreInsts emptyTidyEnv insts
 
-show_uniq u = ifPprDebug (text "{-" <> ppr u <> text "-}")
+showLIE :: SDoc -> TcM ()      -- Debugging
+showLIE str
+  = do { lie_var <- getLIEVar ;
+        lie <- readMutVar lie_var ;
+        traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) }
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[InstEnv-types]{Type declarations}
+       Extending the instance environment
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-type InstanceMapper = Class -> ClassInstEnv
+tcExtendLocalInstEnv :: [DFunId] -> TcM a -> TcM a
+  -- Add new locally-defined instances
+tcExtendLocalInstEnv dfuns thing_inside
+ = do { traceDFuns dfuns
+      ; env <- getGblEnv
+      ; dflags  <- getDOpts
+      ; inst_env' <- foldlM (addInst dflags) (tcg_inst_env env) dfuns
+      ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
+                        tcg_inst_env = inst_env' }
+      ; setGblEnv env' thing_inside }
+
+addInst :: DynFlags -> InstEnv -> DFunId -> TcM InstEnv
+-- Check that the proposed new instance is OK, 
+-- and then add it to the home inst env
+addInst dflags home_ie dfun
+  = do {       -- Instantiate the dfun type so that we extend the instance
+               -- envt with completely fresh template variables
+               -- This is important because the template variables must
+               -- not overlap with anything in the things being looked up
+               -- (since we do unification).  
+               -- We use tcSkolType because we don't want to allocate fresh
+               --  *meta* type variables.  
+         (tvs', theta', tau') <- tcSkolType (InstSkol dfun) (idType dfun)
+       ; let   (cls, tys') = tcSplitDFunHead tau'
+               dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
+
+               -- Load imported instances, so that we report
+               -- duplicates correctly
+       ; pkg_ie  <- loadImportedInsts cls tys'
+
+               -- Check functional dependencies
+       ; case checkFunDeps (pkg_ie, home_ie) dfun' of
+               Just dfuns -> funDepErr dfun dfuns
+               Nothing    -> return ()
+
+               -- Check for duplicate instance decls
+       ; let { (matches, _) = lookupInstEnv dflags (pkg_ie, home_ie) cls tys'
+             ; dup_dfuns = [dup_dfun | (_, (_, dup_tys, dup_dfun)) <- matches,
+                                       isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
+               -- Find memebers of the match list which 
+               -- dfun itself matches. If the match is 2-way, it's a duplicate
+       ; case dup_dfuns of
+           dup_dfun : _ -> dupInstErr dfun dup_dfun
+           []           -> return ()
+
+               -- OK, now extend the envt
+       ; return (extendInstEnv home_ie dfun') }
+
+
+traceDFuns dfuns
+  = traceTc (text "Adding instances:" <+> vcat (map pp dfuns))
+  where
+    pp dfun = ppr dfun <+> dcolon <+> ppr (idType dfun)
+
+funDepErr dfun dfuns
+  = addDictLoc dfun $
+    addErr (hang (ptext SLIT("Functional dependencies conflict between instance declarations:"))
+              2 (pprDFuns (dfun:dfuns)))
+dupInstErr dfun dup_dfun
+  = addDictLoc dfun $
+    addErr (hang (ptext SLIT("Duplicate instance declarations:"))
+              2 (pprDFuns [dfun, dup_dfun]))
+
+addDictLoc dfun thing_inside
+  = setSrcSpan (mkSrcSpan loc loc) thing_inside
+  where
+   loc = getSrcLoc dfun
 \end{code}
+    
 
-A @ClassInstEnv@ lives inside a class, and identifies all the instances
-of that class.  The @Id@ inside a ClassInstEnv mapping is the dfun for
-that instance.  
-
-There is an important consistency constraint between the @MatchEnv@s
-in and the dfun @Id@s inside them: the free type variables of the
-@Type@ key in the @MatchEnv@ must be a subset of the universally-quantified
-type variables of the dfun.  Thus, the @ClassInstEnv@ for @Eq@ might
-contain the following entry:
-@
-       [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
-@
-The "a" in the pattern must be one of the forall'd variables in
-the dfun type.
+%************************************************************************
+%*                                                                     *
+\subsection{Looking up Insts}
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
-data LookupInstResult s
+data LookupInstResult
   = NoInstance
-  | SimpleInst TcExpr          -- Just a variable, type application, or literal
-  | GenInst    [Inst] TcExpr   -- The expression and its needed insts
-
-lookupInst :: Inst 
-          -> NF_TcM s (LookupInstResult s)
+  | SimpleInst (LHsExpr TcId)          -- Just a variable, type application, or literal
+  | GenInst    [Inst] (LHsExpr TcId)   -- The expression and its needed insts
 
--- Dictionaries
+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
 
-lookupInst dict@(Dict _ clas tys orig loc)
-  = case lookupSpecEnv (ppr clas) (classInstEnv clas) tys of
-
-      Just (tenv, dfun_id)
-       -> let
-               (tyvars, rho) = splitForAllTys (idType dfun_id)
-               ty_args       = map (expectJust "Inst" . lookupVarEnv tenv) tyvars
-                               -- tenv should bind all the tyvars
-               dfun_rho      = substTopTy tenv rho
-               (theta, tau)  = splitRhoTy dfun_rho
-               ty_app        = mkHsTyApp (HsVar dfun_id) ty_args
-          in
-          if null theta then
-               returnNF_Tc (SimpleInst ty_app)
-          else
-          newDictsAtLoc orig loc theta `thenNF_Tc` \ (dicts, dict_ids) ->
-          let 
-               rhs = mkHsDictApp ty_app dict_ids
-          in
-          returnNF_Tc (GenInst dicts rhs)
-                            
-      Nothing  -> returnNF_Tc NoInstance
 
 -- Methods
 
-lookupInst inst@(Method _ id tys theta _ orig loc)
-  = newDictsAtLoc orig loc theta       `thenNF_Tc` \ (dicts, dict_ids) ->
-    returnNF_Tc (GenInst dicts (mkHsDictApp (mkHsTyApp (HsVar id) tys) dict_ids))
-
--- Literals
-
-lookupInst inst@(LitInst u (OverloadedIntegral i) ty orig loc)
-  | isIntTy ty && in_int_range                 -- Short cut for Int
-  = returnNF_Tc (GenInst [] int_lit)
-       -- GenInst, not SimpleInst, because int_lit is actually a constructor application
-
-  | isIntegerTy ty                             -- Short cut for Integer
-  = returnNF_Tc (GenInst [] integer_lit)
-
-  | in_int_range                               -- It's overloaded but small enough to fit into an Int
-  = tcLookupValueByKey fromIntClassOpKey       `thenNF_Tc` \ from_int ->
-    newMethodAtLoc orig loc from_int [ty]      `thenNF_Tc` \ (method_inst, method_id) ->
-    returnNF_Tc (GenInst [method_inst] (HsApp (HsVar method_id) int_lit))
-
-  | otherwise                                  -- Alas, it is overloaded and a big literal!
-  = tcLookupValueByKey fromIntegerClassOpKey   `thenNF_Tc` \ from_integer ->
-    newMethodAtLoc orig loc from_integer [ty]          `thenNF_Tc` \ (method_inst, method_id) ->
-    returnNF_Tc (GenInst [method_inst] (HsApp (HsVar method_id) integer_lit))
+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)))
   where
-    in_int_range   = inIntRange i
-    intprim_lit    = HsLitOut (HsIntPrim i) intPrimTy
-    integer_lit    = HsLitOut (HsInt i) integerTy
-    int_lit        = HsCon intDataCon [] [intprim_lit]
-
--- similar idea for overloaded floating point literals: if the literal is
--- *definitely* a float or a double, generate the real thing here.
--- This is essential  (see nofib/spectral/nucleic).
-
-lookupInst inst@(LitInst u (OverloadedFractional f) ty orig loc)
-  | isFloatTy ty    = returnNF_Tc (GenInst [] float_lit)
-  | isDoubleTy ty   = returnNF_Tc (GenInst [] double_lit)
-
-  | otherwise 
-         = tcLookupValueByKey fromRationalClassOpKey   `thenNF_Tc` \ from_rational ->
-
-       -- The type Rational isn't wired in so we have to conjure it up
-    tcLookupTyConByKey rationalTyConKey        `thenNF_Tc` \ rational_tycon ->
-    let
-       rational_ty  = mkSynTy rational_tycon []
-       rational_lit = HsLitOut (HsFrac f) rational_ty
-    in
-    newMethodAtLoc orig loc from_rational [ty]         `thenNF_Tc` \ (method_inst, method_id) ->
-    returnNF_Tc (GenInst [method_inst] (HsApp (HsVar method_id) rational_lit))
+    span = instLocSrcSpan loc
 
-  where
-    floatprim_lit  = HsLitOut (HsFloatPrim f) floatPrimTy
-    float_lit      = HsCon floatDataCon [] [floatprim_lit]
-    doubleprim_lit = HsLitOut (HsDoublePrim f) doublePrimTy
-    double_lit     = HsCon doubleDataCon [] [doubleprim_lit]
-
-\end{code}
+-- Literals
 
-There is a second, simpler interface, when you want an instance of a
-class at a given nullary type constructor.  It just returns the
-appropriate dictionary if it exists.  It is used only when resolving
-ambiguous dictionaries.
+-- 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))
 
-\begin{code}
-lookupSimpleInst :: ClassInstEnv
-                -> Class
-                -> [Type]                      -- Look up (c,t)
-                -> NF_TcM s (Maybe ThetaType)          -- Here are the needed (c,t)s
-
-lookupSimpleInst class_inst_env clas tys
-  = case lookupSpecEnv (ppr clas) class_inst_env tys of
-      Nothing   -> returnNF_Tc Nothing
-
-      Just (tenv, dfun)
-       -> returnNF_Tc (Just (substTopTheta tenv theta))
-        where
-          (_, theta, _) = splitSigmaTy (idType dfun)
+-- 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 { pkg_ie <- loadImportedInsts clas tys
+               -- Suck in any instance decls that may be relevant
+       ; tcg_env <- getGblEnv
+       ; dflags  <- getDOpts
+       ; case lookupInstEnv dflags (pkg_ie, tcg_inst_env tcg_env) clas tys of {
+           ([(tenv, (_,_,dfun_id))], []) 
+               -> do   { 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 { dflags <- getDOpts
+       ; let  dfun_name = idName dfun_id
+              dfun_mod  = nameModule dfun_name
+       ; if isInternalName dfun_name || not (isHomeModule dflags dfun_mod)
+         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}
 
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-origin]{The @InstOrigin@ type}
+               Re-mappable syntax
 %*                                                                     *
 %************************************************************************
 
-The @InstOrigin@ type gives information about where a dictionary came from.
-This is important for decent error message reporting because dictionaries
-don't appear in the original source code.  Doubtless this type will evolve...
-
-\begin{code}
-data InstOrigin
-  = OccurrenceOf TcId  -- Occurrence of an overloaded identifier
-  | OccurrenceOfCon Id         -- Occurrence of a data constructor
+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:
 
-  | RecordUpdOrigin
+  (>>) :: HB m n mn => m a -> n b -> mn b
 
-  | DataDeclOrigin             -- Typechecking a data declaration
+So the idea is to generate a local binding for (>>), thus:
 
-  | InstanceDeclOrigin         -- Typechecking an instance decl
+       let then72 :: forall a b. m a -> m b -> m b
+           then72 = ...something involving the user's (>>)...
+       in
+       ...the do-expression...
 
-  | LiteralOrigin      HsLit   -- Occurrence of a literal
+Now the do-expression can proceed using then72, which has exactly
+the expected type.
 
-  | PatOrigin RenamedPat
+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.
 
-  | ArithSeqOrigin     RenamedArithSeqInfo -- [x..], [x..y] etc
-
-  | SignatureOrigin            -- A dict created from a type signature
-  | Rank2Origin                        -- A dict created when typechecking the argument
-                               -- of a rank-2 typed function
-
-  | DoOrigin                   -- The monad for a do expression
-
-  | ClassDeclOrigin            -- Manufactured during a class decl
-
-  | InstanceSpecOrigin Class   -- in a SPECIALIZE instance pragma
-                       Type
-
-       -- When specialising instances the instance info attached to
-       -- each class is not yet ready, so we record it inside the
-       -- origin information.  This is a bit of a hack, but it works
-       -- fine.  (Patrick is to blame [WDP].)
-
-  | ValSpecOrigin      Name    -- in a SPECIALIZE pragma for a value
-
-       -- Argument or result of a ccall
-       -- Dictionaries with this origin aren't actually mentioned in the
-       -- translated term, and so need not be bound.  Nor should they
-       -- be abstracted over.
-
-  | CCallOrigin                String                  -- CCall label
-                       (Maybe RenamedHsExpr)   -- Nothing if it's the result
-                                               -- Just arg, for an argument
-
-  | LitLitOrigin       String  -- the litlit
+\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)      $
 
-  | UnknownOrigin      -- Help! I give up...
-\end{code}
+       -- 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 -> 
+    tcCheckSigma (L span user_nm_expr) sigma1  `thenM` \ expr ->
+    returnM (std_nm, unLoc expr)
 
-\begin{code}
-pprOrigin :: Inst -> SDoc
-pprOrigin inst
-  = hsep [text "arising from", pp_orig orig, text "at", ppr locn]
-  where
-    (orig, locn) = case inst of
-                       Dict _ _ _       orig loc -> (orig,loc)
-                       Method _ _ _ _ _ orig loc -> (orig,loc)
-                       LitInst _ _ _    orig loc -> (orig,loc)
-                       
-    pp_orig (OccurrenceOf id)
-       = hsep [ptext SLIT("use of"), quotes (ppr id)]
-    pp_orig (OccurrenceOfCon id)
-       = hsep [ptext SLIT("use of"), quotes (ppr id)]
-    pp_orig (LiteralOrigin lit)
-       = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
-    pp_orig (PatOrigin pat)
-       = hsep [ptext SLIT("the pattern"), quotes (ppr pat)]
-    pp_orig (InstanceDeclOrigin)
-       =  ptext SLIT("an instance declaration")
-    pp_orig (ArithSeqOrigin seq)
-       = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
-    pp_orig (SignatureOrigin)
-       =  ptext SLIT("a type signature")
-    pp_orig (Rank2Origin)
-       =  ptext SLIT("a function with an overloaded argument type")
-    pp_orig (DoOrigin)
-       =  ptext SLIT("a do statement")
-    pp_orig (ClassDeclOrigin)
-       =  ptext SLIT("a class declaration")
-    pp_orig (InstanceSpecOrigin clas ty)
-       = hsep [text "a SPECIALIZE instance pragma; class",
-               quotes (ppr clas), text "type:", ppr ty]
-    pp_orig (ValSpecOrigin name)
-       = hsep [ptext SLIT("a SPECIALIZE user-pragma for"), quotes (ppr name)]
-    pp_orig (CCallOrigin clabel Nothing{-ccall result-})
-       = hsep [ptext SLIT("the result of the _ccall_ to"), quotes (text clabel)]
-    pp_orig (CCallOrigin clabel (Just arg_expr))
-       = hsep [ptext SLIT("an argument in the _ccall_ to"), quotes (text clabel) <> comma, 
-               text "namely", quotes (ppr arg_expr)]
-    pp_orig (LitLitOrigin s)
-       = hsep [ptext SLIT("the ``literal-literal''"), quotes (text s)]
-    pp_orig (UnknownOrigin)
-       = ptext SLIT("...oops -- I don't know where the overloading came from!")
+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)
 \end{code}