[project @ 2006-01-18 12:15:37 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / Inst.lhs
index 19c484f..b270a59 100644 (file)
@@ -5,28 +5,29 @@
 
 \begin{code}
 module Inst ( 
-       LIE, emptyLIE, unitLIE, plusLIE, consLIE, 
-       plusLIEs, mkLIE, isEmptyLIE, lieToList, listToLIE,
-       showLIE,
-
        Inst, 
-       pprInst, pprInsts, pprInstsInFull, tidyInsts, tidyMoreInsts,
 
-       newDictsFromOld, newDicts, cloneDict, 
-       newOverloadedLit, newIPDict, 
+       pprInstances, pprDictsTheta, pprDictsInFull,    -- User error messages
+       showLIE, pprInst, pprInsts, pprInstInFull,      -- Debugging messages
+
+       tidyInsts, tidyMoreInsts,
+
+       newDicts, newDictAtLoc, newDictsAtLoc, cloneDict, 
+       tcOverloadedLit, newIPDict, 
        newMethod, newMethodFromName, newMethodWithGivenTy, 
-       tcInstClassOp, tcInstCall, tcInstDataCon, tcSyntaxName,
+       tcInstClassOp, tcInstCall, tcInstStupidTheta,
+       tcSyntaxName, 
 
        tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
        ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
        instLoc, getDictClassTys, dictPred,
 
-       lookupInst, LookupInstResult(..),
+       lookupInst, LookupInstResult(..), lookupPred, 
+       tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
 
        isDict, isClassDict, isMethod, 
        isLinearInst, linearInstType, isIPDict, isInheritableInst,
-       isTyVarDict, isStdClassTyVarDict, isMethodFor, 
-       instBindingRequired, instCanBeGeneralised,
+       isTyVarDict, isMethodFor, 
 
        zonkInst, zonkInsts,
        instToId, instName,
@@ -36,46 +37,59 @@ module Inst (
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-}  TcExpr( tcCheckSigma )
+import {-# SOURCE #-}  TcExpr( tcCheckSigma, tcSyntaxOp )
+import {-# SOURCE #-}  TcUnify ( unifyTauTy )  -- Used in checkKind (sigh)
 
-import HsSyn   ( HsLit(..), HsOverLit(..), HsExpr(..) )
-import TcHsSyn ( TcExpr, TcId, TcIdSet, 
-                 mkHsTyApp, mkHsDictApp, mkHsConApp, zonkId,
+import HsSyn   ( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp,
+                 nlHsLit, nlHsVar )
+import TcHsSyn ( mkHsTyApp, mkHsDictApp, zonkId, 
                  mkCoercion, ExprCoFn
                )
 import TcRnMonad
-import TcEnv   ( tcGetInstEnv, tcLookupId, tcLookupTyCon, checkWellStaged, topIdLvl )
-import InstEnv ( InstLookupResult(..), lookupInstEnv )
-import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, 
-                 zonkTcThetaType, tcInstTyVar, tcInstType, tcInstTyVars
+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, tcInstType, tcSkolType
                )
-import TcType  ( Type, TcType, TcThetaType, TcTyVarSet,
-                 SourceType(..), PredType, TyVarDetails(VanillaTv),
-                 tcSplitForAllTys, tcSplitForAllTys, mkTyConApp,
-                 tcSplitPhiTy, mkGenTyConApp,
+import TcType  ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar, TcPredType,
+                 PredType(..), SkolemInfo(..), typeKind, mkSigmaTy,
+                 tcSplitForAllTys, mkFunTy,
+                 tcSplitPhiTy, tcSplitDFunHead,
                  isIntTy,isFloatTy, isIntegerTy, isDoubleTy,
-                 tcIsTyVarTy, mkPredTy, mkTyVarTy, mkTyVarTys,
+                 mkPredTy, mkTyVarTy, mkTyVarTys,
                  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred,
                  isClassPred, isTyVarClassPred, isLinearPred, 
-                 getClassPredTys, getClassPredTys_maybe, mkPredName,
+                 getClassPredTys, mkPredName,
                  isInheritablePred, isIPPred, 
-                 tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy
+                 tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy, 
+                 pprPred, pprParendType, pprTheta 
                )
+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,dataConSig )
-import Id      ( Id, idName, idType, mkUserLocal, mkSysLocal, mkLocalId, setIdUnique )
-import PrelInfo        ( isStandardClass, isCcallishClass, isNoDictClass )
-import Name    ( Name, mkMethodOcc, getOccName )
-import PprType ( pprPred, pprParendType )      
-import Subst   ( substTy, substTyWith, substTheta, mkTyVarSubst )
+import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName, dataConWrapId )
+import Id      ( Id, idName, idType, mkUserLocal, mkLocalId )
+import Name    ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
+                 isInternalName, setNameUnique, mkSystemVarName )
+import NameSet ( addOneToNameSet )
 import Literal ( inIntRange )
-import Var     ( TyVar )
-import VarEnv  ( TidyEnv, emptyTidyEnv, lookupSubstEnv, SubstResult(..) )
-import VarSet  ( elemVarSet, emptyVarSet, unionVarSet )
+import Var     ( TyVar, tyVarKind, setIdType )
+import VarEnv  ( TidyEnv, emptyTidyEnv )
+import VarSet  ( elemVarSet, emptyVarSet, unionVarSet, mkVarSet )
 import TysWiredIn ( floatDataCon, doubleDataCon )
-import PrelNames( fromIntegerName, fromRationalName, rationalTyConName )
+import PrelNames       ( integerTyConName, fromIntegerName, fromRationalName, rationalTyConName )
 import BasicTypes( IPName(..), mapIPName, ipNameName )
 import UniqSupply( uniqsFromSupply )
+import SrcLoc  ( mkSrcSpan, noLoc, unLoc, Located(..) )
+import DynFlags        ( DynFlag(..), dopt )
+import Maybes  ( isJust )
 import Outputable
 \end{code}
 
@@ -87,9 +101,9 @@ instName :: Inst -> Name
 instName inst = idName (instToId inst)
 
 instToId :: Inst -> TcId
-instToId (Dict id _ _)        = id
+instToId (LitInst nm _ ty _)   = mkLocalId nm ty
+instToId (Dict nm pred _)      = mkLocalId nm (mkPredTy pred)
 instToId (Method id _ _ _ _ _) = id
-instToId (LitInst id _ _ _)    = id
 
 instLoc (Dict _ _         loc) = loc
 instLoc (Method _ _ _ _ _ loc) = loc
@@ -177,27 +191,8 @@ isLinearInst other      = False
 
 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
-necessarily result in bindings.  The first tells whether an @Inst@
-must be witnessed by an actual binding; the second tells whether an
-@Inst@ can be generalised over.
-
-\begin{code}
-instBindingRequired :: Inst -> Bool
-instBindingRequired (Dict _ (ClassP clas _) _) = not (isNoDictClass clas)
-instBindingRequired other                     = True
-
-instCanBeGeneralised :: Inst -> Bool
-instCanBeGeneralised (Dict _ (ClassP clas _) _) = not (isCcallishClass clas)
-instCanBeGeneralised other                     = True
-\end{code}
 
 
 %************************************************************************
@@ -215,24 +210,23 @@ newDicts orig theta
     newDictsAtLoc loc theta
 
 cloneDict :: Inst -> TcM Inst
-cloneDict (Dict id ty loc) = newUnique `thenM` \ uniq ->
-                            returnM (Dict (setIdUnique id uniq) ty loc)
+cloneDict (Dict nm ty loc) = newUnique `thenM` \ uniq ->
+                            returnM (Dict (setNameUnique nm uniq) ty loc)
 
-newDictsFromOld :: Inst -> TcThetaType -> TcM [Inst]
-newDictsFromOld (Dict _ _ loc) theta = newDictsAtLoc loc theta
+newDictAtLoc :: InstLoc -> TcPredType -> TcM Inst
+newDictAtLoc inst_loc pred
+  = do { uniq <- newUnique
+       ; return (mkDict inst_loc uniq pred) }
 
--- Local function, similar to newDicts, 
--- but with slightly different interface
-newDictsAtLoc :: InstLoc
-             -> TcThetaType
-             -> TcM [Inst]
+newDictsAtLoc :: InstLoc -> TcThetaType -> TcM [Inst]
 newDictsAtLoc inst_loc theta
   = newUniqueSupply            `thenM` \ us ->
-    returnM (zipWith mk_dict (uniqsFromSupply us) theta)
+    returnM (zipWith (mkDict inst_loc) (uniqsFromSupply us) theta)
+
+mkDict inst_loc uniq pred
+  = Dict name pred inst_loc
   where
-    mk_dict uniq pred = Dict (mkLocalId (mkPredName uniq loc pred) (mkPredTy pred))
-                            pred inst_loc
-    loc = instLocSrcLoc inst_loc
+    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
@@ -241,13 +235,14 @@ newDictsAtLoc inst_loc theta
 newIPDict :: InstOrigin -> IPName Name -> Type 
          -> TcM (IPName Id, Inst)
 newIPDict orig ip_name ty
-  = getInstLoc orig                    `thenM` \ inst_loc@(InstLoc _ loc _) ->
+  = getInstLoc orig                    `thenM` \ inst_loc ->
     newUnique                          `thenM` \ uniq ->
     let
        pred = IParam ip_name ty
-       id   = mkLocalId (mkPredName uniq loc pred) (mkPredTy pred)
+        name = mkPredName uniq (instLocSrcLoc inst_loc) pred 
+       dict = Dict name pred inst_loc
     in
-    returnM (mapIPName (\n -> id) ip_name, Dict id pred inst_loc)
+    returnM (mapIPName (\n -> instToId dict) ip_name, dict)
 \end{code}
 
 
@@ -260,46 +255,28 @@ newIPDict orig ip_name ty
 
 
 \begin{code}
-tcInstCall :: InstOrigin  -> TcType -> TcM (ExprCoFn, TcType)
+tcInstCall :: InstOrigin -> TcType -> TcM (ExprCoFn, [TcTyVar], TcType)
 tcInstCall orig fun_ty -- fun_ty is usually a sigma-type
-  = tcInstType VanillaTv fun_ty        `thenM` \ (tyvars, theta, tau) ->
-    newDicts orig theta                `thenM` \ dicts ->
-    extendLIEs dicts           `thenM_`
-    let
-       inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tyvars)) (map instToId dicts)
-    in
-    returnM (mkCoercion inst_fn, tau)
-
-tcInstDataCon :: InstOrigin -> DataCon
-             -> TcM ([TcType], -- Types to instantiate at
-                     [Inst],   -- Existential dictionaries to apply to
-                     [TcType], -- Argument types of constructor
-                     TcType,   -- Result type
-                     [TyVar])  -- Existential tyvars
-tcInstDataCon orig data_con
-  = let 
-       (tvs, stupid_theta, ex_tvs, ex_theta, arg_tys, tycon) = dataConSig data_con
-            -- We generate constraints for the stupid theta even when 
-            -- pattern matching (as the Report requires)
-    in
-    tcInstTyVars VanillaTv (tvs ++ ex_tvs)     `thenM` \ (all_tvs', ty_args', tenv) ->
-    let
-       stupid_theta' = substTheta tenv stupid_theta
-       ex_theta'     = substTheta tenv ex_theta
-       arg_tys'      = map (substTy tenv) arg_tys
-
-       n_normal_tvs  = length tvs
-       ex_tvs'       = drop n_normal_tvs all_tvs'
-       result_ty     = mkTyConApp tycon (take n_normal_tvs ty_args')
-    in
-    newDicts orig stupid_theta'        `thenM` \ stupid_dicts ->
-    newDicts orig ex_theta'    `thenM` \ ex_dicts ->
-
-       -- Note that we return the stupid theta *only* in the LIE;
-       -- we don't otherwise use it at all
-    extendLIEs stupid_dicts    `thenM_`
-
-    returnM (ty_args', ex_dicts, arg_tys', result_ty, ex_tvs')
+  = 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
@@ -325,6 +302,11 @@ newMethodWithGivenTy orig id tys theta tau
 -- 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
@@ -333,8 +315,21 @@ tcInstClassOp inst_loc sel_id tys
                       substTyWith tyvars tys rho
        (preds,tau)  = tcSplitPhiTy rho_ty
     in
+    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 ->
@@ -346,74 +341,89 @@ newMethod inst_loc id tys theta tau
     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
-                -> HsOverLit
+tcOverloadedLit :: InstOrigin
+                -> HsOverLit Name
                 -> TcType
-                -> TcM TcExpr
-newOverloadedLit orig lit@(HsIntegral i fi) expected_ty
-  | fi /= fromIntegerName      -- Do not generate a LitInst for rebindable
-                               -- syntax.  Reason: tcSyntaxName does unification
-                               -- which is very inconvenient in tcSimplify
-  = tcSyntaxName orig expected_ty fromIntegerName fi   `thenM` \ (expr, _) ->
-    returnM (HsApp expr (HsLit (HsInteger i)))
+                -> TcM (HsOverLit TcId)
+tcOverloadedLit orig lit@(HsIntegral i fi) expected_ty
+  | not (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 
-  = returnM expr
+  = return (HsIntegral i expr)
 
   | otherwise
-  = newLitInst orig lit expected_ty
+  = do         { expr <- newLitInst orig lit expected_ty
+       ; return (HsIntegral i expr) }
 
-newOverloadedLit orig lit@(HsFractional r fr) expected_ty
-  | fr /= fromRationalName     -- c.f. HsIntegral case
-  = tcSyntaxName orig expected_ty fromRationalName fr  `thenM` \ (expr, _) ->
-    mkRatLit r                                         `thenM` \ rat_lit ->
-    returnM (HsApp expr rat_lit)
+tcOverloadedLit orig lit@(HsFractional r fr) expected_ty
+  | not (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 
-  = returnM expr
+  = return (HsFractional r expr)
 
   | otherwise
-  = newLitInst orig lit expected_ty
-
-newLitInst orig lit expected_ty
-  = getInstLoc orig            `thenM` \ loc ->
-    newUnique                  `thenM` \ new_uniq ->
-    let
-       lit_inst = LitInst lit_id lit expected_ty loc
-       lit_id   = mkSysLocal FSLIT("lit") new_uniq expected_ty
-    in
-    extendLIE lit_inst         `thenM_`
-    returnM (HsVar (instToId lit_inst))
-
-shortCutIntLit :: Integer -> TcType -> Maybe TcExpr
+  = 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   = mkSystemVarName new_uniq FSLIT("lit")
+               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
+  | isIntTy ty && inIntRange i                 -- Short cut for Int
   = Just (HsLit (HsInt i))
-  | isIntegerTy ty                             -- Short cut for Integer
-  = Just (HsLit (HsInteger i))
+  | isIntegerTy ty                     -- Short cut for Integer
+  = Just (HsLit (HsInteger i ty))
   | otherwise = Nothing
 
-shortCutFracLit :: Rational -> TcType -> Maybe TcExpr
+shortCutFracLit :: Rational -> TcType -> Maybe (HsExpr TcId)
 shortCutFracLit f ty
   | isFloatTy ty 
-  = Just (mkHsConApp floatDataCon [] [HsLit (HsFloatPrim f)])
+  = Just (mk_lit floatDataCon (HsFloatPrim f))
   | isDoubleTy ty
-  = Just (mkHsConApp doubleDataCon [] [HsLit (HsDoublePrim f)])
+  = 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 TcExpr
+mkRatLit :: Rational -> TcM (LHsExpr TcId)
 mkRatLit r
-  = tcLookupTyCon rationalTyConName                    `thenM` \ rat_tc ->
-    let
-       rational_ty  = mkGenTyConApp rat_tc []
-    in
-    returnM (HsLit (HsRat r rational_ty))
+  = 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}
 
 
@@ -423,15 +433,13 @@ mkRatLit r
 %*                                                                     *
 %************************************************************************
 
-Zonking makes sure that the instance types are fully zonked,
-but doesn't do the same for any of the Ids in an Inst.  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 -> TcM Inst
-zonkInst (Dict id pred loc)
+zonkInst (Dict name pred loc)
   = zonkTcPredType pred                        `thenM` \ new_pred ->
-    returnM (Dict id new_pred loc)
+    returnM (Dict name new_pred loc)
 
 zonkInst (Method m id tys theta tau loc) 
   = zonkId id                  `thenM` \ new_id ->
@@ -444,9 +452,9 @@ zonkInst (Method m id tys theta tau loc)
     zonkTcType tau             `thenM` \ new_tau ->
     returnM (Method m new_id new_tys new_theta new_tau loc)
 
-zonkInst (LitInst id lit ty loc)
+zonkInst (LitInst nm lit ty loc)
   = zonkTcType ty                      `thenM` \ new_ty ->
-    returnM (LitInst id lit new_ty loc)
+    returnM (LitInst nm lit new_ty loc)
 
 zonkInsts insts = mappM zonkInst insts
 \end{code}
@@ -465,32 +473,37 @@ relevant in error messages.
 instance Outputable Inst where
     ppr inst = pprInst inst
 
-pprInsts :: [Inst] -> SDoc
-pprInsts insts  = parens (sep (punctuate comma (map pprInst insts)))
+pprDictsTheta :: [Inst] -> SDoc
+-- Print in type-like fashion (Eq a, Show b)
+pprDictsTheta dicts = pprTheta (map dictPred dicts)
 
-pprInstsInFull insts
-  = vcat (map go insts)
+pprDictsInFull :: [Inst] -> SDoc
+-- Print in type-like fashion, but with source location
+pprDictsInFull dicts 
+  = vcat (map go dicts)
   where
-    go inst = sep [quotes (ppr inst), nest 2 (pprInstLoc (instLoc inst))]
+    go dict = sep [quotes (ppr (dictPred dict)), nest 2 (pprInstLoc (instLoc dict))]
 
-pprInst (LitInst u lit ty loc)
-  = hsep [ppr lit, ptext SLIT("at"), ppr ty, show_uniq u]
+pprInsts :: [Inst] -> SDoc
+-- Debugging: print the evidence :: type
+pprInsts insts  = brackets (interpp'SP insts)
 
-pprInst (Dict u pred loc) = pprPred pred <+> show_uniq u
+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 u id tys theta tau loc)
-  = hsep [ppr id, ptext SLIT("at"), 
-         brackets (sep (map pprParendType tys)) {- ,
-         ptext SLIT("theta"), ppr theta,
-         ptext SLIT("tau"), ppr tau
-         show_uniq u,
-         ppr (instToId m) -}]
+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))])
 
