#13140: Handle subtyping relation for roles in Backpack -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: backpack hs- Resolution: | boot Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3123 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): Blah, that's terrible. I'm trying to think how to solve this problem, because role mismatches in Backpack signatures are actually a problem in practice, that can't be easily worked around (speaking from experience Backpack'ing the reflex library). Let's leave aside hs-boot for now, where I think the current design works reasonably well. Here is my proposal: let's introduce a new "abstract" role which is a blend of the phantom and nominal roles: * Like phantom roles, we want `a ~A b` (where A is the abstract role) to hold for all choices a and b. Then, because the Co_Nth rule says that if `H a ~R H b`, then `a ~ρ b` (where ρ is the role of the first type parameter of H), when H's role is abstract, we learn nothing about a and b. This is sufficient to cause your example to fail to typecheck. * Like nominal roles, we should only have `H a ~R H b` if `a ~N b`; we would adjust the Co_TyConApp rule to always require nominal equality whenever we are at an abstract role type parameter. Since there are no rules where you can use `a ~A b` to derive another form of equality (in particular, we modified `Co_TyConApp` to require nominal equality), the existing safety proof should go through without modification. How does this sound? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler