Subtyping for roles in signatures.

Summary:
This commit implements the plan in #13140:

* Today, roles in signature files default to representational. Let's change the
  default to nominal, as this is the most flexible implementation side. If a
  client of the signature needs to coerce with a type, the signature can be
  adjusted to have more stringent requirements.

* If a parameter is declared as nominal in a signature, it can be implemented
  by a data type which is actually representational.

* When merging abstract data declarations, we take the smallest role for every
  parameter. The roles are considered fix once we specify the structure of an
  ADT.

* Critically, abstract types are NOT injective, so we aren't allowed to
  make inferences like "if T a ~R T b, then a ~N b" based on the nominal
  role of a parameter in an abstract type (this would be unsound if the
  parameter ended up being phantom.)  This restriction is similar to the
  restriction we have on newtypes.

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

Test Plan: validate

Reviewers: simonpj, bgamari, austin, goldfire

Subscribers: goldfire, thomie

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

3 files changed, 69 insertions, 0 deletions

diff --git a/testsuite/tests/backpack/should_compile/T13140.bkp b/testsuite/tests/backpack/should_compile/T13140.bkp
new file mode 100644
index 0000000000..aa04b98c1e
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/T13140.bkp
@@ -0,0 +1,40 @@
+{-# LANGUAGE RoleAnnotations #-}
+unit p where
+    signature A where
+        data T a
+unit q1 where
+    module A where
+        data T a = T a
+unit q2 where
+    module A where
+        type role T nominal
+        data T a = T a
+unit q3 where
+    module A where
+        data T a = T
+unit r where
+    -- Subtyping test
+    dependency p[A=q1:A]
+    dependency p[A=q2:A]
+    dependency p[A=q3:A]
+
+unit p2 where
+    signature A where
+        type role T representational
+        data T a
+    module M where
+        import Data.Coerce
+        import A
+        newtype K = K Int
+        f :: T K -> T Int
+        f = coerce
+unit p3 where
+    -- Merge test
+    dependency p[A=<A>]
+    dependency p2[A=<A>]
+    module M2 where
+        import Data.Coerce
+        import A
+        newtype K = K Int
+        f :: T K -> T Int
+        f = coerce
diff --git a/testsuite/tests/backpack/should_compile/T13140.stderr b/testsuite/tests/backpack/should_compile/T13140.stderr
new file mode 100644
index 0000000000..c40b6bc1df
--- /dev/null
+++ b/testsuite/tests/backpack/should_compile/T13140.stderr
@@ -0,0 +1,28 @@
+[1 of 7] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 7] Processing q1
+  Instantiating q1
+  [1 of 1] Compiling A                ( q1/A.hs, T13140.out/q1/A.o )
+[3 of 7] Processing q2
+  Instantiating q2
+  [1 of 1] Compiling A                ( q2/A.hs, T13140.out/q2/A.o )
+[4 of 7] Processing q3
+  Instantiating q3
+  [1 of 1] Compiling A                ( q3/A.hs, T13140.out/q3/A.o )
+[5 of 7] Processing r
+  Instantiating r
+  [1 of 3] Including p[A=q1:A]
+    Instantiating p[A=q1:A]
+    [1 of 1] Compiling A[sig]           ( p/A.hsig, T13140.out/p/p-BwqqugG2ETwLIwrPGPdl6W/A.o )
+  [2 of 3] Including p[A=q2:A]
+    Instantiating p[A=q2:A]
+    [1 of 1] Compiling A[sig]           ( p/A.hsig, T13140.out/p/p-KZH5iDezOjj6YVcfuBlAG2/A.o )
+  [3 of 3] Including p[A=q3:A]
+    Instantiating p[A=q3:A]
+    [1 of 1] Compiling A[sig]           ( p/A.hsig, T13140.out/p/p-200ijkYDy133WhdgYYHZ24/A.o )
+[6 of 7] Processing p2
+  [1 of 2] Compiling A[sig]           ( p2/A.hsig, nothing )
+  [2 of 2] Compiling M                ( p2/M.hs, nothing )
+[7 of 7] Processing p3
+  [1 of 2] Compiling A[sig]           ( p3/A.hsig, nothing )
+  [2 of 2] Compiling M2               ( p3/M2.hs, nothing )
diff --git a/testsuite/tests/backpack/should_compile/all.T b/testsuite/tests/backpack/should_compile/all.T
index 96bc5e1862..1d0c95e5f5 100644
--- a/testsuite/tests/backpack/should_compile/all.T
+++ b/testsuite/tests/backpack/should_compile/all.T
@@ -45,6 +45,7 @@ test('bkp50', normal, backpack_compile, [''])
 test('bkp51', normal, backpack_compile, [''])
 test('bkp52', normal, backpack_compile, [''])
 
+test('T13140', normal, backpack_compile, [''])
 test('T13149', expect_broken(13149), backpack_compile, [''])
 test('T13214', normal, backpack_compile, [''])
 test('T13250', normal, backpack_compile, [''])