Rewrite Backpack comments on never-exported TyThings.

Summary:
While thesing, I realized this part of the implementation
didn't make very much sense, so I started working on some
documentation updates to try to make things more explainable.

The new docs are organized around the idea of a
"never exported TyThing" (a non-implicit TyThing that never
occurs in the export list of a module).  I also removed
some outdated information that predated the change of
ModIface to store Names rather than OccNames.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Reviewers: simonpj, bgamari, austin

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2989

4 files changed, 127 insertions, 101 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index b7d4623bef..a6d6eddf49 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -71,7 +71,7 @@ failWithRn doc = do
     writeTcRef errs_var (errs `snocBag` mkPlainErrMsg dflags noSrcSpan doc)
     failM
 
--- | What we have a generalized ModIface, which corresponds to
+-- | What we have is a generalized ModIface, which corresponds to
 -- a module that looks like p[A=<A>]:B.  We need a *specific* ModIface, e.g.
 -- p[A=q():A]:B (or maybe even p[A=<B>]:B) which we load
 -- up (either to merge it, or to just use during typechecking).
@@ -304,19 +304,50 @@ rnIfaceGlobal n = do
                     ]
                 Just n' -> return n'
 
--- | Rename an implicit name, e.g., a DFun or default method.
+-- | Rename an implicit name, e.g., a DFun or coercion axiom.
 -- Here is where we ensure that DFuns have the correct module as described in
--- Note [Bogus DFun renamings].
-rnIfaceImplicit :: Name -> ShIfM Name
-rnIfaceImplicit name = do
+-- Note [rnIfaceNeverExported].
+rnIfaceNeverExported :: Name -> ShIfM Name
+rnIfaceNeverExported name = do
     hmap <- getHoleSubst
     dflags <- getDynFlags
     iface_semantic_mod <- fmap sh_if_semantic_module getGblEnv
     let m = renameHoleModule dflags hmap $ nameModule name
-    -- Doublecheck that this DFun was, indeed, locally defined.
+    -- Doublecheck that this DFun/coercion axiom was, indeed, locally defined.
     MASSERT2( iface_semantic_mod == m, ppr iface_semantic_mod <+> ppr m )
     setNameModule (Just m) name
 
