[GHC] #13358: Role ranges (allow decomposition on newtypes)

[GHC]

#13358: Role ranges (allow decomposition on newtypes)
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  backpack       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Extracted from #13140.

 Today, there is a strange asymmetry between data types, for which the
 decomposition rule holds (if `T A ~R T B` then `A ~ρ B`, where ρ is the
 role of the type), and newtypes, for which the decomposition rule is
 unsound.

 I believe the root cause of this problem is the fact that we only maintain
 a single role per type parameter, while in fact what we need is a role
 *range* (i.e., and lower and upper role bound) to specify what inferences
 can be made about a type. Here's how it works.

 Every type parameter is ascribed a role range, specifying the possible
 roles by which the type parameter might possibly be used. For example, if
 I write `data T a = MkT a`, `a` is used exactly at representational role,
 but we could also say that a *might* be used nominally, giving the role
 range nominal-representational.

 The lower bound (nominal is lowest in subroling) specifies at what role
 the application rule is valid: if I say that the role is at least nominal,
 then I must provide `a ~N b` evidence to show that `T a ~R T b`. The upper
 bound (phantom is highest) specifies at what role the decomposition rule
 is valid. If I say that the role is at most phantom, I learn nothing from
 decomposition; but if I say the role is at most representational, when `T
 A ~R T B`, I learn `A ~R B`. Clearly, the role range nominal-phantom
 permits the most implementations, but gives the client the least
 information about equalities.

 How do we tell if a role range is compatible with a type? The lower bound
 (what we call a role today) is computed by propagating roles through, but
 allowing substitution of roles as per the subroling relationship `N <= R
 <= P`. To compute the upper bound, we do exactly the same rules, but with
 the opposite subroling relation: `P <= R <= N`.

 Some 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
 }}}

 Richard wonders if we could use this to solve the "recursive newtype
 unwrapping" problem. Unfortunately, because our solver is guess-free, we
 must also maintain the most precise role for every type constructor. See
 https://ghc.haskell.org/trac/ghc/ticket/13140#comment:12

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