Any more commentary before submitting this to committee? Seems pretty straightforward.

Any more commentary before submitting this to committee?

None from me or @Haskell-mouse. Looks good, thank you!

Let's submit then, @nomeata .

/remind @serras to ensure progress in two weeks

@nomeata set a reminder for Oct 9th 2020

The cost of this proposal is mightily low (there is a small, already ready MR, which has essentially 0 net lines of code).

So I'd see the bar to pass to be just as low.

However, I think that the motivation would be quite a bit more readable, and will stand the test of time better, with a tiny bit of code illustrating the difficulty.

Are there any plans concerning Symbol/String (or maybe Text)? They have basically the same issue. Or would we want to wait for something that allows overloading type level strings? I remember that there was a proposal for this, but no idea what the status is

Are there any plans concerning Symbol/String (or maybe Text)?

There's ongoing work to make the promotion of Char possible, this way you also get String.

However, Symbol is more efficient than String, so we can't just unify them as we unify Nat and Natural here. This will require more thought, and a separate proposal. Personally, I like the idea of making Symbol inhabited at the term level by UTF-8 encoded strings.

@int-index You and colleagues (I don't have their GitHub usernames) are the instigators here. Would you care to write a better motivation section? Feel free just to push to my branch -- it seems you already have access.

My recommendation is to accept this proposal.

Apart from the small comment by @goldfirere, I think it would be nice for the proposal to point our that neither Natural nor the old Nat kind implement Peano naturals, so people should not expect to be able to decompose them.

@aspiwack I've added an example to the Motivation section. How is it looking now?

Are there any plans concerning Symbol/String (or maybe Text)?

There's ongoing work to make the promotion of Char possible, this way you also get String.

However, Symbol is more efficient than String, so we can't just unify them as we unify Nat and Natural here. This will require more thought, and a separate proposal. Personally, I like the idea of making Symbol inhabited at the term level by UTF-8 encoded strings.

Yeah to me the "right" way to do this is dramatically more work than this proposal and should be discussed separately. (I would want promoted IsString so we don't have to bloat base further.)

@aspiwack I've added an example to the Motivation section. How is it looking now?

It's the sort of things I had in mind. Thanks.

👋 @serras, ensure progress

@nomeata @serras What's the status here?

There seems to be pretty clear consensus on the commitee, I’ll mark this as accepted.