This patch removes the separate kind 'Nat' and enables promotion of type 'Natural' for using as type literal.
Now the following code will be successfully type-checked:
data C = MkC Natural type CC = MkC 1
Before this change, we had to create the separate type for promotion
data C = MkC Natural data CP = MkCP Nat type CC = MkCP 1
CP is uninhabited in terms.
For backward compatibility type synonym
Nat has been made:
type Nat = Natural
The user's documentation and tests have been updated.
WIP since one of the tests stuck for some reason.