Handle subtyping relation for roles in Backpack

changed milestone to %8.2.1

changed weight to 5

added Tfeature request Trac import backpack hs-boot typechecker labels

Trac metadata

Trac field	Value
Differential revisions	- → D3123

Sorry for not piping up sooner, but this change would be unsound. Consider this accepted program:

data T a
type role T nominal

foo :: Coercible (T a) (T b) => a -> b
foo x = x

You can see that, if T were abstract, instantiating T with a concrete datatype that had a phantom role would be Wrong. While there is a sub-roling relationship, it does not induce a sub-typing relationship like the one you seek.

Blah, that's terrible.

I'm trying to think how to solve this problem, because role mismatches in Backpack signatures are actually a problem in practice, that can't be easily worked around (speaking from experience Backpack'ing the reflex library). Let's leave aside hs-boot for now, where I think the current design works reasonably well.

Here is my proposal: let's introduce a new "abstract" role which is a blend of the phantom and nominal roles:

Like phantom roles, we want a ~A b (where A is the abstract role) to hold for all choices a and b. Then, because the Co_Nth rule says that if H a ~R H b, then a ~ρ b (where ρ is the role of the first type parameter of H), when H's role is abstract, we learn nothing about a and b. This is sufficient to cause your example to fail to typecheck.
Like nominal roles, we should only have H a ~R H b if a ~N b; we would adjust the Co_TyConApp rule to always require nominal equality whenever we are at an abstract role type parameter.

Since there are no rules where you can use a ~A b to derive another form of equality (in particular, we modified Co_TyConApp to require nominal equality), the existing safety proof should go through without modification.

How does this sound?

If, from your perspective, the added complexity is worth it, then this looks OK to me.

What's frustrating here is that we don't really need a new Abstract equality relation: the current Phantom one works fine. All we need is a new role annotation. Is it worth creating a new data RoleAnnotation = Abstract | Concrete Role? Perhaps. You would also then need to be careful about uses of tyConRoles and tyConRolesX, as they are currently used both for construction and decomposition -- up until this proposal, both directions were happy with the same roles.

I do agree that your approach is type safe. But I have to wonder if there isn't a simpler solution somehow, as I'm hesitant to advocate yet another wrinkle to the role system.

I'm not convinced the complexity is worth it. I think at least for GHC 8.2 we ought not to put in any of this, and we'll see if the role problems really cause people problems.

changed milestone to %8.4.1

Alright, if I understand correctly nothing will be happing on this front until 8.4 at the earliest.

On SPJ's request: here are concrete examples showing that no choice of existing role is suitable for being "abstract":

Suppose we pick nominal to be abstract. Let T be nominal in its first argument: if we have T a ~R T b, we can derive a ~N b. Now set T to phantom, then we have Int ~P Bool and consequently T Int ~R T Bool. This lets us derive Int ~N Bool, bad!
Suppose we pick phantom to be abstract. Let T be phantom in its first argument: then we have T Int ~R T Bool for all a and b. Now set T to nominal; if T a ~R T b, then a ~N b; thus we have Int ~N Bool. Bad!
Suppose we pick representational to be abstract. Let T be representational in its first argument: then we have that if T a ~R T b, then a ~R b. Now set T to phantom, then we have Int ~P Bool and consequently T Int ~R T Bool. But this implies Int ~R Bool, bad! (You can also do the other proof on this one.)

Another question was this: why doesn't subroling break this way? Subroling says that if we have a type variable a at some role ρ, we can use it at role ρ' so long as ρ <= ρ'. (N is a subrole of everything). So for example, the following is acceptable:

data T a = MkT a
type role S nominal
data S a = MkS (T a)

In S, a is at role nominal, but we can pass it to a T which has a at role representational. What we are afraid of is having T a ~R T b imply a ~N b by using S. But from the hypothesis we get is a ~R b, which does NOT imply S a ~R S b (S is nominal!).

Another interesting observation is how we treat a polymorphic type constructor, e.g., m in forall m. m a -> m a. Via the Co_App rule, to show m a ~ρ m' b we must show m ~N m' and a ~ρ b (like the nominal role). Via the Co_Left rules, we can only say a ~N b if m a ~N m' b (just like the phantom role, we learn nothing when m a ~R m' b). So the "abstract" role implicitly falls out of the way the coercion formation rules handle type variables!

All of this seems like evidence that adding an abstract role annotation is "the right thing to do."

The Right Thing to do is to go back in time and erase the idea of roles from our brains... and reimplement GeneralizedNewtypeDeriving in terms of a generated blob of source code that gets type-checked (instead of the magical implementation it used to have).

Barring that, I can't find an argument against a new abstract role other than to groan.

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

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.
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.)
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.

I like ticket:13140#comment:132646.

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 paper. But I do remember that the resolution was dissatisfyingly incomplete in the case of recursive newtypes. Perhaps Edward's idea in ticket:13140#comment:132646 -- separate out two sets of roles -- provides a better way forward.

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:

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.
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 (from a completeness perspective) 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.) Actually, (2) is not quite enough: if we have newtype S = MkS S, then we can infinite loop when trying to solve S ~R T S. But this seems to only be a problem when there is no intervening data type; if there is an intervening data type then unwrapping will stop at the data type, we'll unwrap the other side to the data type, we'll do a data decomposition, and NOW newtype decomposition applies.

mentioned in commit 923d7ca2

Here's another way to think about app-roles and proj-roles.

Previously, we thought of roles as a single thing you ascribe to a type parameter. But it would be more accurate to say that a type parameter is given a role range, which specifies the possible set of underlying roles that the type may be implemented with. For example, the range "phantom to nominal" says that the type could be implemented in a way that treats the type variable phantom, representationally, or nominally: this is the most flexible for the implementor and gives the least information to the client. Or you can say that it is "exactly" nominal: this gives the most information to the client. type role T nominal; newtype T a = MkT a gets "representational to nominal": the annotation sets the upper bound, but the lower bound has to actually include the true role which a is used at.

Of course, when I say lower bound, I mean proj-role, and when I say upper-bound, I mean app role. (I also apologize for flipping the subroling order.)

closed

I'm marking this ticket as fixed but I'll open another ticket about role ranges.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

mentioned in issue #13358

added Pnormal label

Trac field	Value
Version	8.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Handle subtyping relation for roles in Backpack

Child items 0

Activity