Look through type synonyms when deciding if something is a type literal.
[ghc.git] / compiler / types / InstEnv.lhs
index 7a2a65e..569697c 100644 (file)
@@ -8,15 +8,15 @@ The bits common to TcInstDcls and TcDeriv.
 
 \begin{code}
 module InstEnv (
-       DFunId, OverlapFlag(..),
-       Instance(..), pprInstance, pprInstanceHdr, pprInstances, 
-       instanceHead, mkLocalInstance, mkImportedInstance,
-       instanceDFunId, setInstanceDFunId, instanceRoughTcs,
-
-       InstEnv, emptyInstEnv, extendInstEnv, 
-       extendInstEnvList, lookupInstEnv, instEnvElts,
-       classInstances, instanceBindFun,
-       instanceCantMatch, roughMatchTcs
+        DFunId, OverlapFlag(..), InstMatch, ClsInstLookupResult,
+        ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances, 
+        instanceHead, instanceSig, mkLocalInstance, mkImportedInstance,
+        instanceDFunId, tidyClsInstDFun, instanceRoughTcs,
+
+        InstEnv, emptyInstEnv, extendInstEnv, overwriteInstEnv, 
+        extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv', lookupInstEnv, instEnvElts,
+        classInstances, instanceBindFun,
+        instanceCantMatch, roughMatchTcs
     ) where
 
 #include "HsVersions.h"
@@ -29,45 +29,66 @@ import TcType
 import TyCon
 import Unify
 import Outputable
+import ErrUtils
 import BasicTypes
 import UniqFM
+import Util
 import Id
 import FastString
-
-import Data.Maybe      ( isJust, isNothing )
+import Data.Data        ( Data, Typeable )
+import Data.Maybe       ( isJust, isNothing )
 \end{code}
 
 
 %************************************************************************
-%*                                                                     *
+%*                                                                      *
 \subsection{The key types}
