Fix roles merging to apply only to non-rep-injective types.

Test Plan: validate

Reviewers: simonpj

Subscribers:

7 files changed, 111 insertions, 2 deletions

diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 0363c9e581..2a56392910 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -235,20 +235,65 @@ mergeIfaceDecl d1 d2
                 ifSigs  = ops,
                 ifMinDef = BF.mkOr [noLoc bf1, noLoc bf2]
                 }
-            }
+            } `withRolesFrom` d2
     -- It doesn't matter; we'll check for consistency later when
     -- we merge, see 'mergeSignatures'
-    | otherwise              = d1
+    | otherwise              = d1 `withRolesFrom` d2
+
+-- Note [Role merging]
+-- ~~~~~~~~~~~~~~~~~~~
+-- First, why might it be necessary to do a non-trivial role
+-- merge?  It may rescue a merge that might otherwise fail:
+--
+--      signature A where
+--          type role T nominal representational
+--          data T a b
+--
+--      signature A where
+--          type role T representational nominal
+--          data T a b
+--
+-- A module that defines T as representational in both arguments
+-- would successfully fill both signatures, so it would be better
+-- if if we merged the roles of these types in some nontrivial
+-- way.
+--
+-- However, we have to be very careful about how we go about
+-- doing this, because role subtyping is *conditional* on
+-- the supertype being NOT representationally injective, e.g.,
+-- if we have instead:
+--
+--      signature A where
+--          type role T nominal representational
+--          data T a b = T a b
+--
+--      signature A where
+--          type role T representational nominal
+--          data T a b = T a b
+--
+-- Should we merge the definitions of T so that the roles are R/R (or N/N)?
+-- Absolutely not: neither resulting type is a subtype of the original
+-- types (see Note [Role subtyping]), because data is not representationally
+-- injective.
+--
+-- Thus, merging only occurs when BOTH TyCons in question are
+-- representationally injective.  If they're not, no merge.
 
 withRolesFrom :: IfaceDecl -> IfaceDecl -> IfaceDecl
 d1 `withRolesFrom` d2
     | Just roles1 <- ifMaybeRoles d1
     , Just roles2 <- ifMaybeRoles d2
+    , not (isRepInjectiveIfaceDecl d1 || isRepInjectiveIfaceDecl d2)
     = d1 { ifRoles = mergeRoles roles1 roles2 }
     | otherwise = d1
   where
     mergeRoles roles1 roles2 = zipWith max roles1 roles2
 
+isRepInjectiveIfaceDecl :: IfaceDecl -> Bool
+isRepInjectiveIfaceDecl IfaceData{ ifCons = IfDataTyCon _ } = True
+isRepInjectiveIfaceDecl IfaceFamily{ ifFamFlav = IfaceDataFamilyTyCon } = True
+isRepInjectiveIfaceDecl _ = False
+
 mergeIfaceClassOp :: IfaceClassOp -> IfaceClassOp -> IfaceClassOp
 mergeIfaceClassOp op1@(IfaceClassOp _ _ (Just _)) _ = op1
 mergeIfaceClassOp _ op2 = op2
diff --git a/testsuite/tests/backpack/should_compile/all.T b/testsuite/tests/backpack/should_compile/all.T
index 1d0c95e5f5..477c0fe220 100644
--- a/testsuite/tests/backpack/should_compile/all.T
+++ b/testsuite/tests/backpack/should_compile/all.T
@@ -44,6 +44,7 @@ test('bkp49', normal, backpack_compile, [''])
 test('bkp50', normal, backpack_compile, [''])
 test('bkp51', normal, backpack_compile, [''])
 test('bkp52', normal, backpack_compile, [''])
+test('bkp53', normal, backpack_compile, [''])
 
 test('T13140', normal, backpack_compile, [''])
 test('T13149', expect_broken(13149), backpack_compile, [''])
