There is an old GHC issue https://gitlab.haskell.org/ghc/ghc/-/issues/10776 which got recently a PR https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583 - Oleg On 9.7.2020 12.59, Rinat Stryungis wrote:
Hello, libraries!
I want to present a proposal for changes in the `Base` library. The changes in my proposal partially solve the following issue: https://gitlab.haskell.org/ghc/ghc/-/issues/10776 and remove the separate built-in kind `Nat` in favor of promoted type `Natural`.
It means that previously one can't directly promote a data type with Natural fields:
data MyPointN = PointN Natural Natural -- could not be promoted data MyPointP = PointP Nat Nat -- could be promoted, but uninhabited in terms
type M = PointP 1 10
but now one could promote the `Natural` data type:
data MyPoint = Point Natural Natural type MyTLPoint1 = Point 1 10
The proposed changes both simplify the internals of the GHC by removing separate kind and related things and make using of the type-level naturals more convenient for users.
Also new type synonym
type Nat = Natural
appeared in the Data.Type.TypeNats in the name of backward compatibility.
I've opened a new MR with the patch. In the patch with the already implemented promotion of Naturals, one could find new and updated tests and docs.
Also, I want to say about the breakages:
1. One must enable `TypeSynonymInstances` in order to define instances for `Nat`. 2. Different instances for `Nat` and `Natural` won't type check anymore. 3. Type checker plugins that work with the natural numbers now should use `naturalTy` kind instead of removed `typeNatKind`
Anyone interested is welcome to look at the MR and discuss the proposal and its implementation.
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583
The latter is very short and easy, thanks to the recently merged patch with a new `ghc-bignum` library. It greatly simplified my work.
Thanks and best regards. Rinat Stryungis.
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries