Implememt -fdefer-type-errors (Trac #5624)
[ghc.git] / compiler / types / InstEnv.lhs
index c11218d..1e99775 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, 
-       instanceCantMatch, roughMatchTcs
+        DFunId, OverlapFlag(..),
+        ClsInst(..), pprInstance, pprInstanceHdr, pprInstances, 
+        instanceHead, mkLocalInstance, mkImportedInstance,
+        instanceDFunId, setInstanceDFunId, instanceRoughTcs,
+
+        InstEnv, emptyInstEnv, extendInstEnv, overwriteInstEnv, 
+        extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv', lookupInstEnv, instEnvElts,
+        classInstances, instanceBindFun,
+        instanceCantMatch, roughMatchTcs
     ) where
 
 #include "HsVersions.h"
@@ -29,40 +29,42 @@ import TcType
 import TyCon
 import Unify
 import Outputable
+import ErrUtils
 import BasicTypes
 import UniqFM
 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}
-type DFunId = Id
-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
-            , is_flag :: OverlapFlag   -- See detailed comments with
-                                       -- the decl of BasicTypes.OverlapFlag
+data ClsInst 
+  = ClsInst { 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
     }
+  deriving (Data, Typeable)
 \end{code}
 
 Note [Rough-match field]
@@ -78,11 +80,11 @@ 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -99,75 +101,95 @@ However, note that:
    (This is so that we can use the matching substitution to
     instantiate the dfun's context.)
 
+Note [Haddock assumptions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+For normal user-written instances, Haddock relies on
 
+ * the SrcSpan of
+ * the Name of
+ * the is_dfun of
+ * an Instance
+
+being equal to
+
+  * the SrcSpan of
+  * the instance head type of
+  * the InstDecl used to construct the Instance.
 
 \begin{code}
-instanceDFunId :: Instance -> DFunId
+instanceDFunId :: ClsInst -> DFunId
 instanceDFunId = is_dfun
 
-setInstanceDFunId :: Instance -> DFunId -> Instance
+setInstanceDFunId :: ClsInst -> DFunId -> ClsInst
 setInstanceDFunId ispec dfun
-   = ASSERT( idType dfun `tcEqType` 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
+   = 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 ClsInst 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]
+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 })
-  = ptext SLIT("instance") <+> ppr flag
-    <+> sep [pprThetaArrow theta, pprClassPred clas tys]
+pprInstanceHdr :: ClsInst -> SDoc
+-- Prints the ClsInst as an instance declaration
+pprInstanceHdr ispec@(ClsInst { is_flag = flag })
+  = ptext (sLit "instance") <+> ppr flag
+       <+> sep [pprThetaArrowTy theta, ppr res_ty]
   where
-    (_, theta, clas, tys) = instanceHead ispec
-       -- Print without the for-all, which the programmer doesn't write
+    dfun = is_dfun ispec
+    (_, theta, res_ty) = tcSplitSigmaTy (idType dfun)
+        -- 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], [PredType], Class, [Type])
-instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec))
+instanceHead :: ClsInst -> ([TyVar], ThetaType, Class, [Type])
+instanceHead ispec = (tvs, theta, cls, tys)
+   where
+     (tvs, theta, tau) = tcSplitSigmaTy (idType dfun)
+     (cls, tys)        = tcSplitDFunHead tau
+     dfun              = is_dfun ispec
 
-mkLocalInstance :: DFunId -> OverlapFlag -> Instance
+mkLocalInstance :: DFunId
+                -> OverlapFlag
+                -> 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 }
+  = ClsInst {  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)
 
 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 }