diff --git a/testsuite/tests/backpack/should_compile/bkp53.bkp b/testsuite/tests/backpack/should_compile/bkp53.bkp
new file mode 100644
index 0000000000..aa1dc53c61
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/bkp53.bkp
@@ -0,0 +1,22 @@
+{-# LANGUAGE RoleAnnotations #-}
+-- Role merging test
+unit p where
+    signature A where
+        type role T nominal representational
+        data T a b
+        newtype S a b = MkS (T a b)
+unit q where
+    signature A where
+        type role T representational nominal
+        data T a b
+        newtype S a b = MkS (T a b)
+unit r where
+    dependency p[A=<A>]
+    dependency q[A=<A>]
+    module M where
+        import A
+        import Data.Coerce
+        f :: (Coercible a1 a2, Coercible b1 b2) => T a1 b1 -> T a2 b2
+        f = coerce
+        g :: (Coercible a1 a2, Coercible b1 b2) => S a1 b1 -> S a2 b2
+        g = coerce
diff --git a/testsuite/tests/backpack/should_compile/bkp53.stderr b/testsuite/tests/backpack/should_compile/bkp53.stderr
new file mode 100644
index 0000000000..a2b19452b2
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/bkp53.stderr
@@ -0,0 +1,7 @@
+[1 of 3] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 3] Processing q
+  [1 of 1] Compiling A[sig]           ( q/A.hsig, nothing )
+[3 of 3] Processing r
+  [1 of 2] Compiling A[sig]           ( r/A.hsig, nothing )
+  [2 of 2] Compiling M                ( r/M.hs, nothing )
diff --git a/testsuite/tests/backpack/should_fail/all.T b/testsuite/tests/backpack/should_fail/all.T
index 82b4e6803b..e1416fcec8 100644
--- a/testsuite/tests/backpack/should_fail/all.T
+++ b/testsuite/tests/backpack/should_fail/all.T
@@ -42,3 +42,4 @@ test('bkpfail43', normal, backpack_compile_fail, [''])
 test('bkpfail44', normal, backpack_compile_fail, [''])
 test('bkpfail45', normal, backpack_compile_fail, [''])
 test('bkpfail46', normal, backpack_compile_fail, [''])
+test('bkpfail47', normal, backpack_compile_fail, [''])
diff --git a/testsuite/tests/backpack/should_fail/bkpfail47.bkp b/testsuite/tests/backpack/should_fail/bkpfail47.bkp
new file mode 100644
index 0000000000..b8d4ae66d8
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail47.bkp
@@ -0,0 +1,12 @@
+{-# LANGUAGE RoleAnnotations #-}
+unit p where
+    signature A where
+        type role T nominal representational
+        data T a b
+unit q where
+    signature A where
+        type role T representational nominal
+        data T a b = MkT
+unit r where
+    dependency p[A=<A>]
+    dependency q[A=<A>]
diff --git a/testsuite/tests/backpack/should_fail/bkpfail47.stderr b/testsuite/tests/backpack/should_fail/bkpfail47.stderr
new file mode 100644
index 0000000000..b2bc08b4c2
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail47.stderr
@@ -0,0 +1,21 @@
+[1 of 3] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 3] Processing q
+  [1 of 1] Compiling A[sig]           ( q/A.hsig, nothing )
+[3 of 3] Processing r
+  [1 of 1] Compiling A[sig]           ( r/A.hsig, nothing )
+
+bkpfail47.bkp:9:9: error:
+    • Type constructor ‘T’ has conflicting definitions in the module
+      and its hsig file
+      Main module: type role T representational nominal
+                   data T a b = MkT
+      Hsig file:  type role T nominal representational
+                  data T a b
+      The roles are not compatible:
+      Main module: [representational, nominal]
+      Hsig file: [nominal, representational]
+    • while merging the signatures from:
+        • p[A=<A>]:A
+        • q[A=<A>]:A
+        • ...and the local signature for A