Fix treatment of hi-boot files and dfuns

Trac #16038 exposed the fact that TcRnDriver.checkHiBootIface
was creating a binding, in the module being compiled, for
   $fxBlah = $fBlah

 but $fxBlah was a /GlobalId/. But all bindings should be for
 /LocalIds/ else dependency analysis goes down the tubes.

* I added a CoreLint check that an occurrence of a GlobalId
  is not bound by an binding of a LocalId.  (There is already
  a binding-site check that no binding binds a GlobalId.)

* I refactored (and actually signficantly simplified) the
  tricky code for dfuns in checkHiBootIface to ensure that
  we get LocalIds for those boot-dfuns.

Alas, I then got "duplicate instance" messages when compiling
HsExpr. It turns out that this is a long-standing, but extremely
delicate, bug: even before this patch, if you compile HsExpr
with -ddump-tc-trace, you get "duplicate instance". Without
-ddump-tc-trace, it's OK.  What a mess!

The reason for the duplicate-instance is now explained in
Note [Loading your own hi-boot file] in LoadIface.  I fixed
it by a Gross Hack in LoadIface.loadInterface. This is at
least no worse than before.

But there should be a better way. I have opened #16081 for this.

5 files changed, 257 insertions, 198 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 8ab0fbfd80..b1b37c51be 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -2041,12 +2041,15 @@ lintUnliftedCoVar cv
 data LintEnv
   = LE { le_flags :: LintFlags       -- Linting the result of this pass
        , le_loc   :: [LintLocInfo]   -- Locations
-       , le_subst :: TCvSubst        -- Current type substitution; we also use this
-                                     -- to keep track of all the variables in scope,
-                                     -- both Ids and TyVars
-       , le_joins :: IdSet           -- Join points in scope that are valid
-                                     -- A subset of teh InScopeSet in le_subst
-                                     -- See Note [Join points]
+
+       , le_subst :: TCvSubst  -- Current type substitution
+                               -- We also use le_subst to keep track of
+                               -- /all variables/ in scope, both Ids and TyVars
+
+       , le_joins :: IdSet     -- Join points in scope that are valid
+                               -- A subset of the InScopeSet in le_subst
+                               -- See Note [Join points]
+
        , le_dynflags :: DynFlags     -- DynamicFlags
        }
 
@@ -2304,17 +2307,30 @@ applySubstCo :: InCoercion -> LintM OutCoercion
 applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
 
 lookupIdInScope :: Id -> LintM Id
-lookupIdInScope id
-  | not (mustHaveLocalBinding id)
-  = return id   -- An imported Id
-  | otherwise
-  = do  { subst <- getTCvSubst
-        ; case lookupInScope (getTCvInScope subst) id of
-                Just v  -> return v
-                Nothing -> do { addErrL out_of_scope
-                              ; return id } }
+lookupIdInScope id_occ
+  = do { subst <- getTCvSubst
+       ; case lookupInScope (getTCvInScope subst) id_occ of
+           Just id_bnd  -> do { checkL (not (bad_global id_bnd)) global_in_scope
+                              ; return id_bnd }
+           Nothing -> do { checkL (not is_local) local_out_of_scope
+                         ; return id_occ } }
   where
-    out_of_scope = pprBndr LetBind id <+> text "is out of scope"
+    is_local = mustHaveLocalBinding id_occ
+    local_out_of_scope = text "Out of scope:" <+> pprBndr LetBind id_occ
+    global_in_scope    = hang (text "Occurrence is GlobalId, but binding is LocalId")
+                            2 (pprBndr LetBind id_occ)
+    bad_global id_bnd = isGlobalId id_occ
+                     && isLocalId id_bnd
+                     && not (isWiredInName (idName id_occ))
+       -- 'bad_global' checks for the case where an /occurrence/ is
+       -- a GlobalId, but there is an enclosing binding fora a LocalId.
+       -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr,
+       --     but GHCi adds GlobalIds from the interactive context.  These
+       --     are fine; hence the test (isLocalId id == isLocalId v)
+       -- NB: when compiling Control.Exception.Base, things like absentError
+       --     are defined locally, but appear in expressions as (global)
+       --     wired-in Ids after worker/wrapper
+       --     So we simply disable the test in this case
 
 lookupJoinId :: Id -> LintM (Maybe JoinArity)
 -- Look up an Id which should be a join point, valid here
