Fix handling of closed type families in Backpack.

Summary:
A few related problems:

- CoAxioms, like DFuns, are implicit and never exported,
  so we have to make sure we treat them the same way as
  DFuns: in RnModIface we need to rename references to
  them with rnIfaceImplicit and in mergeSignatures we need
  to NOT check them directly for compatibility (the
  test on the type family will do this check for us.)

- But actually, we weren't checking if the axioms WERE
  consistent.  This is because we were forwarding all
  embedded CoAxiom references in the type family TyThing
  to the merged version, but that reference was what
  checkBootDeclM was using as a comparison point.
  This is similar to a problem we saw with DFuns.

  To fix this, I refactored the handling of implicit entities in TcIface
  for Backpack.  See Note [The implicit TypeEnv] for the gory details.
  Instead of passing the TypeEnv around explicitly, we stuffed it in
  IfLclEnv.

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

Test Plan: validate

Reviewers: bgamari, simonpj, austin

Subscribers: thomie

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

7 files changed, 104 insertions, 49 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index ea3eb54b2a..b7d4623bef 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -466,7 +466,7 @@ rnIfaceDecl d@IfaceClass{} = do
                      , ifSigs = sigs
                      }
 rnIfaceDecl d@IfaceAxiom{} = do
-            name <- rnIfaceGlobal (ifName d)
+            name <- rnIfaceImplicit (ifName d)
             tycon <- rnIfaceTyCon (ifTyCon d)
             ax_branches <- mapM rnIfaceAxBranch (ifAxBranches d)
             return d { ifName = name
@@ -497,7 +497,7 @@ rnIfaceDecl d@IfacePatSyn{} =  do
 
 rnIfaceFamTyConFlav :: Rename IfaceFamTyConFlav
 rnIfaceFamTyConFlav (IfaceClosedSynFamilyTyCon (Just (n, axs)))
-    = IfaceClosedSynFamilyTyCon . Just <$> ((,) <$> rnIfaceGlobal n
+    = IfaceClosedSynFamilyTyCon . Just <$> ((,) <$> rnIfaceImplicit n
                                                 <*> mapM rnIfaceAxBranch axs)
 rnIfaceFamTyConFlav flav = pure flav
 
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index d5cc860b64..feb4ecbf86 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -7,6 +7,7 @@ Type checking of type signatures in interface files
 -}
 
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE NondecreasingIndentation #-}
 
 module TcIface (
         tcLookupImported_maybe,
@@ -204,6 +205,7 @@ typecheckIface iface
 isAbstractIfaceDecl :: IfaceDecl -> Bool
 isAbstractIfaceDecl IfaceData{ ifCons = IfAbstractTyCon _ } = True
 isAbstractIfaceDecl IfaceClass{ ifCtxt = [], ifSigs = [], ifATs = [] } = True
+isAbstractIfaceDecl IfaceFamily{ ifFamFlav = IfaceAbstractClosedSynFamilyTyCon } = True
 isAbstractIfaceDecl _ = False
 
 -- | Merge two 'IfaceDecl's together, preferring a non-abstract one.  If
@@ -276,7 +278,7 @@ 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]
+    -- serialize them out.  See Note [Bogus DFun renamings] in RnModIface
     let mk_decl_env decls
             = mkOccEnv [ (getOccName decl, decl)
                        | decl <- decls
@@ -295,13 +297,15 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
 
     -- OK, now typecheck each ModIface using this environment
     details <- forM ifaces $ \iface -> do
-        -- DO NOT load these decls into the mutable variable: we did
-        -- that already!
-        decls     <- loadDecls ignore_prags (mi_decls iface)
-        let type_env = mkNameEnv decls
+        -- See Note [The implicit TypeEnv]
+        type_env <- fixM $ \type_env -> do
+            setImplicitEnvM type_env $ do
+                decls <- loadDecls ignore_prags (mi_decls iface)
+                return (mkNameEnv decls)
         -- But note that we use this type_env to typecheck references to DFun
         -- in 'IfaceInst'
-        insts     <- mapM (tcIfaceInstWithDFunTypeEnv type_env) (mi_insts iface)
+        setImplicitEnvM type_env $ do
+        insts     <- mapM tcIfaceInst (mi_insts iface)
         fam_insts <- mapM tcIfaceFamInst (mi_fam_insts iface)
         rules     <- tcIfaceRules ignore_prags (mi_rules iface)
         anns      <- tcIfaceAnnotations (mi_anns iface)
@@ -333,10 +337,14 @@ typecheckIfaceForInstantiate nsubst iface =
                         (text "typecheckIfaceForInstantiate")
                         (mi_boot iface) nsubst $ do
     ignore_prags <- goptM Opt_IgnoreInterfacePragmas
-    decls     <- loadDecls ignore_prags (mi_decls iface)
-    let type_env = mkNameEnv decls
+    -- See Note [The implicit TypeEnv]
+    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]
-    insts     <- mapM (tcIfaceInstWithDFunTypeEnv type_env) (mi_insts iface)
+    setImplicitEnvM type_env $ do
+    insts     <- mapM tcIfaceInst (mi_insts iface)
     fam_insts <- mapM tcIfaceFamInst (mi_fam_insts iface)
     rules     <- tcIfaceRules ignore_prags (mi_rules iface)
     anns      <- tcIfaceAnnotations (mi_anns iface)
@@ -351,6 +359,33 @@ typecheckIfaceForInstantiate nsubst iface =
                         , md_exports   = exports
                         }
 
