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

11 files changed, 171 insertions, 32 deletions

diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index ffe29c6ce7..d8461f364f 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -212,25 +212,41 @@ isAbstractIfaceDecl IfaceClass{ ifCtxt = [], ifSigs = [], ifATs = [] } = True
 isAbstractIfaceDecl IfaceFamily{ ifFamFlav = IfaceAbstractClosedSynFamilyTyCon } = True
 isAbstractIfaceDecl _ = False
 
+ifMaybeRoles :: IfaceDecl -> Maybe [Role]
+ifMaybeRoles IfaceData    { ifRoles = rs } = Just rs
+ifMaybeRoles IfaceSynonym { ifRoles = rs } = Just rs
+ifMaybeRoles IfaceClass   { ifRoles = rs } = Just rs
+ifMaybeRoles _ = Nothing
+
 -- | Merge two 'IfaceDecl's together, preferring a non-abstract one.  If
 -- both are non-abstract we pick one arbitrarily (and check for consistency
 -- later.)
 mergeIfaceDecl :: IfaceDecl -> IfaceDecl -> IfaceDecl
 mergeIfaceDecl d1 d2
-    | isAbstractIfaceDecl d1 = d2
-    | isAbstractIfaceDecl d2 = d1
+    -- TODO: need to merge roles
+    | isAbstractIfaceDecl d1 = d2 `withRolesFrom` d1
+    | isAbstractIfaceDecl d2 = d1 `withRolesFrom` d2
     | IfaceClass{ ifSigs = ops1, ifMinDef = bf1 } <- d1
     , IfaceClass{ ifSigs = ops2, ifMinDef = bf2 } <- d2
     = let ops = nameEnvElts $
                   plusNameEnv_C mergeIfaceClassOp
                     (mkNameEnv [ (n, op) | op@(IfaceClassOp n _ _) <- ops1 ])
                     (mkNameEnv [ (n, op) | op@(IfaceClassOp n _ _) <- ops2 ])
