Make IfaceAxiom typechecking lazier.

Fixes #13803, but adds a note about a yet to be fixed #13981.

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

Test Plan: validate

Reviewers: bgamari, austin

Reviewed By: bgamari

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #13803

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

10 files changed, 107 insertions, 12 deletions

diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 3a6a4070d2..1477f462fc 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -807,7 +807,14 @@ tc_iface_decl _parent ignore_prags
 tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc
                               , ifAxBranches = branches, ifRole = role })
   = do { tc_tycon    <- tcIfaceTyCon tc
-       ; tc_branches <- tc_ax_branches branches
+       -- Must be done lazily, because axioms are forced when checking
+       -- for family instance consistency, and the RHS may mention
+       -- a hs-boot declared type constructor that is going to be
+       -- defined by this module.
+       -- e.g. type instance F Int = ToBeDefined
+       -- See Trac #13803
+       ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name)
+                      $ tc_ax_branches branches
        ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
                              , co_ax_name     = tc_name
                              , co_ax_tc       = tc_tycon
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index cabfb3376b..87a602c783 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -392,25 +392,72 @@ checkFamInstConsistency directlyImpMods
            -- the family instances of our imported modules are consistent with
            -- one another; this might lead you to think that this process
            -- has nothing to do with the module we are about to typecheck.
-           -- Not so!  If a type family was defined in the hs-boot file
-           -- of the current module, we are NOT allowed to poke the TyThing
-           -- for this family: since we haven't typechecked the definition
-           -- yet (checkFamInstConsistency is called during renaming),
-           -- we won't be able to find our local copy in if_rec_types.
-           -- Failing to do this lead to #11062.
+           -- Not so!  Consider the following case:
            --
