More comments on role subtyping, unsoundness fix.

Summary:
- We incorrectly allowed subroling on injective data in
  some cases. There is now a test to check for this case, and a Note.

- More commentary on how the subtyping with roles works.

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

Test Plan: validate

Reviewers: goldfire, austin, simonpj, bgamari

Subscribers: thomie

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

6 files changed, 134 insertions, 1 deletions

diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index fe0e908c47..5634891f4f 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1094,6 +1094,8 @@ checkBootTyCon is_boot tc1 tc2
         injInfo2 = familyTyConInjectivityInfo tc2
     in
     -- check equality of roles, family flavours and injectivity annotations
+    -- (NB: Type family roles are always nominal. But the check is
+    -- harmless enough.)
     checkRoles roles1 roles2 `andThenCheck`
     check (eqFamFlav fam_flav1 fam_flav2)
         (ifPprDebug $
@@ -1123,9 +1125,60 @@ checkBootTyCon is_boot tc1 tc2
                         text "Hsig file:" <+> ppr roles1
 
     checkRoles r1 r2
-      | is_boot   = check (r1 == r2) roles_msg
+      | is_boot || isInjectiveTyCon tc1 Representational -- See Note [Role subtyping]
+      = check (r1 == r2) roles_msg
       | otherwise = check (r2 `rolesSubtypeOf` r1) roles_subtype_msg
 
+    -- Note [Role subtyping]
+    -- ~~~~~~~~~~~~~~~~~~~~~
+    -- In the current formulation of roles, role subtyping is only OK if
+    -- the "abstract" TyCon was not injective.  Among the most notable
+    -- examples of non-injective TyCons are abstract data, which can be
+    -- implemented via newtypes (which are not injective).  The key example is
+    -- in this example from #13140:
+    --
+    --      -- In an hsig file
+    --      data T a -- abstract!
+    --      type role T nominal
+    --
+    --      -- Elsewhere
+    --      foo :: Coercible (T a) (T b) => a -> b
+    --      foo x = x
+    --
+    -- We must NOT allow foo to typecheck, because if we instantiate
+    -- T with a concrete data type with a phantom role would cause
+    -- Coercible (T a) (T b) to be provable.  Fortunately, if T
+    -- is not injective, we cannot make the inference that a ~N b
+    -- if T a ~R T b.
+    --
+    -- Unconditional role subtyping would be possible if we setup
+    -- an extra set of roles saying when we can project out coercions
+    -- (we call these proj-roles); then it would NOT be valid to instantiate T
+    -- with a data type at phantom since the proj-role subtyping check
+    -- would fail.  See #13140 for more details.
+    --
+    -- One consequence of this is we get no role subtyping for non-abstract
+    -- data types in signatures. Suppose you have:
+    --
+    --      signature A where
+    --          type role T nominal
+    --          data T a = MkT
+    --
+    -- If you write this, we'll treat T as injective, and make inferences
+    -- like T a ~R T b ==> a ~N b (mkNthCo).  But if we can
+    -- subsequently replace T with one at phantom role, we would then be able to
+    -- infer things like T Int ~R T Bool which is bad news.
+    --
+    -- We could allow role subtyping here if we didn't treat *any* data types
+    -- defined in signatures as injective.  But this would be a bit surprising,
+    -- replacing a data type in a module with one in a signature could cause
+    -- your code to stop typechecking (whereas if you made the type abstract,
+    -- it is more understandable that the type checker knows less).
+    --
+    -- It would have been best if this was purely a question of defaults
+    -- (i.e., a user could explicitly ask for one behavior or another) but
+    -- the current role system isn't expressive enough to do this.
+    -- Having explict proj-roles would solve this problem.
     rolesSubtypeOf [] [] = True
     rolesSubtypeOf (x:xs) (y:ys) = x >= y && rolesSubtypeOf xs ys
     rolesSubtypeOf _ _ = False
diff --git a/testsuite/tests/backpack/should_fail/all.T b/testsuite/tests/backpack/should_fail/all.T
index 9878c79464..77b7aa23d8 100644
--- a/testsuite/tests/backpack/should_fail/all.T
+++ b/testsuite/tests/backpack/should_fail/all.T
@@ -39,3 +39,5 @@ test('bkpfail40', normal, backpack_compile_fail, [''])
 test('bkpfail41', normal, backpack_compile_fail, [''])
 test('bkpfail42', normal, backpack_compile_fail, [''])
 test('bkpfail43', normal, backpack_compile_fail, [''])
+test('bkpfail44', normal, backpack_compile_fail, [''])
+test('bkpfail45', normal, backpack_compile_fail, [''])
diff --git a/testsuite/tests/backpack/should_fail/bkpfail44.bkp b/testsuite/tests/backpack/should_fail/bkpfail44.bkp
new file mode 100644
index 0000000000..fb82f3d6a9
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail44.bkp
@@ -0,0 +1,10 @@
+{-# LANGUAGE RoleAnnotations, FlexibleContexts #-}
+unit p where
+    signature A where
+        type role T nominal -- redundant, but just be sure!
+        data T a
+    module B where
+        import Data.Coerce
+        import A
+        f :: Coercible (T a) (T b) => a -> b
+        f x = x -- should not typecheck! T might be phantom
diff --git a/testsuite/tests/backpack/should_fail/bkpfail44.stderr b/testsuite/tests/backpack/should_fail/bkpfail44.stderr
new file mode 100644
index 0000000000..127083f453
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail44.stderr
@@ -0,0 +1,23 @@
+[1 of 1] Processing p
+  [1 of 2] Compiling A[sig]           ( p/A.hsig, nothing )
+  [2 of 2] Compiling B                ( p/B.hs, nothing )
+
+bkpfail44.bkp:10:15: error:
+    • Could not deduce: a ~ b
+      from the context: Coercible (T a) (T b)
+        bound by the type signature for:
+                   f :: Coercible (T a) (T b) => a -> b
+        at bkpfail44.bkp:9:9-44
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. Coercible (T a) (T b) => a -> b
+        at bkpfail44.bkp:9:9-44
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. Coercible (T a) (T b) => a -> b
+        at bkpfail44.bkp:9:9-44
+    • In the expression: x
+      In an equation for ‘f’: f x = x
+    • Relevant bindings include
+        x :: a (bound at bkpfail44.bkp:10:11)
+        f :: a -> b (bound at bkpfail44.bkp:10:9)
diff --git a/testsuite/tests/backpack/should_fail/bkpfail45.bkp b/testsuite/tests/backpack/should_fail/bkpfail45.bkp
new file mode 100644
index 0000000000..f60d45fd6a
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail45.bkp
@@ -0,0 +1,23 @@
+{-# LANGUAGE RoleAnnotations, FlexibleContexts #-}
+unit p where
+    signature A where
+        type role T nominal
+        data T a = T
+    module B where
+        import Data.Coerce
+        import A
+        f :: Coercible (T a) (T b) => a -> b
+        f x = x
+unit a where
+    module A where
+        data T a = T
+unit q where
+    dependency p[A=a:A]
+    module C where
+        import B
+        g :: a -> b
+        g = f
+
+-- Either:
+--  a) B should fail to typecheck against the signature, or
+--  b) A should fail to match against the signature
diff --git a/testsuite/tests/backpack/should_fail/bkpfail45.stderr b/testsuite/tests/backpack/should_fail/bkpfail45.stderr
new file mode 100644
index 0000000000..737769384d
--- /dev/null
+++ b/testsuite/tests/backpack/should_fail/bkpfail45.stderr
@@ -0,0 +1,22 @@
+[1 of 3] Processing p
+  [1 of 2] Compiling A[sig]           ( p/A.hsig, nothing )
+  [2 of 2] Compiling B                ( p/B.hs, nothing )
+[2 of 3] Processing a
+  Instantiating a
+  [1 of 1] Compiling A                ( a/A.hs, bkpfail45.out/a/A.o )
+[3 of 3] Processing q
+  Instantiating q
+  [1 of 1] Including p[A=a:A]
+    Instantiating p[A=a:A]
+    [1 of 2] Compiling A[sig]           ( p/A.hsig, bkpfail45.out/p/p-KvF5Y9pEVY39j64PHPNj9i/A.o )
+
+bkpfail45.bkp:13:9: error:
+    • Type constructor ‘T’ has conflicting definitions in the module
+      and its hsig file
+      Main module: type role T phantom
+                   data T a = T
+      Hsig file:  type role T nominal
+                  data T a = T
+      The roles do not match.
+      Roles on abstract types default to ‘representational’ in boot files.
+    • while checking that a:A implements signature A in p[A=a:A]