+-- Note [rnIfaceNeverExported]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- For the high-level overview, see
+-- Note [Handling never-exported TyThings under Backpack]
+--
+-- When we see a reference to an entity that was defined in a signature,
+-- 'rnIfaceGlobal' relies on the identifier in question being part of the
+-- exports of the implementing 'ModIface', so that we can use the exports to
+-- decide how to rename the identifier.  Unfortunately, references to 'DFun's
+-- and 'CoAxiom's will run into trouble under this strategy, because they are
+-- never exported.
+--
+-- Let us consider first what should happen in the absence of promotion.  In
+-- this setting, a reference to a 'DFun' or a 'CoAxiom' can only occur inside
+-- the signature *that is defining it* (as there are no Core terms in
+-- typechecked-only interface files, there's no way for a reference to occur
+-- besides from the defining 'ClsInst' or closed type family).  Thus,
+-- it doesn't really matter what names we give the DFun/CoAxiom, as long
+-- as it's consistent between the declaration site and the use site.
+--
+-- We have to make sure that these bogus names don't get propagated,
+-- but it is fine: see Note [Signature merging DFuns] for the fixups
+-- to the names we do before writing out the merged interface.
+-- (It's even easier for instantiation, since the DFuns all get
+-- dropped entirely; the instances are reexported implicitly.)
+--
+-- Unfortunately, this strategy is not enough in the presence of promotion
+-- (see bug #13149), where modules which import the signature may make
+-- reference to their coercions.  It's not altogether clear how to
+-- fix this case, but it is definitely a bug!
+
 -- PILES AND PILES OF BOILERPLATE
 
 -- | Rename an 'IfaceClsInst', with special handling for an associated
@@ -326,67 +357,7 @@ rnIfaceClsInst cls_inst = do
     n <- rnIfaceGlobal (ifInstCls cls_inst)
     tys <- mapM rnMaybeIfaceTyCon (ifInstTys cls_inst)
 
-    -- Note [Bogus DFun renamings]
-    -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-    -- Every 'IfaceClsInst' is associated with a DFun; in fact, when
-    -- we are typechecking only, it is the ONLY place a DFun Id
-    -- can appear.  This DFun must refer to a DFun that is defined
-    -- elsewhere in the 'ModIface'.
-    --
-    -- Unfortunately, DFuns are not exported (don't appear in
-    -- mi_exports), so we can't look at the exports (as we do in
-    -- rnIfaceGlobal) to rename it.
-    --
-    -- We have to rename it to *something*.  So what we do depends
-    -- on the situation:
-    --
-    --  * If the instance wasn't defined in a signature, the DFun
-    --    have a name like p[A=<A>]:B.$fShowFoo.  This is the
-    --    easy case: just apply the module substitution to the
-    --    unit id and go our merry way.
-    --
-    --  * If the instance was defined in a signature, we are in
-    --    an interesting situation.  Suppose we are instantiating
-    --    the signature:
-    --
-    --      signature H where
-    --          instance F T           -- {H.$fxFT}
-    --      module H where
-    --          instance F T where ... -- p[]:H.$fFT
-    --
-    --    In an ideal world, we would map {H.$fxFT} to p[]:H.$fFT.
-    --    But we have no idea what the correct DFun is: the OccNames
-    --    don't match up.  Nor do we really want to wire up {H.$fxFT}
-    --    to p[]:H.$fFT: we'd rather have it point at the DFun
-    --    from the *signature's* interface, and use that type to
-    --    find the actual instance we want to compare against.
-    --
-    --    So, to handle this case, we have to do several things:
-    --
-    --      * In 'rnIfaceClsInst', we just blindly rename the
-    --        the identifier to something that looks vaguely plausible.
-    --        In the instantiating case, we just map {H.$fxFT}
-    --        to p[]:H.$fxFT.  In the merging case, we map
-    --        {H.$fxFT} to {H2.$fxFT}.
-    --
-    --      * In 'lookupIfaceTop', we arrange for the top-level DFun
-    --        to be assigned the very same identifier we picked
-    --        during renaming (p[]:H.$fxFT)
-    --
-    --      * Finally, in 'tcIfaceInstWithDFunTypeEnv', we make sure
-    --        to grab the correct 'TyThing' for the DFun directly
-    --        from the local type environment (which was constructed
-    --        using 'Name's from 'lookupIfaceTop').
-    --
-    --    It's all a bit of a giant Rube Goldberg machine, but it
-    --    seems to work!  Note that the name we pick here doesn't
-    --    really matter, since we throw it out shortly after
-    --    (for merging, we rename all of the DFuns so that they
-    --    are unique; for instantiation, the final interface never
-    --    mentions DFuns since they are implicitly exported. See
-    --    Note [Signature merging DFuns])  The important thing is that it's
-    --    consistent everywhere.
-    dfun <- rnIfaceImplicit (ifDFun cls_inst)
+    dfun <- rnIfaceNeverExported (ifDFun cls_inst)
     return cls_inst { ifInstCls = n
                     , ifInstTys = tys
                     , ifDFun = dfun
@@ -409,9 +380,9 @@ rnIfaceDecl' (fp, decl) = (,) fp <$> rnIfaceDecl decl
 rnIfaceDecl :: Rename IfaceDecl
 rnIfaceDecl d@IfaceId{} = do
             name <- case ifIdDetails d of
-                      IfDFunId -> rnIfaceImplicit (ifName d)
+                      IfDFunId -> rnIfaceNeverExported (ifName d)
                       _ | isDefaultMethodOcc (occName (ifName d))
-                        -> rnIfaceImplicit (ifName d)
+                        -> rnIfaceNeverExported (ifName d)
                         | otherwise -> rnIfaceGlobal (ifName d)
             ty <- rnIfaceType (ifType d)
             details <- rnIfaceIdDetails (ifIdDetails d)
@@ -466,7 +437,7 @@ rnIfaceDecl d@IfaceClass{} = do
                      , ifSigs = sigs
                      }
 rnIfaceDecl d@IfaceAxiom{} = do
