<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>There is an old GHC issue <a
href="https://gitlab.haskell.org/ghc/ghc/-/issues/10776">https://gitlab.haskell.org/ghc/ghc/-/issues/10776</a>
which got recently a PR <a
href="https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583">https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583</a></p>
<p>- Oleg<br>
</p>
<div class="moz-cite-prefix">On 9.7.2020 12.59, Rinat Stryungis
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAM89rCXAWC8A2cJrkJ+pMMdRyjd5GCy0h4oFOBTgug8xsF-u4A@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">Hello, libraries!<br>
<br>
I want to present a proposal for changes in the `Base` library.
<br>
The changes in my proposal partially solve the following issue:
<br>
<a href="https://gitlab.haskell.org/ghc/ghc/-/issues/10776"
moz-do-not-send="true">https://gitlab.haskell.org/ghc/ghc/-/issues/10776</a>
<br>
and remove the separate built-in kind `Nat` in favor of promoted
type `Natural`. <br>
<br>
It means that previously one can't directly promote a data type
with Natural fields: <br>
<br>
data MyPointN = PointN Natural Natural -- could not be
promoted <br>
data MyPointP = PointP Nat Nat -- could be promoted,
but uninhabited in terms<br>
<br>
type M = PointP 1 10 <br>
<br>
but now one could promote the `Natural` data type: <br>
<br>
data MyPoint = Point Natural Natural<br>
type MyTLPoint1 = Point 1 10 <br>
<br>
The proposed changes both simplify the internals of the GHC by
removing <br>
separate kind and related things and make using of the
type-level <br>
naturals more convenient for users. <br>
<br>
Also new type synonym <br>
<br>
type Nat = Natural <br>
<br>
appeared in the Data.Type.TypeNats in the name of backward
compatibility. <br>
<br>
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. <br>
<br>
Also, I want to say about the breakages: <br>
<br>
1. One must enable `TypeSynonymInstances` in order to define
instances for `Nat`.<br>
2. Different instances for `Nat` and `Natural` won't type check
anymore.<br>
3. Type checker plugins that work with the natural numbers now <br>
should use `naturalTy` kind instead of removed `typeNatKind`<br>
<br>
Anyone interested is welcome to look at the MR and discuss the
proposal and its implementation. <br>
<br>
<a
href="https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583"
moz-do-not-send="true">https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583</a><br>
<br>
The latter is very short and easy, thanks to the recently merged
patch with a new `ghc-bignum` library. It greatly simplified my
work. <br>
<br>
Thanks and best regards. <br>
Rinat Stryungis. </div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Libraries mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Libraries@haskell.org">Libraries@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</body>
</html>