Why must newtype constructors be linear?
newtype constructors are required to be linear:
ghci> newtype Ur a where Ur :: a -> Ur a <interactive>:8:20: error: • A newtype constructor must be linear • In the definition of data constructor ‘Ur’ In the newtype declaration for ‘Ur’
There's no explanation in the documentation for why this might be, and it's not at all obvious. The reasoning should be documented, or the restriction lifted. Of course, if the restriction is lifted, then the usual newtype coercion axiom will have to be suppressed (in the surface language) for nonlinear newtypes.
- GHC version used (if appropriate): 9.0