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

 After spending some time thinking through the proofs, I realized that
 goldfire's counterexample isn't actually valid, and we only need to do
 something complicated if we want to augment roles with a more fine-grained
 notion of injectivity.

 First, let's see how GHC rejects goldfire's example today, via hs-boot
 files:

 {{{
 -- A.hs-boot
 {-# LANGUAGE RoleAnnotations #-}
 module A where
 data T a
 type role T nominal

 -- B.hs
 {-# LANGUAGE FlexibleContexts, RoleAnnotations #-}
 module B where
 import {-# SOURCE #-} A
 import Data.Coerce
 foo :: Coercible (T a) (T b) => a -> b
 foo x = x

 -- A.hs
 -- Doesn't really matter, but this will do:
 {-# LANGUAGE RoleAnnotations #-}
 module A where
 import B
 type role T nominal
 newtype T a = T Int
 }}}

 When we compile, we get:

 {{{
 B.hs:6:9: error:
     • Could not deduce: a ~ b
       from the context: Coercible (T a) (T b)
         bound by the type signature for:
                    foo :: Coercible (T a) (T b) => a -> b
         at B.hs:5:1-38
       ‘a’ is a rigid type variable bound by
         the type signature for:
           foo :: forall a b. Coercible (T a) (T b) => a -> b
         at B.hs:5:1-38
       ‘b’ is a rigid type variable bound by
         the type signature for:
           foo :: forall a b. Coercible (T a) (T b) => a -> b
         at B.hs:5:1-38
     • In the expression: x
       In an equation for ‘foo’: foo x = x
     • Relevant bindings include
         x :: a (bound at B.hs:6:5)
         foo :: a -> b (bound at B.hs:6:1)
 }}}

 This is because GHC only applies the Co_Nth rule if the TyCon in question
 is *injective*, and abstract types are NOT injective. In fact, they're
 obviously not because I can implement an abstract data type with a newtype
 (as I do in my example), and as was demonstrated in the roles paper, it is
 unsound to Co_Nth on newtypes. So, all we have to do is make sure Backpack
 abstract data types are not injective (and indeed, they're not) and
 there's no problem.

 During our phone call, SPJ noticed that we could just unconditionally
 disable the Co_Nth rule if the TyCon was abstract or not (I didn't realize
 that they would already have been disabled), but we decided that the
 "abstract" strategy made more sense because you might *want* to say, "Hey,
 actually, I really do want you to be able to use Co_Nth on this
 parameter." Maybe it is worth investigating this, but for now I think it
 should be OK to merge Phab:D3123.

 ----

 Since I've been thinking about this, let us talk about Co_Nth on newtypes.
 Consider the following program:

 {{{
 newtype T a = MkT a
 }}}

 Given `T a ~R T b`, I might like to infer that `a ~R b`. If T were a data
 type, I could do this directly, but with newtypes, since Co_Nth doesn't
 apply, I have to take a roundabout route: I show `T a ~R a` and `T b ~R b`
 (by the newtype axiom) and then apply transitivity to pop out the final
 coercion.

 Under what situations would it be safe to apply Co_Nth here? Intuitively,
 the problem is that ascribed role for the parameter of T might not
 accurately describe how a is actually used in the body of the newtype,
 because it may have been weakened by subroling. That's bad news for
 Co_Nth, which really needs subroling to go "in the other direction."

 I conjecture the following system would be sound:

 1. Associate every declaration with two sets of roles: one set that is
 applied in Co_TyConApp (call this the app-roles) and one that is applied
 for Co_Nth (call this the proj-roles). For data types, these are always
 the same.

 2. For newtypes, the app-roles are specified by the existing role
 assignment rules. However, the proj-roles are specified by the role
 assignment rules with the subroling relationship *flipped*: i.e., phantom
 is a subrole of nominal (not the other way around.)

 3. Proj-roles can be inferred like app-roles, but they are always
 consistent with proj-roles, and the subroling relationship is flipped.

 Here are a few examples:

 {{{
 type app  role T representational
 type proj role T representational
 newtype T a = MkT a
 -- T a ~R T b implies a ~R b

 type app  role T nominal
 type proj role T representational
 -- NB: type proj role T nominal is NOT ALLOWED
 newtype T a = MkT a
 -- T a ~R T b implies a ~R b, BUT
 -- a ~R b is insufficient to prove T a ~R T b (you need a ~N b)

 type app role T nominal
 type proj role T phantom -- (representational and nominal not allowed)
 newtype T a = MkT Int
 -- T a ~R T b implies a ~P b (i.e. we don't learn anything)
 -- a ~N b implies T a ~R T b
 }}}

 To relate this back to the "abstract" role, what I have been calling an
 abstract role is actually a nominal app-role but phantom proj-role (i.e.,
 the most flexible role of them all.) I ran into trouble trying to figure
 out how to infer abstractness, but I think if you make the language more
 expressive, that solves the problem.

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