Linear types: projections of records

Currently, record selectors are always non-linear functions.

data P a b = P { p1 :: a, p2 :: b }
p1 :: P a b -> a
p2 :: P a b -> b

However, if a record contains only one field, we can make the projection function linear. This is especially useful for newtypes:

newtype N = N { unN :: A }
unN :: N -> A -- could be N #-> A
              -- but because of backwards compat, we must use forall {m}. N # m -> A

This is similar to constructors being multiplicity polymorphic.

Once we have syntax for multiplicity in record fields #18462 (closed), this can apply more generally to records where all fields except one are unrestricted, e.g. in data R = R { unrestrictedField # 'Many :: A, linearField # 'One :: B } the linearField projection can be linear.

This is not completely trivial to implement - it changes the output in TH (T11103), interacts with overloaded record fields. The case in the definition of unN in Core needs to be case[1], while the current method uses case[Many]. My old (not working) attempt is at https://github.com/tweag/ghc/commit/5cdd5893570d694056c9f1717d8bb77191601a43.