[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.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