+-- Note [The implicit TypeEnv]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- 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
+-- 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'.
+--
+-- 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.
+--
+
 {-
 ************************************************************************
 *                                                                      *
@@ -858,25 +893,7 @@ tcIfaceInst (IfaceClsInst { ifDFun = dfun_name, ifOFlag = oflag
                           , ifInstCls = cls, ifInstTys = mb_tcs
                           , ifInstOrph = orph })
   = do { dfun <- forkM (text "Dict fun" <+> ppr dfun_name) $
-                 tcIfaceExtId dfun_name
-       ; let mb_tcs' = map (fmap ifaceTyConName) mb_tcs
-       ; return (mkImportedInstance cls mb_tcs' dfun_name dfun oflag orph) }
-
--- | Typecheck an 'IfaceClsInst', but rather than using 'tcIfaceGlobal',
--- resolve the 'ifDFun' using a passed in 'TypeEnv'.
---
--- Why do we do it this way?  See Note [Bogus DFun renamings]
-tcIfaceInstWithDFunTypeEnv :: TypeEnv -> IfaceClsInst -> IfL ClsInst
-tcIfaceInstWithDFunTypeEnv tenv
-            (IfaceClsInst { ifDFun = dfun_name, ifOFlag = oflag
-                          , ifInstCls = cls, ifInstTys = mb_tcs
-                          , ifInstOrph = orph })
-  = do { dfun <- case lookupTypeEnv tenv dfun_name of
-                    Nothing -> pprPanic "tcIfaceInstWithDFunTypeEnv"
-                        (ppr dfun_name $$ ppr tenv)
-                    Just (AnId dfun) -> return dfun
-                    Just tything -> pprPanic "tcIfaceInstWithDFunTypeEnv"
-                        (ppr dfun_name <+> ppr tything)
+                    fmap tyThingId (tcIfaceImplicit dfun_name)
        ; let mb_tcs' = map (fmap ifaceTyConName) mb_tcs
        ; return (mkImportedInstance cls mb_tcs' dfun_name dfun oflag orph) }
 
@@ -1618,7 +1635,7 @@ tcIfaceTyCon (IfaceTyCon name info)
            IsPromoted    -> promoteDataCon $ tyThingDataCon thing }
 
 tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
-tcIfaceCoAxiom name = do { thing <- tcIfaceGlobal name
+tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
                          ; return (tyThingCoAxiom thing) }
 
 tcIfaceDataCon :: Name -> IfL DataCon
@@ -1633,6 +1650,17 @@ tcIfaceExtId name = do { thing <- tcIfaceGlobal name
                           AnId id -> return id
                           _       -> pprPanic "tcIfaceExtId" (ppr name$$ ppr thing) }
 
+-- See Note [The implicit TypeEnv]
+tcIfaceImplicit :: Name -> IfL TyThing
+tcIfaceImplicit n = do
+    lcl_env <- getLclEnv
+    case if_implicits_env lcl_env of
+        Nothing -> tcIfaceGlobal n
+        Just tenv ->
+            case lookupTypeEnv tenv n of
+                Nothing -> pprPanic "tcIfaceInst" (ppr n $$ ppr tenv)
+                Just tything -> return tything
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcBackpack.hs b/compiler/typecheck/TcBackpack.hs
index 00e38249ea..5c61871155 100644
--- a/compiler/typecheck/TcBackpack.hs
+++ b/compiler/typecheck/TcBackpack.hs
@@ -135,6 +135,8 @@ checkHsigIface tcg_env gr sig_iface
     dfun_names = map getName sig_insts
     check_export name
       -- Skip instances, we'll check them later
+      -- TODO: Actually this should never happen, because DFuns are
+      -- never exported...
       | name `elem` dfun_names = return ()
       -- See if we can find the type directly in the hsig ModDetails
       -- TODO: need to special case wired in names
@@ -559,23 +561,23 @@ mergeSignatures hsmod lcl_iface0 = do
     tcg_env <- (\x -> foldM x tcg_env infos)
              $ \tcg_env (iface, details) -> do
 
-        -- For every TyThing in the type environment, compare it for
-        -- compatibility with the merged environment, but skip
-        -- DFunIds and implicit TyThings.
-        let check_ty sig_thing
-              -- We'll check these with the parent
-              | isImplicitTyThing sig_thing
-              = return ()
-              -- These aren't in the type environment; checked
-              -- when merging instances
-              | AnId id <- sig_thing
-              , isDFunId id
-              = return ()
-              | Just thing <- lookupTypeEnv type_env (getName sig_thing)
-              = checkHsigDeclM iface sig_thing thing
+        let check_export name
+              | Just sig_thing <- lookupTypeEnv (md_types details) name
+              = case lookupTypeEnv type_env (getName sig_thing) of
+                  Just thing -> checkHsigDeclM iface sig_thing thing
+                  Nothing -> panic "mergeSignatures: check_export"
+              -- Oops! We're looking for this export but it's
+              -- not actually in the type environment of the signature's
+              -- ModDetails.
+              --
+              -- NB: This case happens because the we're iterating
+              -- over the union of all exports, so some interfaces
+              -- won't have everything.  Note that md_exports is nonsense
+              -- (it's the same as exports); maybe we should fix this
+              -- eventually.
               | otherwise
-              = panic "mergeSignatures check_ty"
-        mapM_ check_ty (typeEnvElts (md_types details))
+              = return ()
+        mapM_ check_export (map availName exports)
 
         -- Note [Signature merging instances]
         -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 4c44eecfd9..aac872a0ec 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1066,6 +1066,8 @@ checkBootTyCon is_boot tc1 tc2
   = ASSERT(tc1 == tc2)
     let eqFamFlav OpenSynFamilyTyCon   OpenSynFamilyTyCon = True
         eqFamFlav (DataFamilyTyCon {}) (DataFamilyTyCon {}) = True
+        -- This case only happens for hsig merging:
+        eqFamFlav AbstractClosedSynFamilyTyCon AbstractClosedSynFamilyTyCon = True
         eqFamFlav AbstractClosedSynFamilyTyCon (ClosedSynFamilyTyCon {}) = True
         eqFamFlav (ClosedSynFamilyTyCon {}) AbstractClosedSynFamilyTyCon = True
         eqFamFlav (ClosedSynFamilyTyCon ax1) (ClosedSynFamilyTyCon ax2)
@@ -1077,8 +1079,11 @@ checkBootTyCon is_boot tc1 tc2
     in
     -- check equality of roles, family flavours and injectivity annotations
     check (roles1 == roles2) roles_msg `andThenCheck`
-    check (eqFamFlav fam_flav1 fam_flav2) empty `andThenCheck`
-    check (injInfo1 == injInfo2) empty
+    check (eqFamFlav fam_flav1 fam_flav2)
+        (ifPprDebug $
+            text "Family flavours" <+> ppr fam_flav1 <+> text "and" <+> ppr fam_flav2 <+>
+            text "do not match") `andThenCheck`
+    check (injInfo1 == injInfo2) (text "Injectivities do not match")
 
   | isAlgTyCon tc1 && isAlgTyCon tc2
   , Just env <- eqVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 8c117f0936..817989e5eb 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -124,6 +124,7 @@ module TcRnMonad(
   failIfM,
   forkM_maybe,
   forkM,
+  setImplicitEnvM,
 
   withException,
 
@@ -1670,6 +1671,7 @@ mkIfLclEnv mod loc boot
                                 if_loc     = loc,
                                 if_boot    = boot,
                                 if_nsubst  = Nothing,
+                                if_implicits_env = Nothing,
                                 if_tv_env  = emptyFsEnv,
                                 if_id_env  = emptyFsEnv }
 
@@ -1800,6 +1802,9 @@ forkM doc thing_inside
                                    -- pprPanic "forkM" doc
                         Just r  -> r) }
 
+setImplicitEnvM :: TypeEnv -> IfL a -> IfL a
+setImplicitEnvM tenv m = updLclEnv (\lcl -> lcl { if_implicits_env = Just tenv }) m
+
 {-
 Note [Masking exceptions in forkM_maybe]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 6d902b32e0..c938adffd4 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -321,6 +321,13 @@ data IfLclEnv
 
         if_nsubst :: Maybe NameShape,
 
+        -- 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]
+        -- in TcIface.
+        if_implicits_env :: Maybe TypeEnv,
+
         if_tv_env  :: FastStringEnv TyVar,     -- Nested tyvar bindings
         if_id_env  :: FastStringEnv Id         -- Nested id binding
     }
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index ec2f5d5a09..36149187c6 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -997,6 +997,14 @@ data FamTyConFlav
    -- | Built-in type family used by the TypeNats solver
    | BuiltInSynFamTyCon BuiltInSynFamily
 
+instance Outputable FamTyConFlav where
+    ppr (DataFamilyTyCon n) = text "data family" <+> ppr n
+    ppr OpenSynFamilyTyCon = text "open type family"
+    ppr (ClosedSynFamilyTyCon Nothing) = text "closed type family"
+    ppr (ClosedSynFamilyTyCon (Just coax)) = text "closed type family" <+> ppr coax
+    ppr AbstractClosedSynFamilyTyCon = text "abstract closed type family"
+    ppr (BuiltInSynFamTyCon _) = text "built-in type family"
+
 {- Note [Closed type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * In an open type family you can add new instances later.  This is the