Commit 4aada7a6 authored by Edward Z. Yang's avatar Edward Z. Yang

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: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, austin, simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3222
parent f56fc7f7
......@@ -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
......
......@@ -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, [''])
{-# 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
[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)
{-# 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
[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]
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment