#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