Note [Data constructors are linear by default]

GHC/Core/Multiplicity.hs:211 compiler

All data constructors defined without -XLinearTypes, as well as data constructors
defined with the Haskell 98 in all circumstances, have all their fields linear.

That is, in

    data Maybe a = Nothing | Just a

We have

    Just :: a %1 -> Just a

Irrespective of whether -XLinearTypes is turned on or not. Furthermore, when
-XLinearTypes is turned off, the declaration

    data Endo a where { MkIntEndo :: (Int -> Int) -> T Int }

gives

    MkIntEndo :: (Int -> Int) %1 -> T Int

With -XLinearTypes turned on, instead, this would give

    data EndoU a where { MkIntEndoU :: (Int -> Int) -> T Int }
    MkIntEndoU :: (Int -> Int) -> T Int

With -XLinearTypes turned on, to get a linear field with GADT syntax we
would need to write

    data EndoL a where { MkIntEndoL :: (Int -> Int) %1 -> T Int }

The goal is to maximise reuse of types between linear code and traditional
code. This is argued at length in the proposal and the article (links in Note
[Linear types]).

Unrestricted field don't need to be consumed for a value to be consumed exactly
once. So consuming a value of type `IntEndoU a` exactly once means forcing it at
least once.

Why “at least once”? Because if `case u of { MkIntEndoL x -> f (MkIntEndoL x) }`
is linear (provided `f` is a linear function). But we might as well have done
`case u of { !z -> f z }`. So, we can observe constructors as many times as we
want, and we are actually allowed to force the same thing several times because
laziness means that we are really forcing the value once, and observing its
constructor several times. The type checker and the linter recognise some (but
not all) of these multiple forces as indeed linear. Mostly just enough to
support variable patterns.

In summary:

- Fields of data constructors defined with Haskell 98 syntax are always linear
  (even if `-XLinearTypes` is off). This choice has been made to favour sharing
  types between linearly typed Haskell and traditional Haskell. To avoid an
  ecosystem split.
- When `-XLinearTypes` is off, GADT-syntax declaration can only use the regular
  arrow `(->)`. However all the fields are linear.

References 0

This Note does not link to any other.

Referenced by 3