#13140: Handle subtyping relation for roles in Backpack -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: patch Priority: normal | Milestone: 8.2.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 goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13140: Handle subtyping relation for roles in Backpack -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: patch Priority: normal | Milestone: 8.2.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 goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.1 => 8.4.1 Comment: Alright, if I understand correctly nothing will be happing on this front until 8.4 at the earliest. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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

#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): 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler