... | ... | @@ -234,7 +234,7 @@ Taking this all into account, Richard advocates for (B), but not all that strong |
|
|
## The new type system
|
|
|
|
|
|
|
|
|
The new type system adheres rather closely to what is proposed in the original "FC with Kind Equality" paper, available [here](http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf), with the addition of [NoSubKinds](no-sub-kinds). The type system, as implemented, is in the [ Core Specification](https://github.com/goldfirere/ghc/raw/nokinds/docs/core-spec/core-spec.pdf) document. Here are the highlights of the changes:
|
|
|
The new type system adheres rather closely to what is proposed in the original "FC with Kind Equality" paper, available [here](https://web.archive.org/web/20170918030940/http://cs.brynmawr.edu/~rae/papers/2013/fckinds/fckinds-extended.pdf), with the addition of [NoSubKinds](no-sub-kinds). The type system, as implemented, is in the [ Core Specification](https://github.com/goldfirere/ghc/raw/nokinds/docs/core-spec/core-spec.pdf) document. Here are the highlights of the changes:
|
|
|
|
|
|
- Two new constructors for `Type`: `CastTy :: Type -> Coercion -> Type` (which performs a kind cast) and `CoercionTy :: Coercion -> Type` which embeds coercions into types. The former eliminates kind coercions (that's the whole point of this change!) and the latter allows for the promotion of GADT data constructors, which will promote to a type taking a coercion argument.
|
|
|
|
... | ... | @@ -754,4 +754,4 @@ Once upon a time, I embarked on a mission to reduce imports of `TyCoRep`, instea |
|
|
More minor
|
|
|
|
|
|
- Remove `SubCo` in favour of implicit sub-roling. Do this in HEAD.
|
|
|
- Simon: make `GivenCt` contain `EvVar` only. In HEAD. |
|
|
- Simon: make `GivenCt` contain `EvVar` only. In HEAD. |
|
|
\ No newline at end of file |