+  = ClsInst {  is_flag = oflag, is_dfun = dfun,
+                is_tvs = mkVarSet tvs, is_tys = tys,
+                is_cls = cls, is_tcs = mb_tcs }
   where
     (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
 
@@ -175,8 +197,8 @@ 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
@@ -302,18 +324,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
@@ -321,62 +343,83 @@ 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
+
+newtype ClsInstEnv 
+  = ClsIE [ClsInst]    -- The instances for a particular class, in any order
 
-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
+instance Outputable ClsInstEnv where
+  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 = cls_nm })
+  = addToUFM_C add inst_env cls_nm (ClsIE [ins_item])
+  where
+    add (ClsIE cur_insts) _ = ClsIE (ins_item : cur_insts)
+
+overwriteInstEnv :: InstEnv -> ClsInst -> InstEnv
+overwriteInstEnv inst_env ins_item@(ClsInst { is_cls = cls_nm, is_tys = tys })
+  = 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 (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,
+                                  is_dfun = dfun }) : rest)
+    -- Fast check for no match, uses the "rough match" fields
+      | instanceCantMatch rough_tcs mb_tcs
+      = item : replaceInst rest
+
+      | Just _ <- tcMatchTys tpl_tvs tpl_tys tys
+      = let (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
+        in ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs )        -- Check invariant
+           ins_item : rest
+
+      | otherwise
+      = item : replaceInst rest
 \end{code}
 
 
 %************************************************************************
-%*                                                                     *
-\subsection{Looking up an instance}
-%*                                                                     *
+%*                                                                      *
+        Looking up an instance
+%*                                                                      *
 %************************************************************************
 
 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
@@ -385,153 +428,231 @@ 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
+        -- Right ty     => Instantiate with this type
+        -- Left tv      => Instantiate with any type of this tyvar's kind
 
-type InstMatch = (Instance, InstTypes)
+type InstMatch = (ClsInst, InstTypes)
 \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
+A successful match is an 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
+        [Right ty, Left b]
+where the 'Left b' 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 | Right ty <- inst_tys]
+               noFlexiVar = all isRight inst_tys
+      _other -> Left $ ptext (sLit "instance not found") <+> (ppr $ mkTyConApp (classTyCon cls) tys)
+  where
+    isRight (Left  _) = False
+    isRight (Right _) = True
 
+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,
+                                 is_dfun = dfun }) : 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
-
-       -- Does not match, so next check whether the things unify
-       -- See Note [overlapping instances] above
-      | Incoherent <- oflag
+            (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
+
+        -- 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
-        case tcUnifyTys bind_fn tpl_tys tys of
-           Just _   -> find ms (item:us) rest
-           Nothing  -> find ms us        rest
+                 (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
+        case tcUnifyTys instanceBindFun tpl_tys tys of
+            Just _   -> find ms (item:us) rest
+            Nothing  -> find ms us        rest
+
+    ----------------
+    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
 
 ---------------
-bind_fn :: TyVar -> BindFlag
-bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
-          | otherwise                             = BindMe
-       -- 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]
-       -- 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 pattern-bound skolems.  For example we reject
-       --      g :: forall a => [a] -> Int
-       --      g x = op x
-       -- on the grounds that the correct instance depends on the instantiation of 'a'
+-- 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
+                   -> ([InstMatch],     -- Successful matches
+                       [ClsInst],      -- These don't match but do unify
+                       Bool)            -- True if error condition caused by
+                                        -- SafeHaskell condition.
+
+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)
 
 ---------------
+---------------
 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
 -- Add a new solution, knocking out strictly less specific ones
 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))
-               -- A beats B if A is more specific than B, and B admits overlap
-               -- I.e. if B can be instantiated to match A
-       where
-         overlap_ok = case is_flag instB of
-                       NoOverlap -> False
-                       _         -> True
+          = overlap_ok && 
+            isJust (tcMatchTys (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
+          where
+            -- Overlap permitted if *either* instance permits overlap
+            -- 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
 \end{code}
 
+
+%************************************************************************
+%*                                                                      *
+        Binding decisions
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+instanceBindFun :: TyVar -> BindFlag
+instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar tv = Skolem
+                   | otherwise                              = BindMe
+   -- Note [Binding when looking up instances]
+\end{code}
+
+Note [Binding when looking up instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When looking up in the instance environment, or family-instance environment,
+we are careful about multiple matches, as described above in 
+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]
+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
+on the grounds that the correct instance depends on the instantiation of 'a'