[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 goldfire):

 I like comment:10.

 I had forgotten that abstract types were not injective w.r.t.
 representational equality. Is this because GHC 8.0 (and below) allows an
 hs-boot file to say `data` where the implementing module says `newtype`? I
 can't think of another reason. In any case, this is a happy ending to your
 story.

 As for the app-roles vs. proj-roles: very interesting. Currently, the
 solver runs into a problem when proving, say, `N a ~R N b`, where `N` is a
 newtype whose constructor is in scope: should we unwrap the newtype? Or
 use decomposition? (Note that this is somewhat the converse problem to the
 discussion above. Here we're trying to ''prove'' `N a ~R N b`; previous
 discussion assumed `N a ~R N b` and was trying to learn about `a` and
 `b`.) I forget exactly what happens here -- it's all in the
 [http://cs.brynmawr.edu/~rae/papers/2016/coercible-jfp/coercible-jfp.pdf
 paper]. But I do remember that the resolution was dissatisfyingly
 incomplete in the case of recursive newtypes. Perhaps Edward's idea in
 comment:10 -- separate out two sets of roles -- provides a better way
 forward.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13140#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler