## 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, 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.