diff options
author | Edward Z. Yang <ezyang@cs.stanford.edu> | 2017-02-26 20:15:30 -0800 |
---|---|---|
committer | Edward Z. Yang <ezyang@cs.stanford.edu> | 2017-03-02 15:58:16 -0800 |
commit | 4aada7a6c13752652cfce5e04f015a8909553917 (patch) | |
tree | b1cb067394e98218d568951c20f8b48cd28e6877 | |
parent | f56fc7f7fe72f96348d663a83f736c4c8b12b08b (diff) | |
download | haskell-4aada7a6c13752652cfce5e04f015a8909553917.tar.gz |
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
-rw-r--r-- | compiler/typecheck/TcRnDriver.hs | 55 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/all.T | 2 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/bkpfail44.bkp | 10 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/bkpfail44.stderr | 23 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/bkpfail45.bkp | 23 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/bkpfail45.stderr | 22 |
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] |