Levity should be on the arrow, not on the kind

[atravers]

Well, I prefer strictness for types rather than just parameters, in the same way e.g. Clean or Single-Assignment C have uniqueness for types rather than just parameters - as I explained here:

Experience Report: Linear Haskell enables Pure, Parallel, and In-place Fast Fourier Transformation

Sometimes, however, linearity annotations can add boilerplate clutter. What I’m thinking about is the Unique and associated UniqueSupply types in GHC: (…presumably values of these types should not be reused, hence the use of the word “unique”.) Since both types already exist and are used considerably in GHC, changing them to use linearity annotations should preferably require changes to none (or a few) existing types and type signatures. It seems to me that based on !10952: Linear let and wh…

…only having linearity for parameters (but not types) isn’t always enough - I would expect that having only strictness for parameters (but not types) will invariably encounter similar problems.

In summary: to me, moving strictness from types to parameters goes against the DRY principle - rather that placing the strictness annotation only on the type declaration (best case), all functions which use that type would need their signatures annotated (worst case).