Commit df919fb2 authored by Edward Z. Yang's avatar Edward Z. Yang

Fix roles merging to apply only to non-rep-injective types.

Test Plan: validate

Reviewers: simonpj

Subscribers:
parent fb5cd9d6
......@@ -235,20 +235,65 @@ mergeIfaceDecl d1 d2
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
-- Note [Role merging]
-- ~~~~~~~~~~~~~~~~~~~
-- First, why might it be necessary to do a non-trivial role
-- merge? It may rescue a merge that might otherwise fail:
--
-- signature A where
-- type role T nominal representational
-- data T a b
--
-- signature A where
-- type role T representational nominal
-- data T a b
--
-- A module that defines T as representational in both arguments
-- would successfully fill both signatures, so it would be better
-- if if we merged the roles of these types in some nontrivial
-- way.
--
-- However, we have to be very careful about how we go about
-- doing this, because role subtyping is *conditional* on
-- the supertype being NOT representationally injective, e.g.,
-- if we have instead:
--
-- signature A where
-- type role T nominal representational
-- data T a b = T a b
--
-- signature A where
-- type role T representational nominal
-- data T a b = T a b
--
-- Should we merge the definitions of T so that the roles are R/R (or N/N)?
-- Absolutely not: neither resulting type is a subtype of the original
-- types (see Note [Role subtyping]), because data is not representationally
-- injective.
--
-- Thus, merging only occurs when BOTH TyCons in question are
-- representationally injective. If they're not, no merge.
withRolesFrom :: IfaceDecl -> IfaceDecl -> IfaceDecl
d1 `withRolesFrom` d2
| Just roles1 <- ifMaybeRoles d1
, Just roles2 <- ifMaybeRoles d2
, not (isRepInjectiveIfaceDecl d1 || isRepInjectiveIfaceDecl d2)
= d1 { ifRoles = mergeRoles roles1 roles2 }
| otherwise = d1
where
mergeRoles roles1 roles2 = zipWith max roles1 roles2
isRepInjectiveIfaceDecl :: IfaceDecl -> Bool
isRepInjectiveIfaceDecl IfaceData{ ifCons = IfDataTyCon _ } = True
isRepInjectiveIfaceDecl IfaceFamily{ ifFamFlav = IfaceDataFamilyTyCon } = True
isRepInjectiveIfaceDecl _ = False
mergeIfaceClassOp :: IfaceClassOp -> IfaceClassOp -> IfaceClassOp
mergeIfaceClassOp op1@(IfaceClassOp _ _ (Just _)) _ = op1
mergeIfaceClassOp _ op2 = op2
......
......@@ -44,6 +44,7 @@ test('bkp49', normal, backpack_compile, [''])
test('bkp50', normal, backpack_compile, [''])
test('bkp51', normal, backpack_compile, [''])
test('bkp52', normal, backpack_compile, [''])
test('bkp53', normal, backpack_compile, [''])
test('T13140', normal, backpack_compile, [''])
test('T13149', expect_broken(13149), backpack_compile, [''])
......
{-# LANGUAGE RoleAnnotations #-}
-- Role merging test
unit p where
signature A where
type role T nominal representational
data T a b
newtype S a b = MkS (T a b)
unit q where
signature A where
type role T representational nominal
data T a b
newtype S a b = MkS (T a b)
unit r where
dependency p[A=<A>]
dependency q[A=<A>]
module M where
import A
import Data.Coerce
f :: (Coercible a1 a2, Coercible b1 b2) => T a1 b1 -> T a2 b2
f = coerce
g :: (Coercible a1 a2, Coercible b1 b2) => S a1 b1 -> S a2 b2
g = coerce
[1 of 3] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 3] Processing q
[1 of 1] Compiling A[sig] ( q/A.hsig, nothing )
[3 of 3] Processing r
[1 of 2] Compiling A[sig] ( r/A.hsig, nothing )
[2 of 2] Compiling M ( r/M.hs, nothing )
......@@ -42,3 +42,4 @@ test('bkpfail43', normal, backpack_compile_fail, [''])
test('bkpfail44', normal, backpack_compile_fail, [''])
test('bkpfail45', normal, backpack_compile_fail, [''])
test('bkpfail46', normal, backpack_compile_fail, [''])
test('bkpfail47', normal, backpack_compile_fail, [''])
{-# LANGUAGE RoleAnnotations #-}
unit p where
signature A where
type role T nominal representational
data T a b
unit q where
signature A where
type role T representational nominal
data T a b = MkT
unit r where
dependency p[A=<A>]
dependency q[A=<A>]
[1 of 3] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 3] Processing q
[1 of 1] Compiling A[sig] ( q/A.hsig, nothing )
[3 of 3] Processing r
[1 of 1] Compiling A[sig] ( r/A.hsig, nothing )
bkpfail47.bkp:9:9: error:
• Type constructor ‘T’ has conflicting definitions in the module
and its hsig file
Main module: type role T representational nominal
data T a b = MkT
Hsig file: type role T nominal representational
data T a b
The roles are not compatible:
Main module: [representational, nominal]
Hsig file: [nominal, representational]
• while merging the signatures from:
• p[A=<A>]:A
• q[A=<A>]:A
• ...and the local signature for 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