-           -- So, we have to defer the checks for family instances that
-           -- refer to families that are locally defined.
+           --   -- A.hs-boot
+           --   type family F a
+           --
+           --   -- B.hs
+           --   import {-# SOURCE #-} A
+           --   type instance F Int = Bool
+           --
+           --   -- A.hs
+           --   import B
+           --   type family F a
+           --
+           -- When typechecking A, we are NOT allowed to poke the TyThing
+           -- for for F until we have typechecked the family.  Thus, we
+           -- can't do consistency checking for the instance in B
+           -- (checkFamInstConsistency is called during renaming).
+           -- Failing to defer the consistency check lead to #11062.
+           --
+           -- Additionally, we should also defer consistency checking when
+           -- type from the hs-boot file of the current module occurs on
+           -- the left hand side, as we will poke its TyThing when checking
+           -- for overlap.
+           --
+           --   -- F.hs
+           --   type family F a
+           --
+           --   -- A.hs-boot
+           --   import F
+           --   data T
+           --
+           --   -- B.hs
+           --   import {-# SOURCE #-} A
+           --   import F
+           --   type instance F T = Int
+           --
+           --   -- A.hs
+           --   import B
+           --   data T = MkT
+           --
+           -- However, this is not yet done; see #13981.
+           --
+           -- Note that it is NOT necessary to defer for occurrences in the
+           -- RHS (e.g., type instance F Int = T, in the above example),
+           -- since that never participates in consistency checking
+           -- in any nontrivial way.
+           --
+           -- Why don't we defer ALL of the checks to later?  Well, many
+           -- instances aren't involved in the recursive loop at all.  So
+           -- we might as well check them immediately; and there isn't
+           -- a good time to check them later in any case: every time
+           -- we finish kind-checking a type declaration and add it to
+           -- a context, we *then* consistency check all of the instances
+           -- which mentioned that type.  We DO want to check instances
+           -- as quickly as possible, so that we aren't typechecking
+           -- values with inconsistent axioms in scope.
            --
            -- See also Note [Tying the knot] and Note [Type-checking inside the knot]
            -- for why we are doing this at all.
            ; this_mod <- getModule
-           ; let (check_now, check_later)
                     -- NB: == this_mod only holds if there's an hs-boot file;
                     -- otherwise we cannot possible see instances for families
                     -- defined by the module we are compiling in imports.
-                    = partition ((/= this_mod) . nameModule . fi_fam)
-                                (famInstEnvElts env1)
+           ; let shouldCheckNow = ((/= this_mod) . nameModule . fi_fam)
+                 (check_now, check_later) =
+                    partition shouldCheckNow (famInstEnvElts env1)
            ; mapM_ (checkForConflicts (emptyFamInstEnv, env2))           check_now
            ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
            ; let check_later_map =
diff --git a/testsuite/tests/driver/T13803/D.hs b/testsuite/tests/driver/T13803/D.hs
new file mode 100644
index 0000000000..839f115953
--- /dev/null
+++ b/testsuite/tests/driver/T13803/D.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeFamilies #-}
+module D (D) where
+
+type family D a
+type instance D Int = Int
diff --git a/testsuite/tests/driver/T13803/E.hs b/testsuite/tests/driver/T13803/E.hs
new file mode 100644
index 0000000000..2ae1908e34
--- /dev/null
+++ b/testsuite/tests/driver/T13803/E.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module E where
+
+import                GHC.Exts (Constraint)
+import {-# SOURCE #-} Y
+
+data E
+
+type family CF a :: * -> Constraint
+type instance CF E = Y
diff --git a/testsuite/tests/driver/T13803/E.hs-boot b/testsuite/tests/driver/T13803/E.hs-boot
new file mode 100644
index 0000000000..858a5ef617
--- /dev/null
+++ b/testsuite/tests/driver/T13803/E.hs-boot
@@ -0,0 +1 @@
+module E where
diff --git a/testsuite/tests/driver/T13803/Makefile b/testsuite/tests/driver/T13803/Makefile
new file mode 100644
index 0000000000..4a18296cc2
--- /dev/null
+++ b/testsuite/tests/driver/T13803/Makefile
@@ -0,0 +1,6 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
+
+T13803:
+	'$(TEST_HC)' $(TEST_HC_OPTS) --make Y.hs
diff --git a/testsuite/tests/driver/T13803/T13803.stdout b/testsuite/tests/driver/T13803/T13803.stdout
new file mode 100644
index 0000000000..bab4a55099
--- /dev/null
+++ b/testsuite/tests/driver/T13803/T13803.stdout
@@ -0,0 +1,5 @@
+[1 of 5] Compiling D                ( D.hs, D.o )
+[2 of 5] Compiling E[boot]          ( E.hs-boot, E.o-boot )
+[3 of 5] Compiling Y[boot]          ( Y.hs-boot, Y.o-boot )
+[4 of 5] Compiling E                ( E.hs, E.o )
+[5 of 5] Compiling Y                ( Y.hs, Y.o )
diff --git a/testsuite/tests/driver/T13803/Y.hs b/testsuite/tests/driver/T13803/Y.hs
new file mode 100644
index 0000000000..c1bf116b0b
--- /dev/null
+++ b/testsuite/tests/driver/T13803/Y.hs
@@ -0,0 +1,6 @@
+module Y where
+
+import                D ()
+import {-# SOURCE #-} E
+
+class Y o
diff --git a/testsuite/tests/driver/T13803/Y.hs-boot b/testsuite/tests/driver/T13803/Y.hs-boot
new file mode 100644
index 0000000000..42737ccb93
--- /dev/null
+++ b/testsuite/tests/driver/T13803/Y.hs-boot
@@ -0,0 +1,3 @@
+module Y where
+
+class Y o
diff --git a/testsuite/tests/driver/T13803/all.T b/testsuite/tests/driver/T13803/all.T
new file mode 100644
index 0000000000..bfd720cae9
--- /dev/null
+++ b/testsuite/tests/driver/T13803/all.T
@@ -0,0 +1,4 @@
+test('T13803',
+     [extra_files(['D.hs', 'E.hs-boot', 'E.hs', 'Y.hs', 'Y.hs-boot'])],
+     run_command,
+     ['$MAKE -s --no-print-directory T13803'])