[GHC] #13140: Handle subtyping relation for roles in Backpack

[GHC]

#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