-%*                                                                     *
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
-data Instance 
-  = Instance { is_cls  :: Name         -- Class name
-       
-               -- Used for "rough matching"; see Note [Rough-match field]
-               -- INVARIANT: is_tcs = roughMatchTcs is_tys
-            , is_tcs  :: [Maybe Name]  -- Top of type args
-
-               -- Used for "proper matching"; see Note [Proper-match fields]
-            , is_tvs  :: TyVarSet      -- Template tyvars for full match
-            , is_tys  :: [Type]        -- Full arg types
-               -- INVARIANT: is_dfun Id has type 
-               --      forall is_tvs. (...) => is_cls is_tys
-
-            , is_dfun :: DFunId -- See Note [Haddock assumptions]
-            , is_flag :: OverlapFlag   -- See detailed comments with
-                                       -- the decl of BasicTypes.OverlapFlag
+data ClsInst 
+  = ClsInst {   -- Used for "rough matching"; see Note [Rough-match field]
+                -- INVARIANT: is_tcs = roughMatchTcs is_tys
+               is_cls_nm :: Name  -- Class name
+             , is_tcs  :: [Maybe Name]  -- Top of type args
+
+                -- Used for "proper matching"; see Note [Proper-match fields]
+             , is_tvs  :: [TyVar]       -- Fresh template tyvars for full match
+                                        -- See Note [Template tyvars are fresh]
+             , is_cls  :: Class         -- The real class
+             , is_tys  :: [Type]        -- Full arg types (mentioning is_tvs)
+                -- INVARIANT: is_dfun Id has type 
+                --      forall is_tvs. (...) => is_cls is_tys
+                -- (modulo alpha conversion)
+
+             , is_dfun :: DFunId -- See Note [Haddock assumptions]
+                    -- See Note [Silent superclass arguments] in TcInstDcls
+                    -- for how to map the DFun's type back to the source
+                    -- language instance decl
+
+             , is_flag :: OverlapFlag   -- See detailed comments with
+                                        -- the decl of BasicTypes.OverlapFlag
     }
+  deriving (Data, Typeable)
 \end{code}
 
+Note [Template tyvars are fresh]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The is_tvs field of a ClsInst has *completely fresh* tyvars.  
+That is, they are
+  * distinct from any other ClsInst
+  * distinct from any tyvars free in predicates that may
+    be looked up in the class instance environment
+Reason for freshness: we use unification when checking for overlap
+etc, and that requires the tyvars to be distinct.
+
+The invariant is checked by the ASSERT in lookupInstEnv'.
+
 Note [Rough-match field]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The is_cls, is_tcs fields allow a "rough match" to be done
-without poking inside the DFunId.  Poking the DFunId forces
+The is_cls_nm, is_tcs fields allow a "rough match" to be done
+*without* poking inside the DFunId.  Poking the DFunId forces
 us to suck in all the type constructors etc it involves,
 which is a total waste of time if it has no chance of matching
 So the Name, [Maybe Name] fields allow us to say "definitely
@@ -77,26 +98,25 @@ In is_tcs,
     Nothing  means that this type arg is a type variable
 
     (Just n) means that this type arg is a
-               TyConApp with a type constructor of n.
-               This is always a real tycon, never a synonym!
-               (Two different synonyms might match, but two
-               different real tycons can't.)
-               NB: newtypes are not transparent, though!
+                TyConApp with a type constructor of n.
+                This is always a real tycon, never a synonym!
+                (Two different synonyms might match, but two
+                different real tycons can't.)
+                NB: newtypes are not transparent, though!
 
 Note [Proper-match fields]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
-The is_tvs, is_tys fields are simply cached values, pulled
+The is_tvs, is_cls, is_tys fields are simply cached values, pulled
 out (lazily) from the dfun id. They are cached here simply so 
 that we don't need to decompose the DFunId each time we want 
 to match it.  The hope is that the fast-match fields mean
-that we often never poke th proper-match fields
+that we often never poke the proper-match fields.
 
 However, note that:
  * is_tvs must be a superset of the free vars of is_tys
 
- * The is_dfun must itself be quantified over exactly is_tvs
-   (This is so that we can use the matching substitution to
-    instantiate the dfun's context.)
+ * is_tvs, is_tys may be alpha-renamed compared to the ones in
+   the dfun Id
 
 Note [Haddock assumptions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -114,95 +134,88 @@ being equal to
   * the InstDecl used to construct the Instance.
 
 \begin{code}
-instanceDFunId :: Instance -> DFunId
+instanceDFunId :: ClsInst -> DFunId
 instanceDFunId = is_dfun
 
-setInstanceDFunId :: Instance -> DFunId -> Instance
-setInstanceDFunId ispec dfun
-   = ASSERT( idType dfun `eqType` idType (is_dfun ispec) )
-       -- We need to create the cached fields afresh from
-       -- the new dfun id.  In particular, the is_tvs in
-       -- the Instance must match those in the dfun!
-       -- We assume that the only thing that changes is
-       -- the quantified type variables, so the other fields
-       -- are ok; hence the assert
-     ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
-   where 
-     (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
-
-instanceRoughTcs :: Instance -> [Maybe Name]
+tidyClsInstDFun :: (DFunId -> DFunId) -> ClsInst -> ClsInst
+tidyClsInstDFun tidy_dfun ispec
+  = ispec { is_dfun = tidy_dfun (is_dfun ispec) }
+
+instanceRoughTcs :: ClsInst -> [Maybe Name]
 instanceRoughTcs = is_tcs
 \end{code}
 
 \begin{code}
-instance NamedThing Instance where
+instance NamedThing ClsInst where
    getName ispec = getName (is_dfun ispec)
 
-instance Outputable Instance where
+instance Outputable ClsInst where
    ppr = pprInstance
 
-pprInstance :: Instance -> SDoc
--- Prints the Instance as an instance declaration
+pprInstance :: ClsInst -> SDoc
+-- Prints the ClsInst as an instance declaration
 pprInstance ispec
   = hang (pprInstanceHdr ispec)
-       2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
+        2 (ptext (sLit "--") <+> pprDefinedAt (getName ispec))
 
 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
-pprInstanceHdr :: Instance -> SDoc
--- Prints the Instance as an instance declaration
-pprInstanceHdr ispec@(Instance { is_flag = flag })
+pprInstanceHdr :: ClsInst -> SDoc
+-- Prints the ClsInst as an instance declaration
+pprInstanceHdr (ClsInst { is_flag = flag, is_dfun = dfun })
   = getPprStyle $ \ sty ->
     let theta_to_print
           | debugStyle sty = theta
           | otherwise = drop (dfunNSilent dfun) theta
+          -- See Note [Silent superclass arguments] in TcInstDcls
     in ptext (sLit "instance") <+> ppr flag
        <+> sep [pprThetaArrowTy theta_to_print, ppr res_ty]
   where
-    dfun = is_dfun ispec
     (_, theta, res_ty) = tcSplitSigmaTy (idType dfun)
-       -- Print without the for-all, which the programmer doesn't write
+       -- Print without the for-all, which the programmer doesn't write
 
-pprInstances :: [Instance] -> SDoc
+pprInstances :: [ClsInst] -> SDoc
 pprInstances ispecs = vcat (map pprInstance ispecs)
 
-instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
--- Returns the *source* theta, without the silent arguments
-instanceHead ispec
-   = (tvs, drop n_silent theta, cls, tys)
+instanceHead :: ClsInst -> ([TyVar], Class, [Type])
+-- Returns the head, using the fresh tyavs from the ClsInst
+instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
+   = (tvs, cls, tys)
    where
-     (tvs, theta, tau) = tcSplitSigmaTy (idType dfun)
-     (cls, tys)        = tcSplitDFunHead tau
-     dfun              = is_dfun ispec
-     n_silent          = dfunNSilent dfun
-
-mkLocalInstance :: DFunId
-                -> OverlapFlag
-                -> Instance
+     (_, _, cls, _) = tcSplitDFunTy (idType dfun)
+
+instanceSig :: ClsInst -> ([TyVar], [Type], Class, [Type])
+-- Decomposes the DFunId
+instanceSig ispec = tcSplitDFunTy (idType (is_dfun ispec))
+
+mkLocalInstance :: DFunId -> OverlapFlag
+                -> [TyVar] -> Class -> [Type]
+                -> ClsInst
 -- Used for local instances, where we can safely pull on the DFunId
-mkLocalInstance dfun oflag
-  = Instance { is_flag = oflag, is_dfun = dfun,
-               is_tvs = mkVarSet tvs, is_tys = tys,
-                is_cls = className cls, is_tcs = roughMatchTcs tys }
-  where
-    (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
+mkLocalInstance dfun oflag tvs cls tys
+  = ClsInst { is_flag = oflag, is_dfun = dfun
+            , is_tvs = tvs
+            , is_cls = cls, is_cls_nm = className cls
+            , is_tys = tys, is_tcs = roughMatchTcs tys }
 
 mkImportedInstance :: Name -> [Maybe Name]
-                  -> DFunId -> OverlapFlag -> Instance
+                   -> DFunId -> OverlapFlag -> ClsInst
 -- Used for imported instances, where we get the rough-match stuff
 -- from the interface file
-mkImportedInstance cls mb_tcs dfun oflag
-  = Instance { is_flag = oflag, is_dfun = dfun,
-               is_tvs = mkVarSet tvs, is_tys = tys,
-               is_cls = cls, is_tcs = mb_tcs }
+-- The bound tyvars of the dfun are guaranteed fresh, because
+-- the dfun has been typechecked out of the same interface file
+mkImportedInstance cls_nm mb_tcs dfun oflag
+  = ClsInst { is_flag = oflag, is_dfun = dfun
+            , is_tvs = tvs, is_tys = tys
+            , is_cls_nm = cls_nm, is_cls = cls, is_tcs = mb_tcs }
   where
-    (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
+    (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
 
 roughMatchTcs :: [Type] -> [Maybe Name]
 roughMatchTcs tys = map rough tys
   where
     rough ty = case tcSplitTyConApp_maybe ty of
-                 Just (tc,_) -> Just (tyConName tc)
-                 Nothing     -> Nothing
+                  Just (tc,_) -> Just (tyConName tc)
+                  Nothing     -> Nothing
 
 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
@@ -328,18 +341,18 @@ this test.  Suppose the instance envt had
     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
 (still most specific first)
 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
-       C x y Int  doesn't match the template {a,b} C a a b
+        C x y Int  doesn't match the template {a,b} C a a b
 but neither does 
-       C a a b  match the template {x,y} C x y Int
+        C a a b  match the template {x,y} C x y Int
 But still x and y might subsequently be unified so they *do* match.
 
 Simple story: unify, don't match.
 
 
 %************************************************************************
-%*                                                                     *
-               InstEnv, ClsInstEnv
-%*                                                                     *
+%*                                                                      *
+                InstEnv, ClsInstEnv
+%*                                                                      *
 %************************************************************************
 
 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
@@ -347,65 +360,81 @@ ClsInstEnv mapping is the dfun for that instance.
 
 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
 
-       forall a b, C t1 t2 t3  can be constructed by dfun
+        forall a b, C t1 t2 t3  can be constructed by dfun
 
 or, to put it another way, we have
 
-       instance (...) => C t1 t2 t3,  witnessed by dfun
+        instance (...) => C t1 t2 t3,  witnessed by dfun
 
 \begin{code}
 ---------------------------------------------------
-type InstEnv = UniqFM ClsInstEnv       -- Maps Class to instances for that class
+type InstEnv = UniqFM ClsInstEnv        -- Maps Class to instances for that class
 
-data ClsInstEnv 
-  = ClsIE [Instance]   -- The instances for a particular class, in any order
-         Bool          -- True <=> there is an instance of form C a b c
-                       --      If *not* then the common case of looking up
-                       --      (C a b c) can fail immediately
+newtype ClsInstEnv 
+  = ClsIE [ClsInst]    -- The instances for a particular class, in any order
 
 instance Outputable ClsInstEnv where
-  ppr (ClsIE is b) = ptext (sLit "ClsIE") <+> ppr b <+> pprInstances is
+  ppr (ClsIE is) = pprInstances is
 
 -- INVARIANTS:
---  * The is_tvs are distinct in each Instance
---     of a ClsInstEnv (so we can safely unify them)
+--  * The is_tvs are distinct in each ClsInst
+--      of a ClsInstEnv (so we can safely unify them)
 
 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
---     [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
+--      [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.
 
 emptyInstEnv :: InstEnv
 emptyInstEnv = emptyUFM
 
-instEnvElts :: InstEnv -> [Instance]
-instEnvElts ie = [elt | ClsIE elts <- eltsUFM ie, elt <- elts]
+instEnvElts :: InstEnv -> [ClsInst]
+instEnvElts ie = [elt | ClsIE elts <- eltsUFM ie, elt <- elts]
 
-classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
+classInstances :: (InstEnv,InstEnv) -> Class -> [ClsInst]
 classInstances (pkg_ie, home_ie) cls 
   = get home_ie ++ get pkg_ie
   where
     get env = case lookupUFM env cls of
-               Just (ClsIE insts _) -> insts
-               Nothing              -> []
+                Just (ClsIE insts) -> insts
+                Nothing            -> []
 
-extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
+extendInstEnvList :: InstEnv -> [ClsInst] -> InstEnv
 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
 
-extendInstEnv :: InstEnv -> Instance -> InstEnv
-extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
-  = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
+extendInstEnv :: InstEnv -> ClsInst -> InstEnv
+extendInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
+  = addToUFM_C add inst_env cls_nm (ClsIE [ins_item])
   where
-    add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
-                                             (ins_tyvar || cur_tyvar)
-    ins_tyvar = not (any isJust mb_tcs)
+    add (ClsIE cur_insts) _ = ClsIE (ins_item : cur_insts)
+
+overwriteInstEnv :: InstEnv -> ClsInst -> InstEnv
+overwriteInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm, is_tys = tys })
+  = addToUFM_C add inst_env cls_nm (ClsIE [ins_item])
+  where
+    add (ClsIE cur_insts) _ = ClsIE (replaceInst cur_insts)
+    
+    rough_tcs  = roughMatchTcs tys
+    replaceInst [] = [ins_item]
+    replaceInst (item@(ClsInst { is_tcs = mb_tcs,  is_tvs = tpl_tvs 
+                               , is_tys = tpl_tys }) : rest)
+    -- Fast check for no match, uses the "rough match" fields
+      | instanceCantMatch rough_tcs mb_tcs
+      = item : replaceInst rest
+
+      | let tpl_tv_set = mkVarSet tpl_tvs
+      , Just _ <- tcMatchTys tpl_tv_set tpl_tys tys
+      = ins_item : rest
+
+      | otherwise
+      = item : replaceInst rest
 \end{code}
 
 
 %************************************************************************
-%*                                                                     *
-       Looking up an instance
-%*                                                                     *
+%*                                                                      *
+        Looking up an instance
+%*                                                                      *
 %************************************************************************
 
 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
@@ -413,106 +442,163 @@ the env is kept ordered, the first match must be the only one.  The
 thing we are looking up can have an arbitrary "flexi" part.
 
 \begin{code}
-type InstTypes = [Either TyVar Type]
-       -- Right ty     => Instantiate with this type
-       -- Left tv      => Instantiate with any type of this tyvar's kind
-
-type InstMatch = (Instance, InstTypes)
+type DFunInstType = Maybe Type
+        -- Just ty   => Instantiate with this type
+        -- Nothing   => Instantiate with any type of this tyvar's kind
+        -- See Note [DFunInstType: instantiating types]
+
+type InstMatch = (ClsInst, [DFunInstType])
+
+type ClsInstLookupResult 
+     = ( [InstMatch]     -- Successful matches
+       , [ClsInst]       -- These don't match but do unify
+       , Bool)           -- True if error condition caused by
+                         -- SafeHaskell condition.
 \end{code}
 
-Note [InstTypes: instantiating types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A successful match is an Instance, together with the types at which
-       the dfun_id in the Instance should be instantiated
-The instantiating types are (Mabye Type)s because the dfun
+Note [DFunInstType: instantiating types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A successful match is a ClsInst, together with the types at which
+        the dfun_id in the ClsInst should be instantiated
+The instantiating types are (Either TyVar Type)s because the dfun
 might have some tyvars that *only* appear in arguments
-       dfun :: forall a b. C a b, Ord b => D [a]
+        dfun :: forall a b. C a b, Ord b => D [a]
 When we match this against D [ty], we return the instantiating types
-       [Right ty, Left b]
-where the Nothing indicates that 'b' can be freely instantiated.  
-(The caller instantiates it to a flexi type variable, which will presumably
+        [Just ty, Nothing]
+where the 'Nothing' indicates that 'b' can be freely instantiated.  
+(The caller instantiates it to a flexi type variable, which will 
  presumably later become fixed via functional dependencies.)
 
 \begin{code}
-lookupInstEnv :: (InstEnv, InstEnv)    -- External and home package inst-env
-             -> Class -> [Type]        -- What we are looking for
-             -> ([InstMatch],          -- Successful matches
-                 [Instance])           -- These don't match but do unify
-
+-- |Look up an instance in the given instance environment. The given class application must match exactly
+-- one instance and the match may not contain any flexi type variables.  If the lookup is unsuccessful,
+-- yield 'Left errorMessage'.
+--
+lookupUniqueInstEnv :: (InstEnv, InstEnv) 
+                    -> Class -> [Type]
+                    -> Either MsgDoc (ClsInst, [Type])
+lookupUniqueInstEnv instEnv cls tys
+  = case lookupInstEnv instEnv cls tys of
+      ([(inst, inst_tys)], _, _) 
+             | noFlexiVar -> Right (inst, inst_tys')
+             | otherwise  -> Left $ ptext (sLit "flexible type variable:") <+>
+                                    (ppr $ mkTyConApp (classTyCon cls) tys)
+             where
+               inst_tys'  = [ty | Just ty <- inst_tys]
+               noFlexiVar = all isJust inst_tys
+      _other -> Left $ ptext (sLit "instance not found") <+> (ppr $ mkTyConApp (classTyCon cls) tys)
+
+lookupInstEnv' :: InstEnv          -- InstEnv to look in
+               -> Class -> [Type]  -- What we are looking for
+               -> ([InstMatch],    -- Successful matches
+                   [ClsInst])     -- These don't match but do unify
 -- The second component of the result pair happens when we look up
---     Foo [a]
+--      Foo [a]
 -- in an InstEnv that has entries for
---     Foo [Int]
---     Foo [b]
+--      Foo [Int]
+--      Foo [b]
 -- Then which we choose would depend on the way in which 'a'
 -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
 -- but Foo [Int] is a unifier.  This gives the caller a better chance of
--- giving a suitable error messagen
+-- giving a suitable error message
 
-lookupInstEnv (pkg_ie, home_ie) cls tys
-  = (pruned_matches, all_unifs)
+lookupInstEnv' ie cls tys
+  = lookup ie
   where
     rough_tcs  = roughMatchTcs tys
     all_tvs    = all isNothing rough_tcs
-    (home_matches, home_unifs) = lookup home_ie 
-    (pkg_matches,  pkg_unifs)  = lookup pkg_ie  
-    all_matches = home_matches ++ pkg_matches
-    all_unifs   = home_unifs   ++ pkg_unifs
-    pruned_matches = foldr insert_overlapping [] all_matches
-       -- Even if the unifs is non-empty (an error situation)
-       -- we still prune the matches, so that the error message isn't
-       -- misleading (complaining of multiple matches when some should be
-       -- overlapped away)
-
     --------------
     lookup env = case lookupUFM env cls of
-                  Nothing -> ([],[])   -- No instances for this class
-                  Just (ClsIE insts has_tv_insts)
-                       | all_tvs && not has_tv_insts
-                       -> ([],[])      -- Short cut for common case
-                       -- The thing we are looking up is of form (C a b c), and
-                       -- the ClsIE has no instances of that form, so don't bother to search
-       
-                       | otherwise
-                       -> find [] [] insts
+                   Nothing -> ([],[])   -- No instances for this class
+                   Just (ClsIE insts) -> find [] [] insts
 
     --------------
-    lookup_tv :: TvSubst -> TyVar -> Either TyVar Type 
-       -- See Note [InstTypes: instantiating types]
-    lookup_tv subst tv = case lookupTyVar subst tv of
-                               Just ty -> Right ty
-                               Nothing -> Left tv
-
     find ms us [] = (ms, us)
-    find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs, 
-                                is_tys = tpl_tys, is_flag = oflag,
-                                is_dfun = dfun }) : rest)
-       -- Fast check for no match, uses the "rough match" fields
+    find ms us (item@(ClsInst { is_tcs = mb_tcs, is_tvs = tpl_tvs
+                              , is_tys = tpl_tys, is_flag = oflag }) : rest)
+        -- Fast check for no match, uses the "rough match" fields
       | instanceCantMatch rough_tcs mb_tcs
       = find ms us rest
 
-      | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
-      = let 
-           (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
-       in 
-       ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs )   -- Check invariant
-       find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
+      | Just subst <- tcMatchTys tpl_tv_set tpl_tys tys
+      = find ((item, map (lookup_tv subst) tpl_tvs) : ms) us rest
 
-       -- Does not match, so next check whether the things unify
-       -- See Note [Overlapping instances] above
-      | Incoherent <- oflag
+        -- Does not match, so next check whether the things unify
+        -- See Note [Overlapping instances] above
+      | Incoherent <- oflag
       = find ms us rest
 
       | otherwise
-      = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
-                (ppr cls <+> ppr tys <+> ppr all_tvs) $$
-                (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
-               )
-               -- Unification will break badly if the variables overlap
-               -- They shouldn't because we allocate separate uniques for them
+      = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tv_set,
+                 (ppr cls <+> ppr tys <+> ppr all_tvs) $$
+                 (ppr tpl_tvs <+> ppr tpl_tys)
+                )
+                -- Unification will break badly if the variables overlap
+                -- They shouldn't because we allocate separate uniques for them
+                -- See Note [Template tyvars are fresh]
         case tcUnifyTys instanceBindFun tpl_tys tys of
-           Just _   -> find ms (item:us) rest
-           Nothing  -> find ms us        rest
+            Just _   -> find ms (item:us) rest
+            Nothing  -> find ms us        rest
+      where
+        tpl_tv_set = mkVarSet tpl_tvs
+
+    ----------------
+    lookup_tv :: TvSubst -> TyVar -> DFunInstType
+        -- See Note [DFunInstType: instantiating types]
+    lookup_tv subst tv = case lookupTyVar subst tv of
+                                Just ty -> Just ty
+                                Nothing -> Nothing
+
+---------------
+-- This is the common way to call this function.
+lookupInstEnv :: (InstEnv, InstEnv)     -- External and home package inst-env
+              -> Class -> [Type]   -- What we are looking for
+              -> ClsInstLookupResult
+lookupInstEnv (pkg_ie, home_ie) cls tys
+  = (safe_matches, all_unifs, safe_fail)
+  where
+    (home_matches, home_unifs) = lookupInstEnv' home_ie cls tys
+    (pkg_matches,  pkg_unifs)  = lookupInstEnv' pkg_ie  cls tys
+    all_matches = home_matches ++ pkg_matches
+    all_unifs   = home_unifs   ++ pkg_unifs
+    pruned_matches = foldr insert_overlapping [] all_matches
+    (safe_matches, safe_fail) = if length pruned_matches == 1 
+                        then check_safe (head pruned_matches) all_matches
+                        else (pruned_matches, False)
+        -- Even if the unifs is non-empty (an error situation)
+        -- we still prune the matches, so that the error message isn't
+        -- misleading (complaining of multiple matches when some should be
+        -- overlapped away)
+
+    -- Safe Haskell: We restrict code compiled in 'Safe' mode from 
+    -- overriding code compiled in any other mode. The rational is
+    -- that code compiled in 'Safe' mode is code that is untrusted
+    -- by the ghc user. So we shouldn't let that code change the
+    -- behaviour of code the user didn't compile in 'Safe' mode
+    -- since that's the code they trust. So 'Safe' instances can only
+    -- overlap instances from the same module. A same instance origin
+    -- policy for safe compiled instances.
+    check_safe match@(inst,_) others
+        = case isSafeOverlap (is_flag inst) of
+                -- most specific isn't from a Safe module so OK
+                False -> ([match], False)
+                -- otherwise we make sure it only overlaps instances from
+                -- the same module
+                True -> (go [] others, True)
+        where
+            go bad [] = match:bad
+            go bad (i@(x,_):unchecked) =
+                if inSameMod x
+                    then go bad unchecked
+                    else go (i:bad) unchecked
+            
+            inSameMod b =
+                let na = getName $ getName inst
+                    la = isInternalName na
+                    nb = getName $ getName b
+                    lb = isInternalName nb
+                in (la && lb) || (nameModule na == nameModule nb)
 
 ---------------
 ---------------
@@ -521,20 +607,20 @@ insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
 insert_overlapping new_item [] = [new_item]
 insert_overlapping new_item (item:items)
   | new_beats_old && old_beats_new = item : insert_overlapping new_item items
-       -- Duplicate => keep both for error report
+        -- Duplicate => keep both for error report
   | new_beats_old = insert_overlapping new_item items
-       -- Keep new one
+        -- Keep new one
   | old_beats_new = item : items
-       -- Keep old one
-  | otherwise    = item : insert_overlapping new_item items
-       -- Keep both
+        -- Keep old one
+  | otherwise     = item : insert_overlapping new_item items
+        -- Keep both
   where
     new_beats_old = new_item `beats` item
     old_beats_new = item `beats` new_item
 
     (instA, _) `beats` (instB, _)
           = overlap_ok && 
-            isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
+            isJust (tcMatchTys (mkVarSet (is_tvs instB)) (is_tys instB) (is_tys instA))
                     -- A beats B if A is more specific than B,
                     -- (ie. if B can be instantiated to match A)
                     -- and overlap is permitted
@@ -543,15 +629,15 @@ insert_overlapping new_item (item:items)
             -- This is a change (Trac #3877, Dec 10). It used to
             -- require that instB (the less specific one) permitted overlap.
             overlap_ok = case (is_flag instA, is_flag instB) of
-                              (NoOverlap, NoOverlap) -> False
-                              _                      -> True
+                              (NoOverlap _, NoOverlap _) -> False
+                              _                          -> True
 \end{code}
 
 
 %************************************************************************
-%*                                                                     *
-       Binding decisions
-%*                                                                     *
+%*                                                                      *
+        Binding decisions
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
@@ -570,17 +656,17 @@ Note [Overlapping instances]
 The key_tys can contain skolem constants, and we can guarantee that those
 are never going to be instantiated to anything, so we should not involve
 them in the unification test.  Example:
-       class Foo a where { op :: a -> Int }
-       instance Foo a => Foo [a]       -- NB overlap
-       instance Foo [Int]              -- NB overlap
-       data T = forall a. Foo a => MkT a
-       f :: T -> Int
-       f (MkT x) = op [x,x]
+        class Foo a where { op :: a -> Int }
+        instance Foo a => Foo [a]       -- NB overlap
+        instance Foo [Int]              -- NB overlap
+        data T = forall a. Foo a => MkT a
+        f :: T -> Int
+        f (MkT x) = op [x,x]
 The op [x,x] means we need (Foo [a]).  Without the filterVarSet we'd
 complain, saying that the choice of instance depended on the instantiation
 of 'a'; but of course it isn't *going* to be instantiated.
 
 We do this only for isOverlappableTyVar skolems.  For example we reject
-       g :: forall a => [a] -> Int
-       g x = op x
+        g :: forall a => [a] -> Int
+        g x = op x
 on the grounds that the correct instance depends on the instantiation of 'a'