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

8 files changed, 81 insertions, 0 deletions

diff --git a/testsuite/tests/backpack/should_compile/all.T b/testsuite/tests/backpack/should_compile/all.T
index 3525a8521f..33d0357988 100644
--- a/testsuite/tests/backpack/should_compile/all.T
+++ b/testsuite/tests/backpack/should_compile/all.T
@@ -39,3 +39,5 @@ test('bkp44', normal, backpack_compile, [''])
 test('bkp45', normal, backpack_compile, [''])
 test('bkp46', normal, backpack_compile, [''])
 test('bkp47', normal, backpack_compile, [''])
+test('bkp48', normal, backpack_compile, [''])
+test('bkp49', normal, backpack_compile, [''])
diff --git a/testsuite/tests/backpack/should_compile/bkp48.bkp b/testsuite/tests/backpack/should_compile/bkp48.bkp
new file mode 100644
index 0000000000..d48d0359d2
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/bkp48.bkp
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeFamilies #-}
+unit p where
+    signature A where
+        type family K a where ..
+
+unit q where
+    signature A where
+        type family K a where
+            K a = Int
+
+unit r where
+    dependency p[A=<A>]
+    dependency q[A=<A>]
+
+unit i where
+    module A where
+        type family K a where
+            K a = Int
+
+unit m where
+    dependency r[A=i:A]
+    dependency p[A=i:A]
+    dependency q[A=i:A]
diff --git a/testsuite/tests/backpack/should_compile/bkp48.stderr b/testsuite/tests/backpack/should_compile/bkp48.stderr
new file mode 100644
index 0000000000..ae6c7fc575
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/bkp48.stderr
@@ -0,0 +1,22 @@
+[1 of 5] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 5] Processing q
+  [1 of 1] Compiling A[sig]           ( q/A.hsig, nothing )
+[3 of 5] Processing r
+  [1 of 1] Compiling A[sig]           ( r/A.hsig, nothing )
+[4 of 5] Processing i
+  Instantiating i
+  [1 of 1] Compiling A                ( i/A.hs, bkp48.out/i/A.o )
+[5 of 5] Processing m
+  Instantiating m
+  [1 of 3] Including r[A=i:A]
+    Instantiating r[A=i:A]
+    [1 of 2] Including p[A=i:A]
+      Instantiating p[A=i:A]
+      [1 of 1] Compiling A[sig]           ( p/A.hsig, bkp48.out/p/p-CtJxD03mJqIIVJzOga8l4X/A.o )
+    [2 of 2] Including q[A=i:A]
+      Instantiating q[A=i:A]
+      [1 of 1] Compiling A[sig]           ( q/A.hsig, bkp48.out/q/q-CtJxD03mJqIIVJzOga8l4X/A.o )
+    [1 of 1] Compiling A[sig]           ( r/A.hsig, bkp48.out/r/r-CtJxD03mJqIIVJzOga8l4X/A.o )
+  [2 of 3] Including p[A=i:A]
+  [3 of 3] Including q[A=i:A]
diff --git a/testsuite/tests/backpack/should_compile/bkp49.bkp b/testsuite/tests/backpack/should_compile/bkp49.bkp
new file mode 100644
index 0000000000..b8f6e0097e
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/bkp49.bkp
@@ -0,0 +1,7 @@
+unit p where
+    signature A where
+        data T
+        instance Eq T
+unit q where
+    dependency p[A=<A>]
+    signature A (T) where
diff --git a/testsuite/tests/backpack/should_compile/bkp49.stderr b/testsuite/tests/backpack/should_compile/bkp49.stderr
new file mode 100644
index 0000000000..d8f64f0657
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/bkp49.stderr
@@ -0,0 +1,4 @@
+[1 of 2] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 2] Processing q
+  [1 of 1] Compiling A[sig]           ( q/A.hsig, nothing )
diff --git a/testsuite/tests/backpack/should_fail/all.T b/testsuite/tests/backpack/should_fail/all.T
index c24fa25f3b..ff171d38f6 100644
--- a/testsuite/tests/backpack/should_fail/all.T
+++ b/testsuite/tests/backpack/should_fail/all.T
@@ -37,3 +37,4 @@ test('bkpfail38', normal, backpack_compile_fail, [''])
 test('bkpfail39', expect_broken(13068), backpack_compile_fail, [''])
 test('bkpfail40', normal, backpack_compile_fail, [''])
 test('bkpfail41', normal, backpack_compile_fail, [''])
+test('bkpfail42', normal, backpack_compile_fail, [''])
diff --git a/testsuite/tests/backpack/should_fail/bkpfail42.bkp b/testsuite/tests/backpack/should_fail/bkpfail42.bkp
new file mode 100644
index 0000000000..8face3f3be
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail42.bkp
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+unit p where
+    signature A where
+        type family F a where
+            F a = Bool
+unit q where
+    dependency p[A=<A>]
+    signature A where
+        type family F a where
+            F a = Int
diff --git a/testsuite/tests/backpack/should_fail/bkpfail42.stderr b/testsuite/tests/backpack/should_fail/bkpfail42.stderr
new file mode 100644
index 0000000000..734832ff4b
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail42.stderr
@@ -0,0 +1,12 @@
+[1 of 2] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 2] Processing q
+  [1 of 1] Compiling A[sig]           ( q/A.hsig, nothing )
+
+bkpfail42.bkp:9:9: error:
+    Type constructor ‘F’ has conflicting definitions in the module
+    and its hsig file
+    Main module: type family F a :: *
+                   where [a] F a = GHC.Types.Int
+    Hsig file:  type family F a :: *
+                  where [a] F a = GHC.Types.Bool