Linear fields in NP

[alt-romes]

Hello!

I was hoping to replace my own generic heterogeneous list by sop-core's n-ary products NP, however, I realized I am not yet able to do this since the fields of NP are not linear.

Do you think we might have instead:

data NP :: (k -> Type) -> [k] -> Type where
  Nil  :: NP f '[]
-  (:*) :: f x -> NP f xs -> NP f (x ': xs)
+  (:*) :: f x %1 -> NP f xs %1 -> NP f (x ': xs)

In theory, this would only affect LinearType users of sop-core who use an NP linearly, which I reckon are not many, as otherwise all datatype constructors have linear components instead of unrestricted ones by default.

I would additionally argue that NP having linear fields is something that wasn't previously considered, as the first commit defining NP is from 2014, when LinearTypes were nowhere in sight, and was already using the GADTSyntax with unrestricted arrows.

Much appreciated!