...  @@ 21,59 +21,67 @@ See also 
...  @@ 21,59 +21,67 @@ See also 

## Tickets


## Tickets














Use Keyword = `Roles` to ensure that a ticket ends up on these lists.


Use Keyword = `Roles` to ensure that a ticket ends up on these lists.














**Open Tickets:**


**Open Tickets:**






<table><tr><th>[\#9112](https://gitlab.haskell.org//ghc/ghc/issues/9112)</th>


<table><tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9112">#9112</a></th>


<td>support for deriving Vector/MVector instances</td></tr>


<td>support for deriving Vector/MVector instances</td></tr>


<tr><th>[\#9118](https://gitlab.haskell.org//ghc/ghc/issues/9118)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9118">#9118</a></th>


<td>Can't etareduce representational coercions</td></tr>


<td>Can't etareduce representational coercions</td></tr>


<tr><th>[\#11715](https://gitlab.haskell.org//ghc/ghc/issues/11715)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11715">#11715</a></th>


<td>Constraint vs \*</td></tr>


<td>Constraint vs *</td></tr>


<tr><th>[\#13358](https://gitlab.haskell.org//ghc/ghc/issues/13358)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13358">#13358</a></th>


<td>Role ranges (allow decomposition on newtypes)</td></tr>


<td>Role ranges (allow decomposition on newtypes)</td></tr>


<tr><th>[\#14292](https://gitlab.haskell.org//ghc/ghc/issues/14292)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14292">#14292</a></th>


<td>Coercing between constraints of newtypes</td></tr>


<td>Coercing between constraints of newtypes</td></tr>


<tr><th>[\#14317](https://gitlab.haskell.org//ghc/ghc/issues/14317)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14317">#14317</a></th>


<td>Solve Coercible constraints over type constructors</td></tr>


<td>Solve Coercible constraints over type constructors</td></tr>


<tr><th>[\#14362](https://gitlab.haskell.org//ghc/ghc/issues/14362)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14362">#14362</a></th>


<td>Allow: Coercing (a:\~:b) to (b:\~:a)</td></tr>


<td>Allow: Coercing (a:~:b) to (b:~:a)</td></tr>


<tr><th>[\#14386](https://gitlab.haskell.org//ghc/ghc/issues/14386)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14386">#14386</a></th>


<td>GHC doesn't allow Coercion between partlysaturated type constructors</td></tr>


<td>GHC doesn't allow Coercion between partlysaturated type constructors</td></tr>


<tr><th>[\#14694](https://gitlab.haskell.org//ghc/ghc/issues/14694)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14694">#14694</a></th>


<td>Incompleteness in the Coercible constraint solver</td></tr>


<td>Incompleteness in the Coercible constraint solver</td></tr>


<tr><th>[\#15441](https://gitlab.haskell.org//ghc/ghc/issues/15441)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15441">#15441</a></th>


<td>Data type with phantoms using TypeInType isn't coercible</td></tr>


<td>Data type with phantoms using TypeInType isn't coercible</td></tr>


<tr><th>[\#15707](https://gitlab.haskell.org//ghc/ghc/issues/15707)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15707">#15707</a></th>


<td>More liberally kinded coercions for newtypes</td></tr></table>


<td>More liberally kinded coercions for newtypes</td></tr></table>


















**Closed Tickets:**


**Closed Tickets:**






<table><tr><th>[\#8246](https://gitlab.haskell.org//ghc/ghc/issues/8246)</th>


<table><tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/8246">#8246</a></th>


<td>Role annotations does not allow the use of parenthesis</td></tr>


<td>Role annotations does not allow the use of parenthesis</td></tr>


<tr><th>[\#9117](https://gitlab.haskell.org//ghc/ghc/issues/9117)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9117">#9117</a></th>


<td>Coercible constraint solver misses one</td></tr>


<td>Coercible constraint solver misses one</td></tr>


<tr><th>[\#9123](https://gitlab.haskell.org//ghc/ghc/issues/9123)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9123">#9123</a></th>


<td>Emit quantified Coercible constraints in GeneralizedNewtypeDeriving</td></tr>


<td>Emit quantified Coercible constraints in GeneralizedNewtypeDeriving</td></tr>


<tr><th>[\#9131](https://gitlab.haskell.org//ghc/ghc/issues/9131)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9131">#9131</a></th>


<td>Experiment with a dedicated solver for Coercible</td></tr>


<td>Experiment with a dedicated solver for Coercible</td></tr>


<tr><th>[\#10905](https://gitlab.haskell.org//ghc/ghc/issues/10905)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/10905">#10905</a></th>


<td>Incorrect number of parameters in "role" errors</td></tr>


<td>Incorrect number of parameters in "role" errors</td></tr>


<tr><th>[\#11230](https://gitlab.haskell.org//ghc/ghc/issues/11230)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11230">#11230</a></th>


<td>No runtime exception for deferred type errors when error is in a phantom role position</td></tr>


<td>No runtime exception for deferred type errors when error is in a phantom role position</td></tr>


<tr><th>[\#12616](https://gitlab.haskell.org//ghc/ghc/issues/12616)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12616">#12616</a></th>


<td>type synonyms confuse generalized newtype deriving role checking</td></tr>


<td>type synonyms confuse generalized newtype deriving role checking</td></tr>


<tr><th>[\#14101](https://gitlab.haskell.org//ghc/ghc/issues/14101)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14101">#14101</a></th>


<td>Type synonyms can make roles too conservative</td></tr>


<td>Type synonyms can make roles too conservative</td></tr>


<tr><th>[\#14333](https://gitlab.haskell.org//ghc/ghc/issues/14333)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14333">#14333</a></th>


<td>GHC doesn't use the fact that Coercible is symmetric</td></tr>


<td>GHC doesn't use the fact that Coercible is symmetric</td></tr>


<tr><th>[\#14363](https://gitlab.haskell.org//ghc/ghc/issues/14363)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14363">#14363</a></th>


<td>:type hangs on coerce</td></tr>


<td>:type hangs on coerce</td></tr>


<tr><th>[\#15294](https://gitlab.haskell.org//ghc/ghc/issues/15294)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15294">#15294</a></th>


<td>Unused "foralls" prevent types from being Coercible</td></tr>


<td>Unused "foralls" prevent types from being Coercible</td></tr>


<tr><th>[\#15431](https://gitlab.haskell.org//ghc/ghc/issues/15431)</th>


<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15431">#15431</a></th>


<td>Coercible and Existential types don't play nicely</td></tr></table>


<td>Coercible and Existential types don't play nicely</td></tr></table>














## The problem we wish to solve


## The problem we wish to solve





...  @@ 103,8 +111,10 @@ This code is accepted by GHC 7.6.3. Yet, it goes wrong when you say `bad (MkAge 
...  @@ 103,8 +111,10 @@ This code is accepted by GHC 7.6.3. Yet, it goes wrong when you say `bad (MkAge 

A newtype is a new algebraic datatype that wraps up exactly one field (in our example, of type `Int`). Yet, the semantics of Haskell makes a guarantee that wrapping and unwrapping a value (with `MkAge` or `unAge`) has no runtime cost. Thus, internally, we must consider `Age` to be wholly equivalent to `Int`.


A newtype is a new algebraic datatype that wraps up exactly one field (in our example, of type `Int`). Yet, the semantics of Haskell makes a guarantee that wrapping and unwrapping a value (with `MkAge` or `unAge`) has no runtime cost. Thus, internally, we must consider `Age` to be wholly equivalent to `Int`.














The problem with this idea comes with type families. (There are other ways to tickle the bug, but one example is enough here.) A type family can branch on *Haskell* type, and of course, in Haskell (unlike in the internals of a compiler), `Age` is most certainly *not* `Int`. (If it were, newtypes would be useless for controlling instance selection, a very popular use case.) So, in our example, we see that `Inspect Age` is `Int`, but `Inspect Int` is `Bool`. Now, note the type of `bad`, the method in class `BadIdea`. When passed an `Int`, `bad` will return a `Bool`. When passed an `Age`, `bad` will return an `Int`. What happens on the last line above, when we use GND? Internally, we take the existing instance for `Int` and just transform it into an instance for `Age`. But, this transformation is very dumb  because `Age` and `Int` are the same, internally, the code for the `Age` instance and the code for the `Int` instance are the same. This means that when we call `bad (MkAge 5)`, we run `5` through the existing implementation for `bad`, which produces a `Bool`. But, of course, the type of `bad (MkAge 5)` is `Int`, and so we have effectively converted a `Bool` to an `Int`. Yuck.


The problem with this idea comes with type families. (There are other ways to tickle the bug, but one example is enough here.) A type family can branch on *Haskell* type, and of course, in Haskell (unlike in the internals of a compiler), `Age` is most certainly *not* `Int`. (If it were, newtypes would be useless for controlling instance selection, a very popular use case.) So, in our example, we see that `Inspect Age` is `Int`, but `Inspect Int` is `Bool`. Now, note the type of `bad`, the method in class `BadIdea`. When passed an `Int`, `bad` will return a `Bool`. When passed an `Age`, `bad` will return an `Int`. What happens on the last line above, when we use GND? Internally, we take the existing instance for `Int` and just transform it into an instance for `Age`. But, this transformation is very dumb  because `Age` and `Int` are the same, internally, the code for the `Age` instance and the code for the `Int` instance are the same. This means that when we call `bad (MkAge 5)`, we run `5` through the existing implementation for `bad`, which produces a `Bool`. But, of course, the type of `bad (MkAge 5)` is `Int`, and so we have effectively converted a `Bool` to an `Int`. Yuck.










## The solution


## The solution









...  @@ 297,10 +307,14 @@ Currently, the type constructors for all type families and data families all con 
...  @@ 297,10 +307,14 @@ Currently, the type constructors for all type families and data families all con 

## Examples we cannot write today


## Examples we cannot write today














This example ([ courtesy of glguy](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:32)) will not typecheck:


This example ([ courtesy of glguy](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:32)) will not typecheck:










```


```


  Family of Nary operator types.typefamilyOp n a b whereOp'Z a b = b


  Family of Nary operator types.




type family Op n a b where




Op 'Z a b = b


Op ('S n) a b = a > Op n a b


Op ('S n) a b = a > Op n a b






coerceOp :: Coercible a b => Op n a c > Op n b c


coerceOp :: Coercible a b => Op n a c > Op n b c

...  @@ 311,27 +325,52 @@ coerceOp= coerce 
...  @@ 311,27 +325,52 @@ 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. **RAE:** "feels"? Let's prove it! **End RAE**


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:


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










```


```


 represents effect methods for some monad `m`datafamilyEffDict(eff :: k)(m ::Type>Type) Note this matches on `eff`, not `m`dataStateEff s


 represents effect methods for some monad `m`


datainstanceEffDict(StateEff s) m =StateDict{ _state :: forall a .(s >(a,s))> m a,


data family EffDict (eff :: k) (m :: Type > Type)








 Note this matches on `eff`, not `m`




data StateEff s




data instance EffDict (StateEff s) m =




StateDict




{ _state :: forall a . (s > (a,s)) > m a,


_get :: m s,


_get :: m s,


_put :: s > m ()} composition of monad transformersnewtypeTComp t1 t2 m a =TComp(t1 (t2 m) a)coerceDict::EffDict eff (t1 (t2 m))>EffDict eff (TComp t1 t2 m)coerceDict= coerce


_put :: s > m () }








 composition of monad transformers




newtype TComp t1 t2 m a = TComp (t1 (t2 m) a)








coerceDict :: EffDict eff (t1 (t2 m)) > EffDict eff (TComp t1 t2 m)




coerceDict = coerce


```


```










Again, `coerceDict` will not typecheck due to the role of `m` in `EffDict` being `nominal`. But there's no good reason why this *must* be the case—we ought to be able to tell GHC to allow `m` to have `representational role`. (Of course, this would prevent any `EffDict` instance from using `m` at a `nominal` role, but them's the breaks.)


Again, `coerceDict` will not typecheck due to the role of `m` in `EffDict` being `nominal`. But there's no good reason why this *must* be the case—we ought to be able to tell GHC to allow `m` to have `representational role`. (Of course, this would prevent any `EffDict` instance from using `m` at a `nominal` role, but them's the breaks.)














Additionally, we might like to have roles for *associated* type families. For instance, consider this example ([ courtesy of dmcclean](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:20)):


Additionally, we might like to have roles for *associated* type families. For instance, consider this example ([ courtesy of dmcclean](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:20)):










```


```


dataVariant=DQuantityDUnitPrefixabilitydataDimensionclassKnownVariant(var ::Variant)wheredataDimensional var ::Dimension>*>*instanceKnownVariantDQuantitywherenewtypeDimensionalDQuantity d v =Quantity' v


data Variant = DQuantity  DUnit Prefixability




data Dimension








class KnownVariant (var :: Variant) where




data Dimensional var :: Dimension > * > *






instanceKnownVariant(DUnit p)wheredataDimensional(DUnit p) d v =Unit'UnitName v


instance KnownVariant DQuantity where




newtype Dimensional DQuantity d v = Quantity' v






typeQuantity=DimensionalDQuantitycoerceQuantity::Coercible v w =>Quantity d v >Quantity d w


instance KnownVariant (DUnit p) where




data Dimensional (DUnit p) d v = Unit' UnitName v








type Quantity = Dimensional DQuantity




coerceQuantity :: Coercible v w => Quantity d v > Quantity d w


coerceQuantity = coerce


coerceQuantity = coerce


```


```





...  @@ 341,8 +380,10 @@ Once again, `coerceQuantity` is ill typed, simply because of the conservative `n 
...  @@ 341,8 +380,10 @@ Once again, `coerceQuantity` is ill typed, simply because of the conservative `n 

## Syntax


## Syntax














Implementing roles for type families would not require too many changes to the syntax of the language, as most of the required pieces are already there. The biggest current restriction is the fact that one cannot declare role annotations for type families, e.g.,


Implementing roles for type families would not require too many changes to the syntax of the language, as most of the required pieces are already there. The biggest current restriction is the fact that one cannot declare role annotations for type families, e.g.,










```


```


type role F nominal


type role F nominal


type family F a


type family F a

...  @@ 351,8 +392,10 @@ typefamilyF a 
...  @@ 351,8 +392,10 @@ 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:


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


class C a where




type role Assoc nominal nominal


type Assoc a b


type Assoc a b


```


```





...  @@ 363,12 +406,17 @@ But this could be added without much difficulty. 
...  @@ 363,12 +406,17 @@ But this could be added without much difficulty. 

data families and data instances. And both might usefully


data families and data instances. And both might usefully


have role annotations. For example:


have role annotations. For example:










```


```






data family DF a b


data family DF a b


type role DF nominal representational


type role DF nominal representational






data instance DF Int b = MkDFInt b


data instance DF Int b = MkDFInt b


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


 NB: No scrutinizing the second parameter.




 Also, b is not used in a nominal context








data instance DF [c] b = MkDFList c b


type role DF [nominal] representational


type role DF [nominal] representational






data instance DF (Maybe d) b = MkDFMaybe d b


data instance DF (Maybe d) b = MkDFMaybe d b

...  @@ 400,10 +448,13 @@ Regardless of whether we're dealing with a closed, open, or associated type fami 
...  @@ 400,10 +448,13 @@ Regardless of whether we're dealing with a closed, open, or associated type fami 

### Example


### Example














Consider this type family:


Consider this type family:










```


```


typefamilyF(e ::*)(f ::*)(g ::*)(h ::*):: k whereFInt b c d = c


type family F (e :: *) (f :: *) (g :: *) (h :: *) :: k where




F Int b c d = c


F (Maybe a) b a d = Maybe b


F (Maybe a) b a d = Maybe b


F a b c d = a


F a b c d = a


```


```

...  @@ 422,13 +473,20 @@ First, we gather all of the free variables in the type family's kind and mark ea 
...  @@ 422,13 +473,20 @@ First, we gather all of the free variables in the type family's kind and mark ea 

Next, we descend into each defining equation of the type family and inspect the lefthand and righthand sides. The righthand sides are analyzed just like the fields of a data constructor; see the [ Role inference](https://ghc.haskell.org/trac/ghc/wiki/Roles#Roleinference) section above for more details. From the righthand sides, we learn that the roles of `e`, `f`, and `g` should be (at least) `representational`.


Next, we descend into each defining equation of the type family and inspect the lefthand and righthand sides. The righthand sides are analyzed just like the fields of a data constructor; see the [ Role inference](https://ghc.haskell.org/trac/ghc/wiki/Roles#Roleinference) section above for more details. From the righthand sides, we learn that the roles of `e`, `f`, and `g` should be (at least) `representational`.














The more interesting analysis comes when inspecting the lefthand sides. We want to mark any type variable that is *scrutinized* as `nominal`. By "scrutinized", we mean a variable that is being used in a nonparametric fashion. For instance, we want to rule out scenarios like this one:


The more interesting analysis comes when inspecting the lefthand sides. We want to mark any type variable that is *scrutinized* as `nominal`. By "scrutinized", we mean a variable that is being used in a nonparametric fashion. For instance, we want to rule out scenarios like this one:










```


```


typefamilyInspect x whereInspectBool=IntInspectInt=BoolcoerceInspect::Coercible a b =>Inspect a >Inspect b


type family Inspect x where




Inspect Bool = Int




Inspect Int = Bool








coerceInspect :: Coercible a b => Inspect a > Inspect b


coerceInspect = coerce


coerceInspect = coerce






unsafeBoolToInt::Bool>IntunsafeBoolToInt=(coerceInspect ::InspectInt>InspectAge)


unsafeBoolToInt :: Bool > Int




unsafeBoolToInt = (coerceInspect :: Inspect Int > Inspect Age)


```


```









...  @@ 437,21 +495,30 @@ To accomplish this, we check for any occurences of the either of the following s 
...  @@ 437,21 +495,30 @@ To accomplish this, we check for any occurences of the either of the following s 

1. A type pattern that is not a single type variable. For instance, all of these equations provde examples of type patterns which do scrutinize a particular type variable:


1. A type pattern that is not a single type variable. For instance, all of these equations provde examples of type patterns which do scrutinize a particular type variable:






```


```


typefamilyInspect x whereInspectInt=BoolInspect(Either a b)= a


type family Inspect x where




Inspect Int = Bool




Inspect (Either a b) = a


Inspect (f a) = a


Inspect (f a) = a


```


```








>


>


>


> Any type variable that is scrutinized in this fashion (`x` in the above example) is marked as `nominal`.


> Any type variable that is scrutinized in this fashion (`x` in the above example) is marked as `nominal`.




>




>






1. Type patterns that are syntactically equal are all marked as nominal. For instance:


1. Type patterns that are syntactically equal are all marked as nominal. For instance:






```


```


typefamilyEq w x y z whereEq a b (Either b a) c = a


type family Eq w x y z where




Eq a b (Either b a) c = a


```


```








>


>


>


> Here, we have two variable names that are used in multiple places: `a` and `b`. As a result, the type variables which they inhabit (`w`, `x`, and `y`) are all marked as `nominal`.


> Here, we have two variable names that are used in multiple places: `a` and `b`. As a result, the type variables which they inhabit (`w`, `x`, and `y`) are all marked as `nominal`.




>




>










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


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

...  @@ 461,19 +528,24 @@ Returning to the earlier `F` example, we would learn that `e` and `g` should be 
...  @@ 461,19 +528,24 @@ Returning to the earlier `F` example, we would learn that `e` and `g` should be 

## Role checking for type families


## Role checking for type families














Users can also specify role annotations for type families that should be checked against the inferred roles. For instance:


Users can also specify role annotations for type families that should be checked against the inferred roles. For instance:










```


```


type role G nominal nominal


type role G nominal nominal


typefamilyG a b whereG a b =Either a b


type family G a b where




G a b = Either a b


```


```










If the user hadn't written the role annotation for `G`, its role signature would have been inferred to be `type role G representational representational`. However, role checking overrides the inferred roles and assigns the more conservative roles of `type role G nominal nominal`.


If the user hadn't written the role annotation for `G`, its role signature would have been inferred to be `type role G representational representational`. However, role checking overrides the inferred roles and assigns the more conservative roles of `type role G nominal nominal`.














Note that while writing role annotations for *closed* type families is purely optional, it is somewhat more important for open type families. For instance, what should be the roles for this type family?


Note that while writing role annotations for *closed* type families is purely optional, it is somewhat more important for open type families. For instance, what should be the roles for this type family?










```


```


type family Open a b


type family Open a b


```


```

...  @@ 482,8 +554,10 @@ typefamilyOpen a b 
...  @@ 482,8 +554,10 @@ typefamilyOpen a b 

Here, we have a choice to make. We could decide to make the roles for open type families default to, say, `representational`. While this would give us the freedom to `coerce` values of type `Open a b` more freely, it simultaneously restricts the instances we can give for `Open`, since every type instance must be checked to ensure that neither `a` nor `b` is used at a `nominal` role.


Here, we have a choice to make. We could decide to make the roles for open type families default to, say, `representational`. While this would give us the freedom to `coerce` values of type `Open a b` more freely, it simultaneously restricts the instances we can give for `Open`, since every type instance must be checked to ensure that neither `a` nor `b` is used at a `nominal` role.














For the sake of backwards compatibility and the principle of least surprise, roles for open type families default to `nominal`. This allows more instances to be written, but makes it harder to `coerce` them. If a user wishes to `coerce` open type families, the onus is on her to write a role annotation, e.g.,


For the sake of backwards compatibility and the principle of least surprise, roles for open type families default to `nominal`. This allows more instances to be written, but makes it harder to `coerce` them. If a user wishes to `coerce` open type families, the onus is on her to write a role annotation, e.g.,










```


```


type role Open representational representational


type role Open representational representational


type family Open a b


type family Open a b

...   ...  