@@ -2325,14 +2341,11 @@ lookupJoinId id
             Just id' -> return (isJoinId_maybe id')
             Nothing  -> return Nothing }
 
-lintTyCoVarInScope :: Var -> LintM ()
-lintTyCoVarInScope v = lintInScope (text "is out of scope") v
-
-lintInScope :: SDoc -> Var -> LintM ()
-lintInScope loc_msg var =
- do { subst <- getTCvSubst
-    ; lintL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
-             (hsep [pprBndr LetBind var, loc_msg]) }
+lintTyCoVarInScope :: TyCoVar -> LintM ()
+lintTyCoVarInScope var
+  = do { subst <- getTCvSubst
+       ; lintL (var `isInScope` subst)
+               (pprBndr LetBind var <+> text "is out of scope") }
 
 ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
 -- check ty2 is subtype of ty1 (ie, has same structure but usage
diff --git a/compiler/iface/LoadIface.hs b/compiler/iface/LoadIface.hs
index bff507f973..87a6beb3ff 100644
--- a/compiler/iface/LoadIface.hs
+++ b/compiler/iface/LoadIface.hs
@@ -418,15 +418,7 @@ loadInterface doc_str mod from
         -- READ THE MODULE IN
         ; read_result <- case (wantHiBootFile dflags eps mod from) of
                            Failed err             -> return (Failed err)
-                           Succeeded hi_boot_file ->
-                            -- Stoutly warn against an EPS-updating import
-                            -- of one's own boot file! (one-shot only)
-                            --See Note [Do not update EPS with your own hi-boot]
-                            -- in MkIface.
-                            WARN( hi_boot_file &&
-                                  fmap fst (if_rec_types gbl_env) == Just mod,
-                                  ppr mod )
-                            computeInterface doc_str hi_boot_file mod
+                           Succeeded hi_boot_file -> computeInterface doc_str hi_boot_file mod
         ; case read_result of {
             Failed err -> do
                 { let fake_iface = emptyModIface mod
@@ -488,9 +480,20 @@ loadInterface doc_str mod from
                               }
                }
 
-        ; updateEps_  $ \ eps ->
+        ; let bad_boot = mi_boot iface && fmap fst (if_rec_types gbl_env) == Just mod
+                            -- Warn warn against an EPS-updating import
+                            -- of one's own boot file! (one-shot only)
+                            -- See Note [Loading your own hi-boot file]
+                            -- in MkIface.
+
+        ; WARN ( bad_boot, ppr mod )
+          updateEps_  $ \ eps ->
            if elemModuleEnv mod (eps_PIT eps) || is_external_sig dflags iface
-           then eps else
+                then eps
+           else if bad_boot
+                -- See Note [Loading your own hi-boot file]
+                then eps { eps_PTE = addDeclsToPTE (eps_PTE eps) new_eps_decls }
+           else
                 eps {
                   eps_PIT          = extendModuleEnv (eps_PIT eps) mod final_iface,
                   eps_PTE          = addDeclsToPTE   (eps_PTE eps) new_eps_decls,
@@ -525,26 +528,56 @@ loadInterface doc_str mod from
         ; return (Succeeded res)
     }}}}
 