-            name <- rnIfaceImplicit (ifName d)
+            name <- rnIfaceNeverExported (ifName d)
             tycon <- rnIfaceTyCon (ifTyCon d)
             ax_branches <- mapM rnIfaceAxBranch (ifAxBranches d)
             return d { ifName = name
@@ -497,7 +468,7 @@ rnIfaceDecl d@IfacePatSyn{} =  do
 
 rnIfaceFamTyConFlav :: Rename IfaceFamTyConFlav
 rnIfaceFamTyConFlav (IfaceClosedSynFamilyTyCon (Just (n, axs)))
-    = IfaceClosedSynFamilyTyCon . Just <$> ((,) <$> rnIfaceImplicit n
+    = IfaceClosedSynFamilyTyCon . Just <$> ((,) <$> rnIfaceNeverExported n
                                                 <*> mapM rnIfaceAxBranch axs)
 rnIfaceFamTyConFlav flav = pure flav
 
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 988860f4af..c0b84640b0 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -293,7 +293,8 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
     ignore_prags <- goptM Opt_IgnoreInterfacePragmas
     -- Build the initial environment
     -- NB: Don't include dfuns here, because we don't want to
-    -- serialize them out.  See Note [Bogus DFun renamings] in RnModIface
+    -- serialize them out.  See Note [rnIfaceNeverExported] in RnModIface
+    -- NB: But coercions are OK, because they will have the right OccName.
     let mk_decl_env decls
             = mkOccEnv [ (getOccName decl, decl)
                        | decl <- decls
@@ -312,7 +313,7 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
 
     -- OK, now typecheck each ModIface using this environment
     details <- forM ifaces $ \iface -> do
-        -- See Note [The implicit TypeEnv]
+        -- See Note [Resolving never-exported Names in TcIface]
         type_env <- fixM $ \type_env -> do
             setImplicitEnvM type_env $ do
                 decls <- loadDecls ignore_prags (mi_decls iface)
@@ -345,19 +346,19 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
 -- implementing module, which we will use to give our top-level
 -- declarations the correct 'Name's even when the implementor
 -- provided them with a reexport, and (2) we have to deal with
--- DFun silliness (see Note [Bogus DFun renamings])
+-- DFun silliness (see Note [rnIfaceNeverExported])
 typecheckIfaceForInstantiate :: NameShape -> ModIface -> IfM lcl ModDetails
 typecheckIfaceForInstantiate nsubst iface =
   initIfaceLclWithSubst (mi_semantic_module iface)
                         (text "typecheckIfaceForInstantiate")
                         (mi_boot iface) nsubst $ do
     ignore_prags <- goptM Opt_IgnoreInterfacePragmas
-    -- See Note [The implicit TypeEnv]
+    -- See Note [Resolving never-exported Names in TcIface]
     type_env <- fixM $ \type_env -> do
         setImplicitEnvM type_env $ do
             decls     <- loadDecls ignore_prags (mi_decls iface)
             return (mkNameEnv decls)
-    -- See Note [Bogus DFun renamings]
+    -- See Note [rnIfaceNeverExported]
     setImplicitEnvM type_env $ do
     insts     <- mapM tcIfaceInst (mi_insts iface)
     fam_insts <- mapM tcIfaceFamInst (mi_fam_insts iface)
@@ -374,31 +375,38 @@ typecheckIfaceForInstantiate nsubst iface =
                         , md_exports   = exports
                         }
 
--- Note [The implicit TypeEnv]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Note [Resolving never-exported Names in TcIface]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- For the high-level overview, see
+-- Note [Handling never-exported TyThings under Backpack]
+--
 -- As described in 'typecheckIfacesForMerging', the splendid innovation
 -- of signature merging is to rewrite all Names in each of the signatures
 -- we are merging together to a pre-merged structure; this is the key
 -- ingredient that lets us solve some problems when merging type
 -- synonyms.
 --
--- However in the case of DFuns and CoAxioms, this strategy goes
--- *too far*.  In particular, the reference to a DFun or CoAxiom in
--- an instance declaration or closed type family (respectively) will
--- refer to the merged declaration.  However, checkBootDeclM only
--- ever looks at the embedded structure when performing its comparison;
--- by virtue of the fact that everything's been pointed to the merged
+-- However, when a 'Name' refers to a NON-exported entity, as is the
+-- case with the DFun of a ClsInst, or a CoAxiom of a type family,
+-- this strategy causes problems: if we pick one and rewrite all
+-- references to a shared 'Name', we will accidentally fail to check
+-- if the DFun or CoAxioms are compatible, as they will never be
+-- checked--only exported entities are checked for compatibility,
+-- and a non-exported TyThing is checked WHEN we are checking the
+-- ClsInst or type family for compatibility in checkBootDeclM.
+-- By virtue of the fact that everything's been pointed to the merged
 -- declaration, you'll never notice there's a difference even if there
 -- is one.
 --
--- The solution is, for reference to implicit entities, we go straight
--- for the local TypeEnv corresponding to the entities from this particular
--- signature; this logic is in 'tcIfaceImplicit'.
+-- Fortunately, there are only a few places in the interface declarations
+-- where this can occur, so we replace those calls with 'tcIfaceImplicit',
+-- which will consult a local TypeEnv that records any never-exported
+-- TyThings which we should wire up with.
 --
--- There is also some fixM business because families need to refer to
--- coercion axioms, which are all in the big pile of decls.  I didn't
--- feel like untangling first so the fixM is a convenient way to get things
--- where they need to be.
+-- Note that we actually knot-tie this local TypeEnv (the 'fixM'), because a
+-- type family can refer to a coercion axiom, all of which are done in one go
+-- when we typecheck 'mi_decls'.  An alternate strategy would be to typecheck
+-- coercions first before type families, but that seemed more fragile.
 --
 
 {-
@@ -1666,7 +1674,7 @@ tcIfaceExtId name = do { thing <- tcIfaceGlobal name
                           AnId id -> return id
                           _       -> pprPanic "tcIfaceExtId" (ppr name$$ ppr thing) }
 
--- See Note [The implicit TypeEnv]
+-- See Note [Resolving never-exported Names in TcIface]
 tcIfaceImplicit :: Name -> IfL TyThing
 tcIfaceImplicit n = do
     lcl_env <- getLclEnv
diff --git a/compiler/typecheck/TcBackpack.hs b/compiler/typecheck/TcBackpack.hs
index d74cf51d77..9a428a837c 100644
--- a/compiler/typecheck/TcBackpack.hs
+++ b/compiler/typecheck/TcBackpack.hs
@@ -235,13 +235,13 @@ requirementMerges dflags mod_name =
 -- requirements by imports of modules from other packages.  The situation
 -- is something like this:
 --
---      package p where
+--      unit p where
 --          signature A
 --          signature B
 --              import A
 --
---      package q where
---          include p
+--      unit q where
+--          dependency p[A=<A>,B=<B>]
 --          signature A
 --          signature B
 --
@@ -383,7 +383,7 @@ thinModIface avails iface =
 
     non_exported_occs = mkOccSet [ occName n
                                  | (_, d) <- exported_decls
-                                 , n <- ifaceDeclNonExportedRefs d ]
+                                 , n <- ifaceDeclNeverExportedRefs d ]
     non_exported_decls = filter_decls non_exported_occs
 
     dfun_pred IfaceId{ ifIdDetails = IfDFunId } = True
@@ -396,13 +396,13 @@ thinModIface avails iface =
 -- refers to it; we can't decide to keep it by looking at the exports
 -- of a module after thinning.  Keep this synchronized with
 -- 'rnIfaceDecl'.
-ifaceDeclNonExportedRefs :: IfaceDecl -> [Name]
-ifaceDeclNonExportedRefs d@IfaceFamily{} =
+ifaceDeclNeverExportedRefs :: IfaceDecl -> [Name]
+ifaceDeclNeverExportedRefs d@IfaceFamily{} =
     case ifFamFlav d of
         IfaceClosedSynFamilyTyCon (Just (n, _))
             -> [n]
         _   -> []
-ifaceDeclNonExportedRefs _ = []
+ifaceDeclNeverExportedRefs _ = []
 
 
 -- Note [Blank hsigs for all requirements]
@@ -424,6 +424,53 @@ inheritedSigPvpWarning =
           "declaration to the local hsig file or move the signature to a " ++
           "library of its own and add that library as a dependency."
 
+-- Note [Handling never-exported TyThings under Backpack]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--   DEFINITION: A "never-exported TyThing" is a TyThing whose 'Name' will
+--   never be mentioned in the export list of a module (mi_avails).
+--   Unlike implicit TyThings (Note [Implicit TyThings]), non-exported
+--   TyThings DO have a standalone IfaceDecl declaration in their
+--   interface file.
+--
+-- Originally, Backpack was designed under the assumption that anything
+-- you could declare in a module could also be exported; thus, merging
+-- the export lists of two signatures is just merging the declarations
+-- of two signatures writ small.  Of course, in GHC Haskell, there are a
+-- few important things which are not explicitly exported but still can
+-- be used:  in particular, dictionary functions for instances and
+-- coercion axioms for type families also count.
+--
+-- When handling these non-exported things, there two primary things
+-- we need to watch out for:
+--
+--  * Signature matching/merging is done by comparing each
+--    of the exported entities of a signature and a module.  These exported
+--    entities may refer to non-exported TyThings which must be tested for
+--    consistency.  For example, an instance (ClsInst) will refer to a
+--    non-exported DFunId.  In this case, 'checkBootDeclM' directly compares the
+--    embedded 'DFunId' in 'is_dfun'.
+--
+--    For this to work at all, we must ensure that pointers in 'is_dfun' refer
+--    to DISTINCT 'DFunId's, even though the 'Name's (may) be the same.
+--    Unfortunately, this is the OPPOSITE of how we treat most other references
+--    to 'Name's, so this case needs to be handled specially.
+--
+--    The details are in the documentation for 'typecheckIfacesForMerging'.
+--    and the Note [Resolving never-exported Names in TcIface].
+--
+--  * When we rename modules and signatures, we use the export lists to
+--    decide how the declarations should be renamed.  However, this
+--    means we don't get any guidance for how to rename non-exported
+--    entities.  Fortunately, we only need to rename these entities
+--    *consistently*, so that 'typecheckIfacesForMerging' can wire them
+--    up as needed.
+--
+--    The details are in Note [rnIfaceNeverExported] in 'RnModIface'.
+--
+-- The root cause for all of these complications is the fact that these
+-- logically "implicit" entities are defined indirectly in an interface
+-- file.  #13151 gives a proposal to make these *truly* implicit.
+
 -- | Given a local 'ModIface', merge all inherited requirements
 -- from 'requirementMerges' into this signature, producing
 -- a final 'TcGblEnv' that matches the local signature and
@@ -666,7 +713,7 @@ mergeSignatures hsmod lcl_iface0 = do
     -- when we have a ClsInst, we can pull up the correct DFun to check if
     -- the types match.
     --
-    -- See also Note [Bogus DFun renamings] in RnModIface
+    -- See also Note [rnIfaceNeverExported] in RnModIface
     dfun_insts <- forM (tcg_insts tcg_env) $ \inst -> do
         n <- newDFunName (is_cls inst) (is_tys inst) (nameSrcSpan (is_dfun_name inst))
         let dfun = setVarName (is_dfun inst) n
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 46a1ea9872..6223fd1d89 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -324,7 +324,7 @@ data IfLclEnv
         -- This field is used to make sure "implicit" declarations
         -- (anything that cannot be exported in mi_exports) get
         -- wired up correctly in typecheckIfacesForMerging.  Most
-        -- of the time it's @Nothing@.  See Note [The implicit TypeEnv]
+        -- of the time it's @Nothing@.  See Note [Resolving never-exported Names in TcIface]
         -- in TcIface.
         if_implicits_env :: Maybe TypeEnv,