-show_uniq u = ifPprDebug (text "{-" <> ppr u <> text "-}")
+pprInstInFull inst
+  = sep [quotes (pprInst inst), nest 2 (pprInstLoc (instLoc inst))]
 
 tidyInst :: TidyEnv -> Inst -> Inst
-tidyInst env (LitInst u lit ty loc)         = LitInst u lit (tidyType env ty) loc
-tidyInst env (Dict u pred loc)              = Dict u (tidyPred env pred) loc
+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])
@@ -508,107 +521,257 @@ showLIE :: SDoc -> TcM ()       -- Debugging
 showLIE str
   = do { lie_var <- getLIEVar ;
         lie <- readMutVar lie_var ;
-        traceTc (str <+> pprInstsInFull (lieToList lie)) }
+        traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) }
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
+       Extending the instance environment
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
+  -- Add new locally-defined instances
+tcExtendLocalInstEnv dfuns thing_inside
+ = do { traceDFuns dfuns
+      ; env <- getGblEnv
+      ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
+      ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
+                        tcg_inst_env = inst_env' }
+      ; setGblEnv env' thing_inside }
+
+addLocalInst :: InstEnv -> Instance -> TcM InstEnv
+-- Check that the proposed new instance is OK, 
+-- and then add it to the home inst env
+addLocalInst home_ie ispec
+  = 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.  
+         let dfun = instanceDFunId ispec
+       ; (tvs', theta', tau') <- tcSkolType (InstSkol dfun) (idType dfun)
+       ; let   (cls, tys') = tcSplitDFunHead tau'
+               dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
+               ispec'      = setInstanceDFunId ispec dfun'
+
+               -- Load imported instances, so that we report
+               -- duplicates correctly
+       ; eps <- getEps
+       ; let inst_envs = (eps_inst_env eps, home_ie)
+
+               -- Check functional dependencies
+       ; case checkFunDeps inst_envs ispec' of
+               Just specs -> funDepErr ispec' specs
+               Nothing    -> return ()
+
+               -- Check for duplicate instance decls
+       ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
+             ; dup_ispecs = [ dup_ispec 
+                            | (_, 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.
+               -- If the match is 2-way, it's a duplicate
+       ; case dup_ispecs of
+           dup_ispec : _ -> dupInstErr ispec' dup_ispec
+           []            -> return ()
+
+               -- 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 ispecs
+  = traceTc (hang (text "Adding instances:") 2 (vcat (map pp ispecs)))
+  where
+    pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
+       -- Print the dfun name itself too
+
+funDepErr ispec ispecs
+  = addDictLoc ispec $
+    addErr (hang (ptext SLIT("Functional dependencies conflict between instance declarations:"))
+              2 (pprInstances (ispec:ispecs)))
+dupInstErr ispec dup_ispec
+  = addDictLoc ispec $
+    addErr (hang (ptext SLIT("Duplicate instance declarations:"))
+              2 (pprInstances [ispec, dup_ispec]))
+
+addDictLoc ispec thing_inside
+  = setSrcSpan (mkSrcSpan loc loc) thing_inside
+  where
+   loc = getSrcLoc ispec
+\end{code}
+    
+
+%************************************************************************
+%*                                                                     *
 \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
+  | SimpleInst (LHsExpr TcId)          -- Just a variable, type application, or literal
+  | GenInst    [Inst] (LHsExpr TcId)   -- The expression and its needed insts
 
-lookupInst :: Inst -> TcM (LookupInstResult s)
+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
 
 
--- Dictionaries
-lookupInst dict@(Dict _ pred@(ClassP clas tys) loc)
-  = getDOpts                   `thenM` \ dflags ->
-    tcGetInstEnv               `thenM` \ inst_env ->
-    case lookupInstEnv dflags inst_env clas tys of
-
-      FoundInst tenv dfun_id
-       ->      -- 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 mk_ty_arg to instantiate any un-substituted tyvars.        
-          getStage                                             `thenM` \ use_stage ->
-          checkWellStaged (ptext SLIT("instance for") <+> quotes (ppr pred))
-                          (topIdLvl dfun_id) use_stage         `thenM_`
-          traceTc (text "lookupInst" <+> ppr dfun_id <+> ppr (topIdLvl dfun_id) <+> ppr use_stage) `thenM_`
-          let
-               (tyvars, rho) = tcSplitForAllTys (idType dfun_id)
-               mk_ty_arg tv  = case lookupSubstEnv tenv tv of
-                                  Just (DoneTy ty) -> returnM ty
-                                  Nothing          -> tcInstTyVar VanillaTv tv `thenM` \ tc_tv ->
-                                                      returnM (mkTyVarTy tc_tv)
-          in
-          mappM mk_ty_arg tyvars       `thenM` \ ty_args ->
-          let
-               dfun_rho   = substTy (mkTyVarSubst tyvars ty_args) rho
-               (theta, _) = tcSplitPhiTy dfun_rho
-               ty_app     = mkHsTyApp (HsVar dfun_id) ty_args
-          in
-          if null theta then
-               returnM (SimpleInst ty_app)
-          else
-          newDictsAtLoc loc theta      `thenM` \ dicts ->
-          let 
-               rhs = mkHsDictApp ty_app (map instToId dicts)
-          in
-          returnM (GenInst dicts rhs)
-
-      other    -> returnM NoInstance
-
-lookupInst (Dict _ _ _)         = returnM NoInstance
-
 -- Methods
 
 lookupInst inst@(Method _ id tys theta _ loc)
   = newDictsAtLoc loc theta            `thenM` \ dicts ->
-    returnM (GenInst dicts (mkHsDictApp (mkHsTyApp (HsVar id) tys) (map instToId dicts)))
+    returnM (GenInst dicts (mkHsDictApp (mkHsTyApp (L span (HsVar id)) tys) (map instToId dicts)))
+  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).
+-- This is essential (see nofib/spectral/nucleic).
 -- [Same shortcut as in newOverloadedLit, but we
 --  may have done some unification by now]             
 
-
-lookupInst inst@(LitInst u (HsIntegral i from_integer_name) ty loc)
+lookupInst inst@(LitInst _nm (HsIntegral i from_integer_name) ty loc)
   | Just expr <- shortCutIntLit i ty
-  = returnM (GenInst [] expr)  -- GenInst, not SimpleInst, because 
+  = returnM (GenInst [] (noLoc expr))  -- GenInst, not SimpleInst, because 
                                        -- expr may be a constructor application
   | otherwise
-  = ASSERT( from_integer_name == fromIntegerName )     -- A LitInst invariant
+  = 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]
-                    (HsApp (HsVar (instToId method_inst)) (HsLit (HsInteger i))))
+                    (mkHsApp (L (instLocSrcSpan loc)
+                                (HsVar (instToId method_inst))) integer_lit))
 
-
-lookupInst inst@(LitInst u (HsFractional f from_rat_name) ty loc)
+lookupInst inst@(LitInst _nm (HsFractional f from_rat_name) ty loc)
   | Just expr <- shortCutFracLit f ty
-  = returnM (GenInst [] expr)
+  = returnM (GenInst [] (noLoc expr))
 
   | otherwise
-  = ASSERT( from_rat_name == fromRationalName )        -- A LitInst invariant
+  = 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] (HsApp (HsVar (instToId method_inst)) 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 { gbl <- getGblEnv
+       ; let  dfun_name = idName dfun_id
+              dfun_mod  = nameModule dfun_name
+       ; if isInternalName dfun_name ||    -- Internal name => defined in this module
+            not (isHomeModule (tcg_home_mods gbl) 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}
 
 
@@ -619,7 +782,6 @@ lookupInst inst@(LitInst u (HsFractional f from_rat_name) ty loc)
 %*                                                                     *
 %************************************************************************
 
-
 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
@@ -645,29 +807,34 @@ just use the expression inline.
 \begin{code}
 tcSyntaxName :: InstOrigin
             -> TcType                  -- Type to instantiate it at
-            -> Name -> Name            -- (Standard name, user name)
-            -> TcM (TcExpr, TcType)    -- Suitable expression with its type
-
+            -> (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 user_nm
+tcSyntaxName orig ty (std_nm, HsVar user_nm)
   | std_nm == user_nm
   = newMethodFromName orig ty std_nm   `thenM` \ id ->
-    returnM (HsVar id, idType id)
+    returnM (std_nm, HsVar id)
 
-  | otherwise
+tcSyntaxName orig ty (std_nm, user_nm_expr)
   = tcLookupId std_nm          `thenM` \ std_id ->
     let        
        -- C.f. newMethodAtLoc
        ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
-       tau1            = substTyWith [tv] [ty] tau
+       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 orig tau1)     $
-    tcCheckSigma (HsVar user_nm) tau1                  `thenM` \ user_fn ->
-    returnM (user_fn, tau1)
+    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 -> 
+    tcCheckSigma (L span user_nm_expr) sigma1  `thenM` \ expr ->
+    returnM (std_nm, unLoc expr)
 
 syntaxNameCtxt name orig ty tidy_env
   = getInstLoc orig            `thenM` \ inst_loc ->