-      in d1 { ifSigs = ops
+      in d1 { 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
+
+withRolesFrom :: IfaceDecl -> IfaceDecl -> IfaceDecl
+d1 `withRolesFrom` d2
+    | Just roles1 <- ifMaybeRoles d1
+    , Just roles2 <- ifMaybeRoles d2
+    = d1 { ifRoles = mergeRoles roles1 roles2 }
+    | otherwise = d1
+  where
+    mergeRoles roles1 roles2 = zipWith max roles1 roles2
 
 mergeIfaceClassOp :: IfaceClassOp -> IfaceClassOp -> IfaceClassOp
 mergeIfaceClassOp op1@(IfaceClassOp _ _ (Just _)) _ = op1
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index dafc4b8636..d4a83f13de 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -976,7 +976,7 @@ checkBootTyCon is_boot tc1 tc2
          eqListBy (eqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
          eqListBy (eqTypeX env) (mkTyVarTys bs1) (mkTyVarTys bs2)
     in
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
           -- Checks kind of class
     check (eqListBy eqFD clas_fds1 clas_fds2)
           (text "The functional dependencies do not match") `andThenCheck`
@@ -996,7 +996,7 @@ checkBootTyCon is_boot tc1 tc2
   , Just syn_rhs2 <- synTyConRhs_maybe tc2
   , Just env <- eqVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
     check (eqTypeX env syn_rhs1 syn_rhs2) empty   -- nothing interesting to say
 
   -- An abstract TyCon can be implemented using a type synonym, but ONLY
@@ -1034,7 +1034,7 @@ checkBootTyCon is_boot tc1 tc2
         --      type T = K Int
         --
         -- we need to drop the first role of K when comparing!
-        check (roles1 == drop (length args) (tyConRoles tc2')) roles_msg
+        checkRoles roles1 (drop (length args) (tyConRoles tc2'))
 
   -- Note [Constraint synonym implements abstract class]
   -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1066,11 +1066,10 @@ checkBootTyCon is_boot tc1 tc2
     -- massage it into the correct form before checking if roles
     -- match.
     if length tvs == length roles1
-        then check (roles1 == roles2) roles_msg
+        then checkRoles roles1 roles2
         else case tcSplitTyConApp_maybe ty of
                 Just (tc2', args) ->
-                    check (roles1 == drop (length args) (tyConRoles tc2') ++ roles2)
-                          roles_msg
+                    checkRoles roles1 (drop (length args) (tyConRoles tc2') ++ roles2)
                 Nothing -> Just roles_msg
     -- TODO: We really should check if the fundeps are satisfied, but
     -- there is not an obvious way to do this for a constraint synonym.
@@ -1094,7 +1093,7 @@ checkBootTyCon is_boot tc1 tc2
         injInfo2 = familyTyConInjectivityInfo tc2
     in
     -- check equality of roles, family flavours and injectivity annotations
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
     check (eqFamFlav fam_flav1 fam_flav2)
         (ifPprDebug $
             text "Family flavours" <+> ppr fam_flav1 <+> text "and" <+> ppr fam_flav2 <+>
@@ -1104,7 +1103,7 @@ checkBootTyCon is_boot tc1 tc2
   | isAlgTyCon tc1 && isAlgTyCon tc2
   , Just env <- eqVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
     check (eqListBy (eqTypeX env)
                      (tyConStupidTheta tc1) (tyConStupidTheta tc2))
           (text "The datatype contexts do not match") `andThenCheck`
@@ -1112,12 +1111,24 @@ checkBootTyCon is_boot tc1 tc2
 
   | otherwise = Just empty   -- two very different types -- should be obvious
   where
-    roles1 = tyConRoles tc1
+    roles1 = tyConRoles tc1 -- the abstract one
     roles2 = tyConRoles tc2
     roles_msg = text "The roles do not match." $$
                 (text "Roles on abstract types default to" <+>
                  quotes (text "representational") <+> text "in boot files.")
 
+    roles_subtype_msg = text "The roles are not compatible:" $$
+                        text "Main module:" <+> ppr roles2 $$
+                        text "Hsig file:" <+> ppr roles1
+
+    checkRoles r1 r2
+      | is_boot   = check (r1 == r2) roles_msg
+      | otherwise = check (r2 `rolesSubtypeOf` r1) roles_subtype_msg
+
+    rolesSubtypeOf [] [] = True
+    rolesSubtypeOf (x:xs) (y:ys) = x >= y && rolesSubtypeOf xs ys
+    rolesSubtypeOf _ _ = False
+
     eqAlgRhs _ AbstractTyCon _rhs2
       = checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon
     eqAlgRhs _  tc1@DataTyCon{} tc2@DataTyCon{} =
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index a45df3ade6..b21cb911d7 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -198,8 +198,8 @@ tcTyClDecls tyclds role_annots
             -- type synonyms, as we have not tested for type synonym
             -- loops yet and could fall into a black hole.
        ; fixM $ \ ~rec_tyclss -> do
-           { is_boot   <- tcIsHsBootOrSig
-           ; let roles = inferRoles is_boot role_annots rec_tyclss
+           { tcg_env <- getGblEnv
+           ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
 
                  -- Populate environment with knot-tied ATyCon for TyCons
                  -- NB: if the decls mention any ill-staged data cons
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 96154cca8b..626a1e8cfc 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -452,20 +452,20 @@ type RoleEnv = NameEnv [Role]        -- from tycon names to roles
 -- This, and any of the functions it calls, must *not* look at the roles
 -- field of a tycon we are inferring roles about!
 -- See Note [Role inference]
-inferRoles :: Bool -> RoleAnnotEnv -> [TyCon] -> Name -> [Role]
-inferRoles is_boot annots tycons
-  = let role_env  = initialRoleEnv is_boot annots tycons
+inferRoles :: HscSource -> RoleAnnotEnv -> [TyCon] -> Name -> [Role]
+inferRoles hsc_src annots tycons
+  = let role_env  = initialRoleEnv hsc_src annots tycons
         role_env' = irGroup role_env tycons in
     \name -> case lookupNameEnv role_env' name of
       Just roles -> roles
       Nothing    -> pprPanic "inferRoles" (ppr name)
 
-initialRoleEnv :: Bool -> RoleAnnotEnv -> [TyCon] -> RoleEnv
-initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
-                                map (initialRoleEnv1 is_boot annots)
+initialRoleEnv :: HscSource -> RoleAnnotEnv -> [TyCon] -> RoleEnv
+initialRoleEnv hsc_src annots = extendNameEnvList emptyNameEnv .
+                                map (initialRoleEnv1 hsc_src annots)
 
-initialRoleEnv1 :: Bool -> RoleAnnotEnv -> TyCon -> (Name, [Role])
-initialRoleEnv1 is_boot annots_env tc
+initialRoleEnv1 :: HscSource -> RoleAnnotEnv -> TyCon -> (Name, [Role])
+initialRoleEnv1 hsc_src annots_env tc
   | isFamilyTyCon tc      = (name, map (const Nominal) bndrs)
   | isAlgTyCon tc         = (name, default_roles)
   | isTypeSynonymTyCon tc = (name, default_roles)
@@ -495,9 +495,39 @@ initialRoleEnv1 is_boot annots_env tc
 
         default_role
           | isClassTyCon tc               = Nominal
-          | is_boot && isAbstractTyCon tc = Representational
+          -- Note [Default roles for abstract TyCons in hs-boot/hsig]
+          | HsBootFile <- hsc_src
+          , isAbstractTyCon tc            = Representational
+          | HsigFile   <- hsc_src
+          , isAbstractTyCon tc            = Nominal
           | otherwise                     = Phantom
 
+-- Note [Default roles for abstract TyCons in hs-boot/hsig]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- What should the default role for an abstract TyCon be?
+--
+-- Originally, we inferred phantom role for abstract TyCons
+-- in hs-boot files, because the type variables were never used.
+--
+-- This was silly, because the role of the abstract TyCon
+-- was required to match the implementation, and the roles of
+-- data types are almost never phantom.  Thus, in ticket #9204,
+-- the default was changed so be representational (the most common case).  If
+-- the implementing data type was actually nominal, you'd get an easy
+-- to understand error, and add the role annotation yourself.
+--
+-- Then Backpack was added, and with it we added role *subtyping*
+-- the matching judgment: if an abstract TyCon has a nominal
+-- parameter, it's OK to implement it with a representational
+-- parameter.  But now, the representational default is not a good
+-- one, because you should *only* request representational if
+-- you're planning to do coercions. To be maximally flexible
+-- with what data types you will accept, you want the default
+-- for hsig files is nominal.  We don't allow role subtyping
+-- with hs-boot files (it's good practice to give an exactly
+-- accurate role here, because any types that use the abstract
+-- type will propagate the role information.)
+
 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
 irGroup env tcs
   = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
diff --git a/compiler/types/CoAxiom.hs b/compiler/types/CoAxiom.hs
index fcbf4e83f7..6d66fb80b1 100644
--- a/compiler/types/CoAxiom.hs
+++ b/compiler/types/CoAxiom.hs
@@ -419,6 +419,9 @@ Roles are defined here to avoid circular dependencies.
 
 -- See Note [Roles] in Coercion
 -- defined here to avoid cyclic dependency with Coercion
+--
+-- Order of constructors matters: the Ord instance coincides with the *super*typing
+-- relation on roles.
 data Role = Nominal | Representational | Phantom
   deriving (Eq, Ord, Data.Data)
 
diff --git a/docs/users_guide/separate_compilation.rst b/docs/users_guide/separate_compilation.rst
index 280631a7df..743822f4fc 100644
--- a/docs/users_guide/separate_compilation.rst
+++ b/docs/users_guide/separate_compilation.rst
@@ -909,11 +909,19 @@ to ``hs-boot`` files, but with some slight changes:
   ``type Elem = Char``, you can now use ``head`` from the
   inherited signature as if it returned a ``Char``.
 
-  If you do not write out the constructors, you may need to give
-  a kind and/or role annotation to tell GHC what the kinds or roles
-  of the type variables are, if they are not the default (``*`` and
-  representational).  It will be obvious if you've gotten it wrong when
-  you try implementing the signature.
+  If you do not write out the constructors, you may need to give a kind to tell
+  GHC what the kinds of the type variables are, if they are not the default
+  ``*``.
+
+  Roles of type parameters are subject to the subtyping
+  relation ``phantom < representational < nominal``: for example,
+  an abstract type with a nominal type parameter can be implemented
+  using a concrete type with a representational type parameter.
+  Roles in signatures default to ``nominal``, which gives maximum
+  flexibility on the implementor's side.  You should only need to
+  give an explicit role annotation if a client of the signature
+  would like to coerce the abstract type in a type parameter (in which case you
+  should specify ``representational`` explicitly.)
 
 - A class declarations can either be abstract or concrete.  An
   abstract class is one with no superclasses or class methods::
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, [''])
diff --git a/testsuite/tests/backpack/should_fail/bkpfail25.stderr b/testsuite/tests/backpack/should_fail/bkpfail25.stderr
index 936fbb561b..1a9c573157 100644
--- a/testsuite/tests/backpack/should_fail/bkpfail25.stderr
+++ b/testsuite/tests/backpack/should_fail/bkpfail25.stderr
@@ -19,5 +19,6 @@ bkpfail25.bkp:12:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
       Main module: type T a = a
-      Hsig file:  data T a
+      Hsig file:  type role T nominal
+                  data T a
     • while checking that q:H implements signature H in p[H=q:H]
diff --git a/testsuite/tests/backpack/should_fail/bkpfail26.stderr b/testsuite/tests/backpack/should_fail/bkpfail26.stderr
index 01c8c32d1e..3de59a22c7 100644
--- a/testsuite/tests/backpack/should_fail/bkpfail26.stderr
+++ b/testsuite/tests/backpack/should_fail/bkpfail26.stderr
@@ -14,7 +14,8 @@ bkpfail26.bkp:15:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
       Main module: type T a = [a]
-      Hsig file:  data T a
+      Hsig file:  type role T nominal
+                  data T a
       Illegal parameterized type synonym in implementation of abstract data.
       (Try eta reducing your type synonym so that it is nullary.)
     • while checking that q:H implements signature H in p[H=q:H]