Proposal for removing separate `Nat` in favour of promoted `Natural` type.

[Oleg Grenrus]

I should have read the whole email before replying... Sorry for the noise.

On 9.7.2020 15.09, Oleg Grenrus wrote:
>
> 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200709/d3bd050b/attachment.html>