...  ...  @@ 308,7 +308,7 @@ coerceOp= coerce 


```









Since the role signature for `Op` is `type role Op nominal nominal nominal`. But in an ideal world, the role signature for `Op` would be inferred as `type role Op nominal representational representational`. After all, neither `a` nor `b` is "scrutinized" in any sense, so it feels perfectly safe to coerce them freely.



Since the role signature for `Op` is `type role Op nominal nominal nominal`. But in an ideal world, the role signature for `Op` would be inferred as `type role Op nominal representational representational`. After all, neither `a` nor `b` is "scrutinized" in any sense, so it feels perfectly safe to coerce them freely. **RAE:** "feels"? Let's prove it! **End RAE**









Another example ([ courtesy of intindex](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:33)) is:

...  ...  @@ 351,19 +351,46 @@ typefamilyF a 





But this is a restriction that is easily overcome. In addition, the parser does not currently recognize role annotations for associated type families:






```



classC a wheretype role Assoc nominal nominal



typeAssoc a b



```






{{\#!hs



class C a where






>



> type role Assoc nominal nominal



> type Assoc a b



But this could be added without much difficulty.






**RAE:** There is a difference between roles for



data families and data instances. And both might usefully



have role annotations. For example:






}}}



```



datafamilyDF a b



type role DF nominal representational






datainstanceDFInt b =MkDFInt b



 NB: No scrutinizing the second parameter. Also, b is not used in a nominal contextdatainstanceDF[c] b =MkDFList c b



type role DF[nominal] representational






But this could be added without much difficulty.



datainstanceDF(Maybe d) b =MkDFMaybe d b



type role DF(Maybe representational) representational



```









With this, we have `Coercible (DF (Maybe Age) Int) (DF (Maybe Int) Age)` but not `Coercible (DF [Age] Int) (DF [Int] Age)`.









I *think* (but have not ever tried to prove) that these instance roles would work out, with the following restrictions:






 If a data family parameter is not scrutinized (that is, it's just a bare variable), then the instance role must match the family role exactly.






 Corollary: all representational/phantom roles from the family must be repeated exactly in the instances.






 Other variables may be given new roles according to the usual rules, including the usage of the variable in the instance head as a usage site. (That is, if the variable is used in a nominal context in the instance head, then it must be marked nominal.)









I'm a bit worried about problems with what happens if a type constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation  could we be breaking soundness with this? Need to think harder.






**End RAE**






## Role inference for type families




...  ...  @@ 387,7 +414,7 @@ There are five type parameters for `F`: `k`, `e`, `f`, `g`, and `h`. What should 


### The type family kind









First, we gather all of the free variables in the type family's kind and mark each as `nominal`. This is under the observation that only type variables can be at role `phantom` or `nominal`, never kind variables. Therefore, `k` would be marked as nominal.



First, we gather all of the free variables in the type family's kind and mark each as `nominal`. This is under the observation that only type variables can be at role `phantom` or `representational`, never kind variables. Therefore, `k` would be marked as nominal.






### The type family equations




...  ...  @@ 429,6 +456,8 @@ typefamilyEq w x y z whereEq a b (Either b a) c = a 





Returning to the earlier `F` example, we would learn that `e` and `g` should be marked nominal, as they are both scrutinized. Therefore, the final inferred roles for `k`, `e`, `f`, `g`, and `h` are `nominal`, `nominal`, `representational`, `nominal`, and `phantom`.






**RAE:** This works well for *closed* type families, but is ineffective with open type/data families (associated or not). I propose that open families default to nominal roles. This is quite like how open families' type variables default to kind `Type`. Edit: I see this addressed below, but the opening paragraph for this section mentions inference for open families. **End RAE**






## Role checking for type families







...  ...  