+{- Note [Loading your own hi-boot file]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally speaking, when compiling module M, we should not
+load M.hi boot into the EPS.  After all, we are very shortly
+going to have full information about M.  Moreover, see
+Note [Do not update EPS with your own hi-boot] in MkIface.
+
+But there is a HORRIBLE HACK here.
+
+* At the end of tcRnImports, we call checkFamInstConsistency to
+  check consistency of imported type-family instances
+  See Note [The type family instance consistency story] in FamInst
+
+* Alas, those instances may refer to data types defined in M,
+  if there is a M.hs-boot.
+
+* And that means we end up loading M.hi-boot, because those
+  data types are not yet in the type environment.
+
+But in this wierd case, /all/ we need is the types. We don't need
+instances, rules etc.  And if we put the instances in the EPS
+we get "duplicate instance" warnings when we compile the "real"
+instance in M itself.  Hence the strange business of just updateing
+the eps_PTE.
+
+This really happens in practice.  The module HsExpr.hs gets
+"duplicate instance" errors if this hack is not present.
+
+This is a mess.
+
+
+Note [HPT space leak] (#15111)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In IfL, we defer some work until it is demanded using forkM, such
+as building TyThings from IfaceDecls. These thunks are stored in
+the ExternalPackageState, and they might never be poked.  If we're
+not careful, these thunks will capture the state of the loaded
+program when we read an interface file, and retain all that data
+for ever.
+
+Therefore, when loading a package interface file , we use a "clean"
+version of the HscEnv with all the data about the currently loaded
+program stripped out. Most of the fields can be panics because
+we'll never read them, but hsc_HPT needs to be empty because this
+interface will cause other interfaces to be loaded recursively, and
+when looking up those interfaces we use the HPT in loadInterface.
+We know that none of the interfaces below here can refer to
+home-package modules however, so it's safe for the HPT to be empty.
+-}
 
-
--- Note [HPT space leak] (#15111)
---
--- In IfL, we defer some work until it is demanded using forkM, such
--- as building TyThings from IfaceDecls. These thunks are stored in
--- the ExternalPackageState, and they might never be poked.  If we're
--- not careful, these thunks will capture the state of the loaded
--- program when we read an interface file, and retain all that data
--- for ever.
---
--- Therefore, when loading a package interface file , we use a "clean"
--- version of the HscEnv with all the data about the currently loaded
--- program stripped out. Most of the fields can be panics because
--- we'll never read them, but hsc_HPT needs to be empty because this
--- interface will cause other interfaces to be loaded recursively, and
--- when looking up those interfaces we use the HPT in loadInterface.
--- We know that none of the interfaces below here can refer to
--- home-package modules however, so it's safe for the HPT to be empty.
---
 dontLeakTheHPT :: IfL a -> IfL a
 dontLeakTheHPT thing_inside = do
   let
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 144b315bed..5ad27db06e 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -84,57 +84,61 @@ defined in module B.
 How do we ensure that we maintain the necessary consistency?
 
 * Call a module which defines at least one type family instance a
-"family instance module". This flag `mi_finsts` is recorded in the
-interface file.
+  "family instance module". This flag `mi_finsts` is recorded in the
+  interface file.
 
 * For every module we calculate the set of all of its direct and
-indirect dependencies that are family instance modules. This list
-`dep_finsts` is also recorded in the interface file so we can compute
-this list for a module from the lists for its direct dependencies.
+  indirect dependencies that are family instance modules. This list
+  `dep_finsts` is also recorded in the interface file so we can compute
+  this list for a module from the lists for its direct dependencies.
 
 * When type checking a module M we check consistency of all the type
-family instances that are either provided by its `dep_finsts` or
-defined in the module M itself. This is a pairwise check, i.e., for
-every pair of instances we must check that they are consistent.
+  family instances that are either provided by its `dep_finsts` or
+  defined in the module M itself. This is a pairwise check, i.e., for
+  every pair of instances we must check that they are consistent.
 
-- For family instances coming from `dep_finsts`, this is checked in
-checkFamInstConsistency, called from tcRnImports. See Note
-[Checking family instance consistency] for details on this check (and
-in particular how we avoid having to do all these checks for every
-module we compile).
+  - For family instances coming from `dep_finsts`, this is checked in
+    checkFamInstConsistency, called from tcRnImports. See Note
+    [Checking family instance consistency] for details on this check
+    (and in particular how we avoid having to do all these checks for
+    every module we compile).
 
-- That leaves checking the family instances defined in M itself
-against instances defined in either M or its `dep_finsts`. This is
-checked in `tcExtendLocalFamInstEnv'.
+  - That leaves checking the family instances defined in M itself
+    against instances defined in either M or its `dep_finsts`. This is
+    checked in `tcExtendLocalFamInstEnv'.
 
-There are two subtle points in this scheme which have not been
+There are four subtle points in this scheme which have not been
 addressed yet.
 
 * We have checked consistency of the family instances *defined* by M
-or its imports, but this is not by definition the same thing as the
-family instances *used* by M or its imports.  Specifically, we need to
-ensure when we use a type family instance while compiling M that this
-instance was really defined from either M or one of its imports,
-rather than being an instance that we happened to know about from
-reading an interface file in the course of compiling an unrelated
-module. Otherwise, we'll end up with no record of the fact that M
-depends on this family instance and type safety will be compromised.
-See #13102.
+  or its imports, but this is not by definition the same thing as the
+  family instances *used* by M or its imports.  Specifically, we need to
+  ensure when we use a type family instance while compiling M that this
+  instance was really defined from either M or one of its imports,
+  rather than being an instance that we happened to know about from
+  reading an interface file in the course of compiling an unrelated
+  module. Otherwise, we'll end up with no record of the fact that M
+  depends on this family instance and type safety will be compromised.
+  See #13102.
 
 * It can also happen that M uses a function defined in another module
-which is not transitively imported by M. Examples include the
-desugaring of various overloaded constructs, and references inserted
-by Template Haskell splices. If that function's definition makes use
-of type family instances which are not checked against those visible
-from M, type safety can again be compromised. See #13251.
+  which is not transitively imported by M. Examples include the
+  desugaring of various overloaded constructs, and references inserted
+  by Template Haskell splices. If that function's definition makes use
+  of type family instances which are not checked against those visible
+  from M, type safety can again be compromised. See #13251.
 
 * When a module C imports a boot module B.hs-boot, we check that C's
-type family instances are compatible with those visible from
-B.hs-boot. However, C will eventually be linked against a different
-module B.hs, which might define additional type family instances which
-are inconsistent with C's. This can also lead to loss of type safety.
-See #9562.
-
+  type family instances are compatible with those visible from
+  B.hs-boot. However, C will eventually be linked against a different
+  module B.hs, which might define additional type family instances which
+  are inconsistent with C's. This can also lead to loss of type safety.
+  See #9562.
+
+* The call to checkFamConsistency for imported functions occurs very
+  early (in tcRnImports) and that causes problems if the imported
+  instances use type declared in the module being compiled.
+  See Note [Loading your own hi-boot file] in LoadIface.
 -}
 
 {-
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 0a6d7e5bb2..524fa11286 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -675,88 +675,79 @@ checkHiBootIface tcg_env boot_info
              , tcg_type_env = local_type_env
              , tcg_exports  = local_exports } <- tcg_env
   = do  { -- This code is tricky, see Note [DFun knot-tying]
-        ; let boot_dfuns = filter isDFunId (typeEnvIds (md_types boot_details))
-              type_env'  = extendTypeEnvWithIds local_type_env boot_dfuns
-          -- Why the seq?  Without, we will put a TypeEnv thunk in
-          -- tcg_type_env_var.  That thunk will eventually get
-          -- forced if we are typechecking interfaces, but that
-          -- is no good if we are trying to typecheck the very
-          -- DFun we were going to put in.
-          -- TODO: Maybe setGlobalTypeEnv should be strict.
-        ; tcg_env <- type_env' `seq` setGlobalTypeEnv tcg_env type_env'
-        ; dfun_prs <- checkHiBootIface' local_insts type_env'
+        ; dfun_prs <- checkHiBootIface' local_insts local_type_env
                                         local_exports boot_details
-        ; let dfun_binds = listToBag [ mkVarBind boot_dfun (nlHsVar dfun)
-                                     | (boot_dfun, dfun) <- dfun_prs ]
 
-        ; return tcg_env { tcg_binds = binds `unionBags` dfun_binds } }
+        -- Now add the boot-dfun bindings  $fxblah = $fblah
+        -- to (a) the type envt, and (b) the top-level bindings
+        ; let boot_dfuns = map fst dfun_prs
+              type_env'  = extendTypeEnvWithIds local_type_env boot_dfuns
+              dfun_binds = listToBag [ mkVarBind boot_dfun (nlHsVar dfun)
+                                     | (boot_dfun, dfun) <- dfun_prs ]
+              tcg_env_w_binds
+                = tcg_env { tcg_binds = binds `unionBags` dfun_binds }
+
+        ; type_env' `seq`
+             -- Why the seq?  Without, we will put a TypeEnv thunk in
+             -- tcg_type_env_var.  That thunk will eventually get
+             -- forced if we are typechecking interfaces, but that
+             -- is no good if we are trying to typecheck the very
+             -- DFun we were going to put in.
+             -- TODO: Maybe setGlobalTypeEnv should be strict.
+          setGlobalTypeEnv tcg_env_w_binds type_env' }
 
   | otherwise = panic "checkHiBootIface: unreachable code"
 
--- Note [DFun knot-tying]
--- ~~~~~~~~~~~~~~~~~~~~~~
--- The 'SelfBootInfo' that is fed into 'checkHiBootIface' comes
--- from typechecking the hi-boot file that we are presently
--- implementing.  Suppose we are typechecking the module A:
--- when we typecheck the hi-boot file, whenever we see an
--- identifier A.T, we knot-tie this identifier to the
--- *local* type environment (via if_rec_types.)  The contract
--- then is that we don't *look* at 'SelfBootInfo' until
--- we've finished typechecking the module and updated the
--- type environment with the new tycons and ids.
---
--- This most works well, but there is one problem: DFuns!
--- In general, it's not possible to know a priori what an
--- hs-boot file named a DFun (see Note [DFun impedance matching]),
--- so we look at the ClsInsts from the boot file to figure out
--- what DFuns to add to the type environment.  But we're not
--- allowed to poke the DFuns of the ClsInsts in the SelfBootInfo
--- until we've added the DFuns to the type environment.  A
--- Gordian knot!
---
--- We cut the knot by a little trick: we first *unconditionally*
--- add all of the boot-declared DFuns to the type environment
--- (so that knot tying works, see Trac #4003), without the
--- actual bindings for them.  Then, we compute the impedance
--- matching bindings, and add them to the environment.
---
--- There is one subtlety to doing this: we have to get the
--- DFuns from md_types, not md_insts, even though involves
--- filtering a bunch of TyThings we don't care about.  The
--- reason is only the TypeEnv in md_types has the actual
--- Id we want to add to the environment; the DFun fields
--- in md_insts are typechecking thunks that will attempt to
--- go through if_rec_types to lookup the real Id... but
--- that's what we're trying to setup right now.
+{- Note [DFun impedance matching]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We return a list of "impedance-matching" bindings for the dfuns
+defined in the hs-boot file, such as
+          $fxEqT = $fEqT
+We need these because the module and hi-boot file might differ in
+the name it chose for the dfun: the name of a dfun is not
+uniquely determined by its type; there might be multiple dfuns
+which, individually, would map to the same name (in which case
+we have to disambiguate them.)  There's no way for the hi file
+to know exactly what disambiguation to use... without looking
+at the hi-boot file itself.
+
+In fact, the names will always differ because we always pick names
+prefixed with "$fx" for boot dfuns, and "$f" for real dfuns
+(so that this impedance matching is always possible).
+
+Note [DFun knot-tying]
+~~~~~~~~~~~~~~~~~~~~~~
+The 'SelfBootInfo' that is fed into 'checkHiBootIface' comes from
+typechecking the hi-boot file that we are presently implementing.
+Suppose we are typechecking the module A: when we typecheck the
+hi-boot file, whenever we see an identifier A.T, we knot-tie this
+identifier to the *local* type environment (via if_rec_types.)  The
+contract then is that we don't *look* at 'SelfBootInfo' until we've
+finished typechecking the module and updated the type environment with
+the new tycons and ids.
+
+This most works well, but there is one problem: DFuns!  We do not want
+to look at the mb_insts of the ModDetails in SelfBootInfo, because a
+dfun in one of those ClsInsts is gotten (in TcIface.tcIfaceInst) by a
+(lazily evaluated) lookup in the if_rec_types.  We could extend the
+type env, do a setGloblaTypeEnv etc; but that all seems very indirect.
+It is much more directly simply to extract the DFunIds from the
+md_types of the SelfBootInfo.
+
+See Trac #4003, #16038 for why we need to take care here.
+-}
 
 checkHiBootIface' :: [ClsInst] -> TypeEnv -> [AvailInfo]
                   -> ModDetails -> TcM [(Id, Id)]
 -- Variant which doesn't require a full TcGblEnv; you could get the
 -- local components from another ModDetails.
---
--- Note [DFun impedance matching]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- We return a list of "impedance-matching" bindings for the dfuns
--- defined in the hs-boot file, such as
---           $fxEqT = $fEqT
--- We need these because the module and hi-boot file might differ in
--- the name it chose for the dfun: the name of a dfun is not
--- uniquely determined by its type; there might be multiple dfuns
--- which, individually, would map to the same name (in which case
--- we have to disambiguate them.)  There's no way for the hi file
--- to know exactly what disambiguation to use... without looking
--- at the hi-boot file itself.
---
--- In fact, the names will always differ because we always pick names
--- prefixed with "$fx" for boot dfuns, and "$f" for real dfuns
--- (so that this impedance matching is always possible).
-
 checkHiBootIface'
         local_insts local_type_env local_exports
-        (ModDetails { md_insts = boot_insts, md_fam_insts = boot_fam_insts,
-                      md_types = boot_type_env, md_exports = boot_exports })
+        (ModDetails { md_types = boot_type_env
+                    , md_fam_insts = boot_fam_insts
+                    , md_exports = boot_exports })
   = do  { traceTc "checkHiBootIface" $ vcat
-             [ ppr boot_type_env, ppr boot_insts, ppr boot_exports]
+             [ ppr boot_type_env, ppr boot_exports]
 
                 -- Check the exports of the boot module, one by one
         ; mapM_ check_export boot_exports
@@ -771,16 +762,22 @@ checkHiBootIface'
 
                 -- Check instance declarations
                 -- and generate an impedance-matching binding
-        ; mb_dfun_prs <- mapM check_inst boot_insts
+        ; mb_dfun_prs <- mapM check_cls_inst boot_dfuns
 
         ; failIfErrsM
 
         ; return (catMaybes mb_dfun_prs) }
 
   where
+    boot_dfun_names = map idName boot_dfuns
+    boot_dfuns      = filter isDFunId $ typeEnvIds boot_type_env
+       -- NB: boot_dfuns is /not/ defined thus: map instanceDFunId md_insts
+       --     We don't want to look at md_insts!
+       --     Why not?  See Note [DFun knot-tying]
+
     check_export boot_avail     -- boot_avail is exported by the boot iface
-      | name `elem` dfun_names = return ()
-      | isWiredInName name     = return ()      -- No checking for wired-in names.  In particular,
+      | name `elem` boot_dfun_names = return ()
+      | isWiredInName name          = return () -- No checking for wired-in names.  In particular,
                                                 -- 'error' is handled by a rather gross hack
                                                 -- (see comments in GHC.Err.hs-boot)
 
@@ -808,39 +805,53 @@ checkHiBootIface'
                           Nothing    -> [name]
                           Just avail -> availNames boot_avail `minusList` availNames avail
 
-    dfun_names = map getName boot_insts
-
     local_export_env :: NameEnv AvailInfo
     local_export_env = availsToNameEnv local_exports
 
-    check_inst :: ClsInst -> TcM (Maybe (Id, Id))
+    check_cls_inst :: DFunId -> TcM (Maybe (Id, Id))
         -- Returns a pair of the boot dfun in terms of the equivalent
         -- real dfun. Delicate (like checkBootDecl) because it depends
         -- on the types lining up precisely even to the ordering of
         -- the type variables in the foralls.
-    check_inst boot_inst
-        = case [dfun | inst <- local_insts,
-                       let dfun = instanceDFunId inst,
-                       idType dfun `eqType` boot_dfun_ty ] of
-            [] -> do { traceTc "check_inst" $ vcat
-                          [ text "local_insts"  <+> vcat (map (ppr . idType . instanceDFunId) local_insts)
-                          , text "boot_inst"    <+> ppr boot_inst
-                          , text "boot_dfun_ty" <+> ppr boot_dfun_ty
-                          ]
-                     ; addErrTc (instMisMatch True boot_inst)
-                     ; return Nothing }
-            (dfun:_) -> return (Just (local_boot_dfun, dfun))
-                     where
-                        local_boot_dfun = Id.mkExportedVanillaId boot_dfun_name (idType dfun)
-                           -- Name from the /boot-file/ ClsInst, but type from the dfun
-                           -- defined in /this module/.  That ensures that the TyCon etc
-                           -- inside the type are the ones defined in this module, not
-                           -- the ones gotten from the hi-boot file, which may have
-                           -- a lot less info (Trac #T8743, comment:10).
-        where
-          boot_dfun      = instanceDFunId boot_inst
+    check_cls_inst boot_dfun
+      | (real_dfun : _) <- find_real_dfun boot_dfun
+      , let local_boot_dfun = Id.mkExportedVanillaId
+                                  (idName boot_dfun) (idType real_dfun)
+      = return (Just (local_boot_dfun, real_dfun))
+          -- Two tricky points here:
+          --
+          -- * The local_boot_fun should have a Name from the /boot-file/,
+          --   but type from the dfun defined in /this module/.
+          --   That ensures that the TyCon etc inside the type are
+          --   the ones defined in this module, not the ones gotten
+          --   from the hi-boot file, which may have a lot less info
+          --   (Trac #T8743, comment:10).
+          --
+          --  * The DFunIds from boot_details are /GlobalIds/, because
+          --    they come from typechecking M.hi-boot.
+          --    But all bindings in this module should be for /LocalIds/,
+          --    otherwise dependency analysis fails (Trac #16038). This
+          --    is another reason for using mkExportedVanillaId, rather
+          --    that modifying boot_dfun, to make local_boot_fun.
+
+      | otherwise
+      = setSrcSpan (getLoc (getName boot_dfun)) $
+        do { traceTc "check_cls_inst" $ vcat
+                [ text "local_insts"  <+>
+                     vcat (map (ppr . idType . instanceDFunId) local_insts)
+                , text "boot_dfun_ty" <+> ppr (idType boot_dfun) ]
+
+           ; addErrTc (instMisMatch boot_dfun)
+           ; return Nothing }
+
+    find_real_dfun :: DFunId -> [DFunId]
+    find_real_dfun boot_dfun
+       = [dfun | inst <- local_insts
+               , let dfun = instanceDFunId inst
+               , idType dfun `eqType` boot_dfun_ty ]
+       where
           boot_dfun_ty   = idType boot_dfun
-          boot_dfun_name = idName boot_dfun
+
 
 -- In general, to perform these checks we have to
 -- compare the TyThing from the .hi-boot file to the TyThing
@@ -1306,12 +1317,10 @@ bootMisMatch is_boot extra_info real_thing boot_thing
             extra_info
           ]
 
-instMisMatch :: Bool -> ClsInst -> SDoc
-instMisMatch is_boot inst
-  = hang (ppr inst)
-       2 (text "is defined in the" <+>
-        (if is_boot then text "hs-boot" else text "hsig")
-       <+> text "file, but not in the module itself")
+instMisMatch :: DFunId -> SDoc
+instMisMatch dfun
+  = hang (text "instance" <+> ppr (idType dfun))
+       2 (text "is defined in the hs-boot file, but not in the module itself")
 
 {-
 ************************************************************************
diff --git a/testsuite/tests/driver/T14075/T14075.stderr b/testsuite/tests/driver/T14075/T14075.stderr
index 0493a96f12..9c7bb7e359 100644
--- a/testsuite/tests/driver/T14075/T14075.stderr
+++ b/testsuite/tests/driver/T14075/T14075.stderr
@@ -1,7 +1,7 @@
 
-F.hs:1:1: error:
-    instance O.O F.F -- Defined at F.hs-boot:6:10
-      is defined in the hs-boot file, but not in the module itself
-
 F.hs-boot:5:1: error:
     ‘F.F’ is exported by the hs-boot file, but not exported by the module
+
+F.hs-boot:6:10: error:
+    instance O.O F.F
+      is defined in the hs-boot file, but not in the module itself