GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-03-03T14:56:11Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/8177Roles for type families2023-03-03T14:56:11ZSimon Peyton JonesRoles for type familiesNow that we have [roles](roles), it might be helpful to be able to give a role signature for a data/type family.
At the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus
```
data fam...Now that we have [roles](roles), it might be helpful to be able to give a role signature for a data/type family.
At the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus
```
data family D a -- Parameter conservatively assumed to be N
class C a where
op :: D a -> a
instance C Int where ....
newtype N a = MkN a deriving( C ) -- Rejected
```
The generalised-newtype-deriving clause `deriving( C )` is rejected because `D` might use its parameter at role `N` thus:
```
data instance D [b] = MkD (F b) -- F is a type function
```
It would be strictly more expressive if we could
- **Declare** the roles of D's arguments (as we can declare their kinds). E.g.
```
data family D a@R
```
- **Check** that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance:
```
data instance D [b] = MkD (F b) -- F is a type function
```
I think there is no technical difficulty here. Just a question of doing it.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Roles for type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Now that we have [wiki:Roles roles], it might be helpful to be able to give a role signature for a data/type family.\r\n\r\nAt the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus\r\n{{{\r\ndata family D a -- Parameter conservatively assumed to be N\r\n\r\nclass C a where\r\n op :: D a -> a\r\n\r\ninstance C Int where ....\r\n\r\nnewtype N a = MkN a deriving( C ) -- Rejected\r\n}}}\r\nThe generalised-newtype-deriving clause `deriving( C )` is rejected because `D` might use its parameter at role `N` thus:\r\n{{{\r\ndata instance D [b] = MkD (F b) -- F is a type function\r\n}}}\r\nIt would be strictly more expressive if we could\r\n * '''Declare''' the roles of D's arguments (as we can declare their kinds). E.g.\r\n{{{\r\ndata family D a@R\r\n}}}\r\n * '''Check''' that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance:\r\n{{{\r\ndata instance D [b] = MkD (F b) -- F is a type function\r\n}}}\r\n\r\nI think there is no technical difficulty here. Just a question of doing it.","type_of_failure":"OtherFailure","blocking":[]} -->⊥Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev