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

 > Is this because GHC 8.0 (and below) allows an hs-boot file to say data
 where the implementing module says newtype?

 Yep.

 > 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?

 Ah, this is very interesting (also, thank you for telling me about the
 journal paper; I didn't realize you had both an extended mix and a journal
 copy).

 What we would like to do is two things:

 1. Allow decomposition on newtype givens (currently disallowed because
 Co_Nth doesn't work on newtypes). If we use the proj-roles here, that
 should solve the soundness problem.

 2. Do decomposition BEFORE unwrapping, so that if we hit `FixEither Age ~R
 FixEither Int`, we immediately jump to `Age ~R Int`, rather than uselessly
 infinite loop on the newtype unwrapping.

 (2) is a bit trickier. Suppose when you have something like this:

 {{{
 type app  role T nominal
 type proj role T phantom
 newtype T a = MkT a
 }}}

 What "roles" should I use in the decomposition here, if I am trying to
 prove `T Int ~R T Age`? Clearly, the only sound and complete choice is
 representational. Ignoring proj-roles for a moment, the reason we must
 flatten before we decompose, even today, is because if we decomposed the
 constraint above, we would end up with `Int ~N Age` which is unsolvable.

 So, it seems to me, that eager decomposition will go wrong UNLESS you know
 the "exact" roles of the newtype (the role computation without any
 subroling). The subroling doesn't affect soundness but it does affect
 completeness if your constraint solver doesn't backtrack (which ours does
 not.)

 I'm also not sure if just (2) is guaranteed to get us to the point where
 newtype decomposition will actually apply, but the simple examples I
 thought of seemed to work (including the one in the paper.)

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