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

[GHC]

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

Old description:

> 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

New description:

 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 role T representational..representational
 newtype T a = MkT a
 -- T a ~R T b implies a ~R b

 type role T nominal..representational -- NB: nominal..nominal illegal!
 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 role T nominal..phantom -- NB: nominal..representational illegal!
 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler