#13140: Handle subtyping relation for roles in Backpack -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: patch Priority: normal | Milestone: 8.4.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): On SPJ's request: here are concrete examples showing that no choice of existing role is suitable for being "abstract": * Suppose we pick `nominal` to be abstract. Let `T` be `nominal` in its first argument: if we have `T a ~R T b`, we can derive `a ~N b`. Now set `T` to `phantom`, then we have `Int ~P Bool` and consequently `T Int ~R T Bool`. This lets us derive `Int ~N Bool`, bad! * Suppose we pick `phantom` to be abstract. Let `T` be `phantom` in its first argument: then we have `T Int ~R T Bool` for all a and b. Now set `T` to `nominal`; if `T a ~R T b`, then `a ~N b`; thus we have `Int ~N Bool`. Bad! * Suppose we pick `representational` to be abstract. Let `T` be `representational` in its first argument: then we have that if `T a ~R T b`, then `a ~R b`. Now set `T` to `phantom`, then we have `Int ~P Bool` and consequently `T Int ~R T Bool`. But this implies `Int ~R Bool`, bad! (You can also do the other proof on this one.) Another question was this: why doesn't subroling break this way? Subroling says that if we have a type variable `a` at some role ρ, we can use it at role ρ' so long as ρ <= ρ'. (N is a subrole of everything). So for example, the following is acceptable: {{{ data T a = MkT a type role S nominal data S a = MkS (T a) }}} In S, a is at role nominal, but we can pass it to a T which has a at role representational. What we are afraid of is having `T a ~R T b` imply `a ~N b` by using S. But from the hypothesis we get is `a ~R b`, which does NOT imply `S a ~R S b` (S is nominal!). Another interesting observation is how we treat a polymorphic type constructor, e.g., m in `forall m. m a -> m a`. Via the Co_App rule, to show `m a ~ρ m' b` we must show `m ~N m'` and `a ~ρ b` (like the nominal role). Via the Co_Left rules, we can only say `a ~N b` if `m a ~N m' b` (just like the phantom role, we learn nothing when `m a ~R m' b`). So the "abstract" role implicitly falls out of the way the coercion formation rules handle type variables! All of this seems like evidence that adding an abstract role annotation is "the right thing to do." -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler