... | ... | @@ -20,75 +20,14 @@ See also |
|
|
|
|
|
## Tickets
|
|
|
|
|
|
|
|
|
|
|
|
Use Keyword = `Roles` to ensure that a ticket ends up on these lists.
|
|
|
|
|
|
|
|
|
|
|
|
**Open Tickets:**
|
|
|
|
|
|
<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>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/9118">#9118</a></th>
|
|
|
<td>Can't eta-reduce representational coercions</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11715">#11715</a></th>
|
|
|
<td>Constraint vs *</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13358">#13358</a></th>
|
|
|
<td>Role ranges (allow decomposition on newtypes)</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14292">#14292</a></th>
|
|
|
<td>Coercing between constraints of newtypes</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14317">#14317</a></th>
|
|
|
<td>Solve Coercible constraints over type constructors</td></tr>
|
|
|
<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>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14386">#14386</a></th>
|
|
|
<td>GHC doesn't allow Coercion between partly-saturated type constructors</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14694">#14694</a></th>
|
|
|
<td>Incompleteness in the Coercible constraint solver</td></tr>
|
|
|
<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>
|
|
|
<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>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
**Closed Tickets:**
|
|
|
|
|
|
<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>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/9117">#9117</a></th>
|
|
|
<td>Coercible constraint solver misses one</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/9123">#9123</a></th>
|
|
|
<td>Emit quantified Coercible constraints in GeneralizedNewtypeDeriving</td></tr>
|
|
|
<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>
|
|
|
<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>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11230">#11230</a></th>
|
|
|
<td>No run-time exception for deferred type errors when error is in a phantom role position</td></tr>
|
|
|
<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>
|
|
|
<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>
|
|
|
<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>
|
|
|
<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14363">#14363</a></th>
|
|
|
<td>:type hangs on coerce</td></tr>
|
|
|
<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>
|
|
|
<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>
|
|
|
|
|
|
|
|
|
See the ~roles label.
|
|
|
|
|
|
## The problem we wish to solve
|
|
|
|
|
|
|
|
|
GHC has had a hole in its type system for several years, as documented in #1496, #4846, #5498, and #7148. The common cause behind all of this is the magic behind `-XGeneralizedNewtypeDeriving` (GND). Here is an example:
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
newtype Age = MkAge { unAge :: Int }
|
|
|
|
|
|
type family Inspect x
|
... | ... | @@ -123,7 +62,7 @@ What to do? It turns out we need a subtler definition of type equality than what |
|
|
|
|
|
Datatypes, classes, and type synonyms can be parametric in their type arguments or not. By "parametric", I mean that they do not *inspect* the type argument. A non-parametric type variable is inspect. Here are some examples:
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
data List a = Nil | Cons a (List a) -- parametric
|
|
|
data GADT a where -- non-parametric
|
|
|
GAge :: GADT Age
|
... | ... | @@ -142,7 +81,7 @@ class BadIdea a where -- non-parametric |
|
|
|
|
|
In the terminology here, non-parametric types and classes care, in some fundamental way, what type parameter they are given. Parametric ones don't. We can generalize this idea a bit further to label each type variable as either parametric or not. For example,
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
data Mixed a b where
|
|
|
MInt :: a -> Mixed a Int
|
|
|
MAge :: a -> Mixed a Age
|
... | ... | @@ -156,7 +95,7 @@ is parametric in its first parameter but not its second. We say that a parametri |
|
|
|
|
|
The libraries with GHC 7.8 offer a new class
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
class Coercible a b where
|
|
|
coerce :: a -> b
|
|
|
```
|
... | ... | @@ -175,7 +114,7 @@ The rule is this: we have `instance Coercible a b => Coercible (T a) (T b)` if a |
|
|
|
|
|
Now that we have all of this `Coercible` machinery, we can define the behavior of GND in terms of it -- we simply `coerce` each method of the derived class. For example:
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
newtype RestrictedIO a = MkRIO { unRIO :: IO a }
|
|
|
deriving Monad
|
|
|
```
|
... | ... | @@ -183,7 +122,7 @@ newtype RestrictedIO a = MkRIO { unRIO :: IO a } |
|
|
|
|
|
generates
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
instance Monad RestrictedIO where
|
|
|
return = coerce (return :: a -> IO a) :: forall a. a -> RestrictedIO a
|
|
|
(>>=) = coerce ((>>=) :: IO a -> (a -> IO b) -> IO b) :: forall a b. RestrictedIO a -> (a -> RestrictedIO b) -> RestrictedIO b
|
... | ... | @@ -214,14 +153,14 @@ The exception to the above algorithm is for classes: all parameters for a class |
|
|
|
|
|
As we have learned with type and kind inference, sometimes the programmer wants to constrain the inference process. For example, the base library contains the following definition:
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
data Ptr a = Ptr Addr#
|
|
|
```
|
|
|
|
|
|
|
|
|
The idea is that `a` should really be a representational parameter, but role inference assigns it to phantom. This makes some level of sense: a pointer to an `Int` really *is* representationally the same as a pointer to a `Bool`. But, that's not at all how we want to use `Ptr`s! So, we want to be able to say
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
type role Ptr representational
|
|
|
data Ptr a = Ptr Addr#
|
|
|
```
|
... | ... | @@ -232,7 +171,7 @@ The `type role` annotation forces the parameter `a` to be at role representation |
|
|
|
|
|
If `Ptr` were to have multiple type parameter we would have used multiple `nominal`/`representational` annotations
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
type role Foo representational representational
|
|
|
data Foo a b = Foo Int
|
|
|
```
|
... | ... | @@ -248,7 +187,7 @@ Role annotations are allowed on type variables in `data`, `newtype`, and `class` |
|
|
|
|
|
Though a minor issue in the overall scheme, work on Roles had led to an interesting interaction with `Traversable`, excerpted here:
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
class Traversable t where
|
|
|
traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
|
|
|
```
|
... | ... | @@ -262,7 +201,7 @@ This means that GND no longer works with Traversable. But, DeriveTraversable *do |
|
|
|
|
|
Despite this, I believe that using GND with `Traversable` is indeed type-safe. Why? Because of the parametricity guaranteed in `Functor` and `Applicative`. The reason GND is prohibited with `Traversable` is that we are worried `f`'s last parameter will be at role nominal. While it is possible to write `Functor` and `Applicative` instances for such a type, the methods of those classes can't really use the any constructors that force the role to be nominal. For example, consider this:
|
|
|
|
|
|
```wiki
|
|
|
```haskell
|
|
|
data G a where
|
|
|
GInt :: a -> G Int
|
|
|
Ga :: a -> G a
|
... | ... | @@ -311,7 +250,7 @@ Currently, the type constructors for all type families and data families all con |
|
|
This example ([courtesy of glguy](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:32)) will not typecheck:
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
-- | Family of N-ary operator types.
|
|
|
type family Op n a b where
|
|
|
Op 'Z a b = b
|
... | ... | @@ -329,7 +268,7 @@ Since the role signature for `Op` is `type role Op nominal nominal nominal`. But |
|
|
Another example ([courtesy of int-index](https://ghc.haskell.org/trac/ghc/ticket/8177#comment:33)) is:
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
-- represents effect methods for some monad `m`
|
|
|
data family EffDict (eff :: k) (m :: Type -> Type)
|
|
|
|
... | ... | @@ -356,7 +295,7 @@ Again, `coerceDict` will not typecheck due to the role of `m` in `EffDict` being |
|
|
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)):
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
data Variant = DQuantity | DUnit Prefixability
|
|
|
data Dimension
|
|
|
|
... | ... | @@ -384,7 +323,7 @@ Once again, `coerceQuantity` is ill typed, simply because of the conservative `n |
|
|
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.,
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type role F nominal
|
|
|
type family F a
|
|
|
```
|
... | ... | @@ -393,7 +332,7 @@ type family F a |
|
|
But this is a restriction that is easily overcome. In addition, the parser does not currently recognize role annotations for associated type families:
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
class C a where
|
|
|
type role Assoc nominal nominal
|
|
|
type Assoc a b
|
... | ... | @@ -407,8 +346,7 @@ data families and data instances. And both might usefully |
|
|
have role annotations. For example:
|
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
```haskell
|
|
|
data family DF a b
|
|
|
type role DF nominal representational
|
|
|
|
... | ... | @@ -452,7 +390,7 @@ Regardless of whether we're dealing with a closed, open, or associated type fami |
|
|
Consider this type family:
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type family F (e :: *) (f :: *) (g :: *) (h :: *) :: k where
|
|
|
F Int b c d = c
|
|
|
F (Maybe a) b a d = Maybe b
|
... | ... | @@ -477,7 +415,7 @@ Next, we descend into each defining equation of the type family and inspect the |
|
|
The more interesting analysis comes when inspecting the left-hand 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 non-parametric fashion. For instance, we want to rule out scenarios like this one:
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type family Inspect x where
|
|
|
Inspect Bool = Int
|
|
|
Inspect Int = Bool
|
... | ... | @@ -494,7 +432,7 @@ 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:
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type family Inspect x where
|
|
|
Inspect Int = Bool
|
|
|
Inspect (Either a b) = a
|
... | ... | @@ -509,7 +447,7 @@ type family Inspect x where |
|
|
|
|
|
1. Type patterns that are syntactically equal are all marked as nominal. For instance:
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type family Eq w x y z where
|
|
|
Eq a b (Either b a) c = a
|
|
|
```
|
... | ... | @@ -532,7 +470,7 @@ Returning to the earlier `F` example, we would learn that `e` and `g` should be |
|
|
Users can also specify role annotations for type families that should be checked against the inferred roles. For instance:
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type role G nominal nominal
|
|
|
type family G a b where
|
|
|
G a b = Either a b
|
... | ... | @@ -546,7 +484,7 @@ If the user hadn't written the role annotation for `G`, its role signature would |
|
|
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?
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type family Open a b
|
|
|
```
|
|
|
|
... | ... | @@ -558,7 +496,7 @@ Here, we have a choice to make. We could decide to make the roles for open type |
|
|
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.,
|
|
|
|
|
|
|
|
|
```
|
|
|
```haskell
|
|
|
type role Open representational representational
|
|
|
type family Open a b
|
|
|
```
|
... | ... | |