Skip to content
  • HaskellMouse's avatar
    Unification of Nat and Naturals · 8f4f5794
    HaskellMouse authored
    This commit removes the separate kind 'Nat' and enables promotion
    of type 'Natural' for using as type literal.
    It partially solves #10776
    
    Now the following code will be successfully typechecked:
        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
    
    But 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.
    The haddock submodule also have been updated.
    8f4f5794
To find the state of this project's repository at the time of any of these versions, check out the tags.